論文の概要: MiniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification

• arxiv url: http://arxiv.org/abs/2512.10187v1
• Date: Thu, 11 Dec 2025 00:52:19 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-12 16:15:42.138162
• Title: MiniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification
• Title（参考訳）: MiniF2F-Dafny: オートアクティベーションによるLCM誘導数理理論証明
• Authors: Mantas Baksys, Stefan Zetzsche, Olivier Bouissou,
• Abstract要約: 数学的推論ベンチマーク miniF2F の最初の翻訳である miniF2F-Dafny を自動定理証明器に提示する。 Dafnyの自動化はテストセットの99/244 (40.6%) と検証セットの109/244 (44.7%) を空の証明で検証する。
• 参考スコア（独自算出の注目度）: 0.5753241925582828
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present miniF2F-Dafny, the first translation of the mathematical reasoning benchmark miniF2F to an automated theorem prover: Dafny. Previously, the benchmark existed only in interactive theorem provers (Lean, Isabelle, HOL Light, Metamath). We find that Dafny's automation verifies 99/244 (40.6%) of the test set and 109/244 (44.7%) of the validation set with empty proofs--requiring no manual proof steps. For problems where empty proofs fail, we evaluate 12 off-the-shelf LLMs on providing proof hints. The best model we test achieves 55.7% pass@4 success rate employing iterative error correction. These preliminary results highlight an effective division of labor: LLMs provide high-level guidance while automation handles low-level details. Our benchmark can be found on GitHub at http://github.com/dafny-lang/miniF2F .
• Abstract（参考訳）: 数学的推論ベンチマーク miniF2F の最初の翻訳である miniF2F-Dafny を自動定理証明器 Dafny に提示する。 以前は、このベンチマークはインタラクティブな定理証明者(Lean, Isabelle, HOL Light, Metamath)にしか存在しなかった。 Dafnyの自動化は、テストセットの99/244 (40.6%) と、空の証明を持つ検証セットの109/244 (44.7%) を検証している。 空の証明が失敗する問題に対しては,12個の既製のLCMを証明ヒントとして評価する。 私たちがテストした最良のモデルは、反復的エラー訂正を用いた55.7%のパス@4成功率を達成する。 LLMは、自動化が低レベルの詳細を処理している間に、高レベルガイダンスを提供する。 私たちのベンチマークはGitHubのhttp://github.com/dafny-lang/miniF2Fで確認できます。

関連論文リスト

• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [16.8655558789989]
  本稿では,自動定理証明のためのモデルに依存しないエージェントフレームワークであるAPOLLO (Automated PrOof repair viaLLM and Lean cOllaboration)を提案する。 エージェントのセットは、証明を分析し、シンタックスのエラーを修正し、リーンを使って証明の誤りを特定し、失敗するサブレムマを分離し、自動化されたソルバを利用し、残りの目標に対してLLMを呼び出す。 この結果から,LLM出力を目標としたコンパイラ誘導型修復は,効率と正確性の両方において劇的に向上することが示された。
  論文  参考訳（メタデータ） (2025-05-09T03:38:31Z)
• ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。 本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。 また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
  リーンでLLM推論を実行するためのフレームワークであるLean Copilotを紹介します。 証明のステップを提案し、証明の目標を完了し、関連する前提を選択するツールを構築します。 人間を助ける場合、Lean Copilotは平均3.86で手動で入力された証明ステップを2.08ステップしか必要としない。 定理証明プロセスを自動化する場合、Lean Copilotの74.2%の証明ステップは平均85%がエソップ(40.1%)より優れている。
  論文  参考訳（メタデータ） (2024-04-18T22:54:08Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。