arXiv:2606.14000 ―― AIエージェントが数学の教科書を形式化：コンパイルは正確性を保証しない

大きな野心：教科書全体をLean 4へ

数学の形式的検証――Lean 4、Coq、Isabelleのようなシステムでの定理証明――は伝統的に何千時間もの専門的な手作業を必要とする。Theodore Meek、Siyuan Ge、Di Qiu Xiang、Simon Chess、Vasily Ilinの研究者たちは、自動化されたエージェントパイプラインを野心的な目標に適用した：Mathlibライブラリを使用して常微分方程式の数値的手法に関する教科書全体をLean 4に形式化することだ。

数値解析は特に要求の厳しい目標だ。この数学の分野は既存の形式的ライブラリでは比較的カバレッジが低く、エージェントが既に証明された補題を単純に呼び出せず、ゼロから形式化された基盤を構築しなければならないことを意味する。

コンパイルは正確性の十分な証明か？

形式的な数学コードを書くエージェントを評価するための標準的な指標はカーネルの受理――コードがエラーなしにLean検証器を通過するか――だ。一見すると、これは堅固なシグナルのように見える：カーネルが文を受理すれば、それは形式的に正しいと証明されている。

研究はこの前提を否定する。著者たちはカーネルの受理が本質的に意味論的エラーを隠蔽することを発見した――エージェントはコンパイルされるが数学的な意味では不正確な文を定期的に生成する。さらに、コンパイルに基づくメトリクスは形式化の実際の品質を著しく過大評価し、このシグナルのみに依存する評価プロトコルの信頼性に疑問を投げかける。

3つの組織的な失敗パターン

エージェントパイプラインはコンパイルが捕捉しない3つの繰り返すエラーパターンを示した。

定理を弱体化する追加された仮説。 エージェントは元の定理が持たない追加の仮定を持つ定理を定式化する。文はその仮定の範囲内では技術的に正しい――しかしより弱い主張を証明する。例えば、数値的手法の収束に関する一般的な定理が正の係数を持つ特殊ケースに制限される可能性があり、Leanはそれを受理するが研究者は受理しない。

複数部分の文の不完全なカバレッジ。 定理に複数の結論やケースがある場合、エージェントは一部のみを形式化する可能性がある。Leanはそれを有効だが部分的な形式化として受理する。元の定理のカバレッジは検証器からの診断メッセージなしに不完全なままだ。

ファントムインポート。 エージェントは存在しないか異なるエクスポート名を持つMathlib定義や補題を参照する。特定のコンテキストでLeanはこのようなインポートを容認したり部分的に解決したりし、カーネルを通じてエラーを通過させ、有効性の誤った印象を残す。

3次元品質フレームワーク

対応として、著者たちは受理か拒否かのバイナリアプローチを超える3次元評価フレームワークを提案する。

第1の次元は意味論的正確性――形式化された文がカーネルの確認とは無関係に教科書の元の定理の意味論に対応するか。第2はMathlibの再利用――エージェントが既に証明された主張を再発明するのではなく、Mathlibライブラリの既存の定義、補題、構造を使用するか。第3はファイル間の再利用――定義がプロジェクトの異なるファイル全体で一貫しているか、論理的な穴を隠蔽する矛盾したペアが存在するか。

3つの次元はすべてLLM-as-judgeアプローチによって評価される――再現可能でスケーラブルな自動評価だ。フレームワークはこの特定のパイプラインだけでなく、将来のエージェント形式化システムにも適用できるよう設計されている。

AIコーディングベンチマークへのより広い影響

この研究は形式的な数学をはるかに超えた影響を持つ。コンパイルを成功の主要なシグナルとして使用することは、標準的なソフトウェアのAIコーディングエージェントの評価でも採用されている――HumanEvalやSWE-benchのようなベンチマークは正確性のプロキシとしてテストの通過に依存している。

同じ問題がそこにも存在するなら――テストには通過するが意味論的に弱体化されたか部分的に正確な実装を生成するエージェント――標準的なAIコーディングベンチマークは品質シグナルとして不十分だ。この研究は実際の形式化プロジェクトでカタログ化された具体的なエラーパターンによって裏付けられた、その懸念への形式的な議論を提供する。

重要なコードの記述や検証のためにAIエージェントを展開するチームにとって、重要なメッセージは明確だ：コンパイルの確認とテストの通過は正確性の必要だが十分でない指標だ。意味論的評価――どれほど高価で自動化が難しくても――は避けられないステップであり続ける。