Meta AIは2026年10月13日、AIエージェントがLean 4で高度な数学を形式化できるかを測るベンチマーク「AutoformBench」を公開しました。24の高度な数学資料から集めた341課題を収録しています。Leanに詳しい数学者が各目標命題を形式化して監査し、評価対象のエージェントはLeanの証明を作成します。

個別の定理証明テストとは異なり、AutoformBenchの各課題は、より広い数学的な展開の中に位置づけられています。エージェントには非形式的な証明が与えられ、それをLeanに翻訳するとともに、結果を形式化されたライブラリにつなぐために必要な定義、中間補題、補助的な基盤を補います。著者らによると、既存の評価では、支援理論の多くがすでにMathlibにある状況で定理の命題が提示されることがよくあります。

研究者らが最先端モデルを比較したところ、数学分野をまたいで難易度の境界はおおむね共通していました。成績は対象分野よりも、不足する形式的な基盤をモデルが構築できるかどうかに左右されたといいます。データセットとコードはGitHubで公開されています。

Meta AIは2026年10月13日、AIエージェントがLean 4で高度な数学を形式化できるかを測るベンチマーク「AutoformBench」を公開しました。24の高度な数学資料から集めた341課題を収録しています。Leanに詳しい数学者が各目標命題を形式化して監査し、評価対象のエージェントはLeanの証明を作成します。

個別の定理証明テストとは異なり、AutoformBenchの各課題は、より広い数学的な展開の中に位置づけられています。エージェントには非形式的な証明が与えられ、それをLeanに翻訳するとともに、結果を形式化されたライブラリにつなぐために必要な定義、中間補題、補助的な基盤を補います。著者らによると、既存の評価では、支援理論の多くがすでにMathlibにある状況で定理の命題が提示されることがよくあります。

研究者らが最先端モデルを比較したところ、数学分野をまたいで難易度の境界はおおむね共通していました。成績は対象分野よりも、不足する形式的な基盤をモデルが構築できるかどうかに左右されたといいます。データセットとコードはGitHubで公開されています。