要旨: 私たちは、大学院レベルにおいてAIモデルが形式的に検証された数学的証明を作成できるかどうかを評価するための、非公開ベンチマークであるFormalProofBenchを提示します。各タスクは自然言語の問題とLean~4の形式的主張を組にしており、モデルはLean 4チェッカーに受理されるLeanの証明を出力する必要があります。FormalProofBenchは、解析、代数、確率、論理を含む幅広いトピックにまたがって、資格試験の問題や標準的な教科書から出題された、上級学部生および大学院生レベルの数学を対象としています。私たちはエージェント型のハーネスを用いて多様な最先端モデルを評価し、その結果、最も高い性能を示した基盤モデルの正確さは33.5%であり、それ以降は急速に低下することが分かりました。正確さの数値に加えて、ツール使用の実証的な分析、失敗モード、コスト、レイテンシーも提供することで、最先端モデルの形式定理証明能力を徹底的に評価しています。
FormalProofBench: モデルは形式的に検証された大学院レベルの数学証明を書けるのか？
arXiv cs.AI / 2026/3/31
💬 オピニオンIdeas & Deep AnalysisModels & Research
要点
- FormalProofBenchは、自然言語の数学問題とLean 4の形式文を対応させ、モデルがLean 4チェッカーで受理される形式証明を出せるかを評価する非公開ベンチマークを提案しています。
- 対象は解析・代数・確率・論理など幅広く、上級学部から大学院レベルの問題（qualifying examsや教科書）を用いています。
- 複数の最先端基盤モデルをエージェント型の実行ハーネスで評価した結果、最高性能モデルでも正解率は33.5%にとどまり、その後は急速に低下したと報告されています。
- 精度に加えて、ツール利用状況、失敗モード、コスト、レイテンシなども分析し、形式定理証明における現状の能力と限界を包括的に示しています。
