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

• arxiv url: http://arxiv.org/abs/2506.19923v1
• Date: Tue, 24 Jun 2025 18:01:52 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-06-26 21:00:42.495668
• 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ベンチマークで86.1%の成功率を達成した。
• 参考スコア（独自算出の注目度）: 6.598148515720521
• 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 to assist in discovering the overall proof strategy. It achieves an 86.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 case studies illustrating how these generated lemmas contribute to solving challenging problems.
• Abstract（参考訳）: 本稿では,大規模言語モデル(LLM)と公式な証明アシスタントであるLeanを統合した,自動定理証明のための新しいAIエージェントであるProver Agentを紹介する。 Prover Agentは、非公式な推論 LLM、フォーマルな証明モデル、リーンからのフィードバックをコーディネートするとともに、全体的な証明戦略の発見を支援する補助的なレムマを生成する。 MiniF2Fベンチマークで86.1%の成功率を実現し、従来のアプローチよりもはるかに低いサンプル予算でSLM(Small Language Model)を用いた新しい最先端の手法を確立した。 また、これらの生成した補題が課題解決にどのように貢献するかを示すケーススタディも提示する。

関連論文リスト

• 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)
• 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)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。 我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。 我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
  論文  参考訳（メタデータ） (2023-10-16T08:42:39Z)

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

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