論文の概要: 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で確認できます。

関連論文リスト

• HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement [7.702809989052384]
  HybridProverは、戦術ベースの生成と全防御合成を組み合わせたデュアルモデル証明フレームワークである。 最適化されたデータセット上にIsabelle定理証明器とファインチューンLPMにHybridProverを実装した。
  論文  参考訳（メタデータ） (2025-05-21T16:45:43Z)
• 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)
• STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving [33.61458249318183]
  セルフプレイ・セオレム・プロバー(STP)は、予想と証明という2つの役割を担っている。 STPは同時に、予想と証明という2つの役割を担っている。 私たちはLeanとIsabelleの2つの形式的検証ツールで評価します。
  論文  参考訳（メタデータ） (2025-01-31T23:01:48Z)
• 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)
• InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search [65.05674971652776]
  代表的な証明法は、証明手法を戦術によって反復的に構築することであり、典型的には最優先の探索スキームに従う。 本稿では,評価モデルを用いて選好情報を抽出する直感的かつ効果的な手法を提案する。 2万日以上のCPUを持つ大規模なエキスパートイテレーションが、証明者と批判者をさらに微調整するために適用される。
  論文  参考訳（メタデータ） (2024-10-21T07:18:23Z)
• Inference-Time Decontamination: Reusing Leaked Benchmarks for Large Language Model Evaluation [61.350306618479365]
  ベンチマークの漏洩は、大規模言語モデルの真のパフォーマンスの正確な評価を防ぐことができる。 この問題に対処するため,ITD(Inference-Time Decontamination)を提案する。 ITDは、GSM8Kで22.9%、MMLUで19.0%の膨張精度を低下させる。
  論文  参考訳（メタデータ） (2024-06-20T04:35:59Z)
• 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)
• Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method [1.8130068086063336]
  本稿では,定理証明のための新しい動的サンプリング手法であるDS-Proverを紹介する。 単純化と書き直しの戦術を複数の前提で1つの前提で戦術に分解することで、トレーニングデータセットを強化します。 ProofNetデータセットでは14.2%の最先端パフォーマンス(Pass@1)、MiniF2Fでは29.8%のパフォーマンスを実現しています。
  論文  参考訳（メタデータ） (2023-12-20T09:55:21Z)
• LLMs as Factual Reasoners: Insights from Existing Benchmarks and Beyond [135.8013388183257]
  そこで我々は,SummEditsと呼ばれる10ドメインのベンチマークで不整合検出ベンチマークを作成し,実装する新しいプロトコルを提案する。 ほとんどのLLMはSummEditsで苦労しており、パフォーマンスはランダムに近い。 最も優れたモデルであるGPT-4は、推定された人間のパフォーマンスよりも8%低い。
  論文  参考訳（メタデータ） (2023-05-23T21:50:06Z)

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

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