FormalTCS、175問のLean課題で研究プロセスを評価——自動形式化の最高スコアはわずか11.5点

FormalTCSは、理論計算機科学の研究プロセスを、中心的な主張の理解、自然言語による記述の作成、定理の形式化、証明戦略の立案、Lean証明の生成といった段階に分解した。データセットには、2025年から2026年にSTOC、FOCS、SODA、COLTで採択された論文を出典とする175件の事例が収録されている。各論文固有の定義、仮定、証明の依存関係を保持し、専門家がLean版を作成・検証した。

研究では、Codex、Claude Code、DeepSeek harnessを使用して、GPT-5.6、Claude 5、DeepSeek-V4の各シリーズを評価した。Claude Opus 5は自然言語による証明戦略の生成で68.7点を獲得したが、自然言語の主張から形式的な定義と定理を生成するNC2FT段階では11.5点にとどまった。GPT-5.6 Solも同様に67.9点から10.6点へ低下した。人間があらかじめ形式化済みの定理を提供した場合、Opus 5によるLean証明のPass@8は28.6に達した。この結果は、難しさが証明探索だけにあるのではなく、数学的対象、量化子、仮定、型を識別し、正確にエンコードする工程にもあることを示している。

チームはさらに、planner、formalizer、judgerで構成される研究ループを構築した。システムが提案した64件の新たな主張のうち、専門家による価値評価と形式証明による検証の両方を通過したのは、最終的にわずか6件だった。これは、「研究上のセンス」が形式的正しさとは別の第二の関門であることを浮き彫りにしている。著者らは匿名化した断片を用いてブラックボックス型のデータ汚染監査を実施し、最も高性能な2モデルのテキスト再構成類似度が9.6％未満であることを確認した。ただし、これは訓練データ漏洩への懸念を軽減するにすぎず、完全には排除できない。また、自然言語段階の評価は一部LLMによる採点に依存している。エンジニアリング上の重要な示唆は、自動定理証明エージェントに独立した定義チェック層と形式化検証層がなければ、証明戦略が一見妥当に見えても、誤った命題を起点として推論全体が進んでしまう可能性があるという点だ。