論文の概要: FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
- arxiv url: http://arxiv.org/abs/2603.26996v1
- Date: Fri, 27 Mar 2026 21:14:53 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-03-31 23:18:44.726576
- Title: FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
- Title（参考訳）: FormalProofBench: モデルでは、形式的に検証されたレベル数学の証明を書けるか?
- Abstract要約: 本稿では、AIモデルが正式に検証された数学的証明を生成できるかどうかを評価するために設計されたプライベートベンチマークであるFormalProofBenchを紹介する。
各タスクは、自然言語とLean4の形式的なステートメントをペアリングし、モデルはLean 4チェッカーが受け入れるリーンの証明を出力する必要があります。
エージェントハーネスを用いたフロンティアモデルの評価を行い,最も優れた基礎モデルが33.5%の精度で達成できることを見出した。
- 参考スコア（独自算出の注目度）: 0.04324039930655099
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We present FormalProofBench, a private benchmark designed to evaluate whether AI models can produce formally verified mathematical proofs at the graduate level. Each task pairs a natural-language problem with a Lean~4 formal statement, and a model must output a Lean proof accepted by the Lean 4 checker. FormalProofBench targets advanced undergraduate and graduate mathematics, with problems drawn from qualifying exams and standard textbooks across topics including analysis, algebra, probability, and logic. We evaluate a range of frontier models with an agentic harness, and find that the best-performing foundation model achieves 33.5% accuracy, with performance dropping rapidly after that. In addition to the accuracy numbers, we also provide empirical analysis of tool-use, failure modes, cost and latency, thereby providing a thorough evaluation of the formal-theorem proving abilities of frontier models.
- Abstract（参考訳）: 我々は、AIモデルが卒業レベルで正式に検証された数学的証明を作成できるかどうかを評価するために設計されたプライベートベンチマークであるFormalProofBenchを提案する。
各タスクは、Lean～4の形式的なステートメントと自然言語の問題をペアリングし、モデルはLean 4チェッカーが受け入れるリーンの証明を出力する必要があります。
FormalProofBenchは、高度な学部と大学院の数学を対象とし、分析、代数、確率、論理などを含む分野にわたる資格試験と標準教科書から引き出された問題がある。
エージェントハーネスを用いたフロンティアモデルの評価を行い、最適性能の基礎モデルが33.5%の精度で達成され、その後性能は急速に低下した。
また, ツール使用, 障害モード, コスト, レイテンシの実験的解析を行い, フロンティアモデルの形式的理論実証能力を徹底的に評価する。
関連論文リスト
- MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize [38.37332307303914]
MathAdvは、学部および大学院レベルの数学で13のドメインにまたがる診断ベンチマークである。
本稿では, 定理証明精度が不明瞭であるモデル機能と故障モードを, コンポーネント単位で評価することで明らかにする方法について述べる。
論文 参考訳（メタデータ） (2026-08-26T07:12:54Z) - MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
MathCoPilotは、数学研究のための新しいAI共生パラダイムを具現化したループシステムである。
MathCoPilotは3つのコア機能を統合する: 証明をナビゲート可能なステップに分解するインタラクティブな証明青写真、適応的な知識ベース検索とリーン統合された反復検証を備えた自動証明スキルオーケストレーション、トピック駆動の紙検索と自動形式化を検証可能なリーン知識ベースに統合する。
論文 参考訳（メタデータ） (2026-07-16T05:22:40Z) - AdvancedMathBench: A Benchmark Suite for Advanced Mathematical Proof Generation and Verification [41.90353470982016]
大型言語モデル (LLM) は、高校やオリンピックスタイルの数学において顕著な性能を発揮している。
既存のベンチマークはスコープと評価の粒度の両方で不足している。
本稿では,高度な数学的推論能力を評価するためのベンチマークスイートであるAdvancedMathBenchを紹介する。
論文 参考訳（メタデータ） (2026-07-13T17:38:22Z) - LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。
本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
論文 参考訳（メタデータ） (2026-06-02T08:16:42Z) - LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
研究レベルの数学的推論のための動的多重選択ベンチマークであるLiveMathematicianBenchを提案する。
新たに発表された定理で評価を基礎づけることで、記憶されたパターンを超えた現実的なテストベッドを提供する。
このパイプラインは、高レベルな証明戦略を使用して、妥当だが無効な解選択を構築する。
論文 参考訳（メタデータ） (2026-04-02T08:22:17Z) - Mathematical Proof as a Litmus Test: Revealing Failure Modes of Advanced Large Reasoning Models [11.250861762443801]
RFMDataset(Reveal Failure Modes)は200種類の数学的証明問題の集合である。
先進モデルの性能を徹底的に評価する。
解析により,現在の大規模推論モデルの基本的制約を示す10種類のきめ細かい誤差型が明らかになった。
論文 参考訳（メタデータ） (2025-06-20T16:14:18Z) - Enumerate-Conjecture-Prove: Formally Solving Answer-Construction Problems in Math Competitions [39.102692814217086]
LLMは難解な解答作業に対処できるが、幻覚や不可解なステップの誤りを生じやすい。
創造性と数学的厳密性の両方を保ちながら、どのように解答-構成問題を解決するか?
本稿では,パターン駆動型推論と形式的定理証明を統合したニューロシンボリックな手法であるLLM-Conjecture-Prove(ECP)フレームワークを紹介する。
ConstructiveBenchでは、ECPは33.1%の最先端の精度(32.5%から)を達成し、公式な数学的推論を前進させる可能性を示している。
論文 参考訳（メタデータ） (2025-05-24T03:52:25Z) - Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。
我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。
我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
論文 参考訳（メタデータ） (2024-11-04T05:57:40Z) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z) - DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。
この合成データセットでDeepSeekMath 7Bモデルを微調整します。
我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
論文 参考訳（メタデータ） (2024-05-23T09:03:42Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳（メタデータ） (2024-02-14T05:57:58Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。