論文の概要: Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs

• arxiv url: http://arxiv.org/abs/2506.19923v3
• Date: Mon, 29 Sep 2025 16:01:54 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-30 17:47:09.070024
• Title: Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs
• Title（参考訳）: Prover Agent:フォーマルな数学的証明のためのエージェントベースのフレームワーク
• Authors: Kaito Baba, Chaoran Liu, Shuhei Kurita, Akiyoshi Sannai,
• Abstract要約: 本稿では,自動定理証明のためのAIエージェントであるProver Agentを紹介する。 大規模な言語モデル(LLM)と公式な証明アシスタントであるLeanを統合している。 MiniF2Fベンチマークで88.1%の成功率を達成した。
• 参考スコア（独自算出の注目度）: 11.87831709160905
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We present Prover Agent, a novel AI agent for automated theorem proving that integrates large language models (LLMs) with a formal proof assistant, Lean. Prover Agent coordinates an informal reasoning LLM, a formal prover model, and feedback from Lean while also generating auxiliary lemmas. These auxiliary lemmas are not limited to subgoals in the formal proof but can also include special cases or potentially useful facts derived from the assumptions, which help in discovering a viable proof strategy. It achieves an 88.1% success rate on the MiniF2F benchmark, establishing a new state-of-the-art among methods using small language models (SLMs) with a much lower sample budget than previous approaches. We also present theoretical analyses and case studies that illustrate how these generated lemmas contribute to solving challenging problems.
• Abstract（参考訳）: 本稿では,大規模言語モデル(LLM)と公式な証明アシスタントであるLeanを統合した,自動定理証明のための新しいAIエージェントであるProver Agentを紹介する。 Prover Agentは、非公式な推論 LLM、フォーマルな証明モデル、リーンからのフィードバックをコーディネートし、補助的な補題を生成する。 これらの補助補題は形式的証明のサブゴールに限らず、仮定から派生した特別なケースや潜在的に有用な事実も含み得る。 MiniF2Fベンチマークで88.1%の成功率を実現し、従来のアプローチよりもはるかに低いサンプル予算でSLM(Small Language Model)を用いた新しい最先端の手法を確立した。 また、これらの生成した補題が課題解決にどのように貢献するかを示す理論的分析とケーススタディも提示する。

関連論文リスト

• Solving Formal Math Problems by Decomposition and Iterative Reflection [30.54275542622631]
  textbfDelta Proverは汎用LLMとLean 4の実証環境とのインタラクションを編成します。 bftextDelta Proverは、miniF2F-testベンチマークで、最先端の95.9%の成功率を達成した。
  論文  参考訳（メタデータ） (2025-07-21T03:56:35Z)
• Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving [48.22540519786074]
  最近の研究では、非公式な精度は80%を超え、公式な成功はPutnamBenchのようなベンチマークで8%以下である。 低レベルの証明生成から高レベルの推論を分離する新しいフレームワークを提案する。 提案手法は,2000年以降のIMO問題に対して,従来のオープンソース証明者が未報告の課題として評価した。
  論文  参考訳（メタデータ） (2025-07-07T22:38:49Z)
• Distilling LLM Agent into Small Models with Retrieval and Code Tools [57.61747522001781]
  Agent Distillationは、推論能力とタスク解決の振る舞いを大きな言語モデルから小さな言語モデルに移行するためのフレームワークである。 その結果,SLMは0.5B,1.5B,3Bのパラメータで,次世代の1.5B,3B,7Bモデルと競合する性能が得られることがわかった。
  論文  参考訳（メタデータ） (2025-05-23T08:20:15Z)
• Towards Reliable Proof Generation with LLMs: A Neuro-Symbolic Approach [14.213719696233934]
  大型言語モデル(LLM)は厳密な論理的推論と記号的推論を必要とする形式的ドメインと競合する。 本稿では,LLMの生成強度と構造成分を組み合わせ,この課題を克服するニューロシンボリックアプローチを提案する。
  論文  参考訳（メタデータ） (2025-05-20T15:13:32Z)
• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [8.056359341994941]
  APOLLOは、Leanコンパイラの強みとLLMの推論能力を組み合わせた、モデルに依存しないパイプラインである。 miniF2Fベンチマークでは、新しい最先端精度75.0%が確立されている。
  論文  参考訳（メタデータ） (2025-05-09T03:38:31Z)
• BRiTE: Bootstrapping Reinforced Thinking Process to Enhance Language Model Reasoning [78.63421517563056]
  大規模言語モデル(LLM)は複雑な推論タスクにおいて顕著な機能を示した。 本稿では,新しいグラフィカルモデルを用いてLLM推論を定式化する統一確率的フレームワークを提案する。 本稿では,Bootstrapping Reinforced Thinking Process (BRiTE)アルゴリズムについて述べる。
  論文  参考訳（メタデータ） (2025-01-31T02:39:07Z)
• 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)
• Textualized Agent-Style Reasoning for Complex Tasks by Multiple Round LLM Generation [49.27250832754313]
  我々は、llmベースの自律エージェントフレームワークであるAgentCOTを紹介する。 それぞれのステップで、AgentCOTはアクションを選択し、それを実行して、証拠を裏付ける中間結果を得る。 エージェントCOTの性能を高めるための2つの新しい戦略を導入する。
  論文  参考訳（メタデータ） (2024-09-19T02:20:06Z)
• Enhancing the General Agent Capabilities of Low-Parameter LLMs through Tuning and Multi-Branch Reasoning [56.82041895921434]
  オープンソースの事前訓練された大規模言語モデル(LLM)は、強力な言語理解と生成能力を示す。 現実世界の複雑な問題に対処するエージェントとして使用される場合、ChatGPTやGPT-4のような大型の商用モデルに比べてパフォーマンスははるかに劣る。
  論文  参考訳（メタデータ） (2024-03-29T03:48:12Z)
• Let's Reinforce Step by Step [10.65244642965387]
  人間のフィードバックからの強化学習をモデル推論の形式化に活用する。 以上の結果から, PRM法により得られる微粒な報酬は, 単純な数学的推論の精度を高めることが示唆された。 また、モデル性能において、報酬アグリゲーション関数が果たす重要な役割を示す。
  論文  参考訳（メタデータ） (2023-11-10T01:35:51Z)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。 我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。 我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
  論文  参考訳（メタデータ） (2023-10-16T08:42:39Z)
• Autoformalization with Large Language Models [22.86710743804944]
  自動形式化システムの成功は、形式検証、プログラム合成、人工知能の分野を前進させる可能性がある。 大規模な言語モデルがこの目標に向けて新たな展望を提供することを示す。 我々の手法はMiniF2F定理証明ベンチマークで新たな最先端結果をもたらし、証明レートを29.6%から35.2%に改善した。
  論文  参考訳（メタデータ） (2022-05-25T09:53:30Z)

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

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