論文の概要: Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics

• arxiv url: http://arxiv.org/abs/2510.12787v1
• Date: Tue, 14 Oct 2025 17:57:04 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-15 19:02:32.437587
• Title: Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics
• Title（参考訳）: Ax-Prover:数学と量子物理学の定理証明のためのディープ推論エージェントフレームワーク
• Authors: Marco Del Tredici, Jacob McCarran, Benjamin Breen, Javier Aspuru Mijares, Weichen Winston Yin, Jacob M. Taylor, Frank Koppens, Dirk Englund,
• Abstract要約: Ax-Proverは、リーンにおける自動定理証明のためのマルチエージェントシステムである。 様々な科学的領域にまたがる問題を解決し、自律的または協調的に人間の専門家と操作することができる。 我々は,2つの公的な数学ベンチマークと,抽象代数学と量子論の分野において導入される2つのリーンベンチマークにおいて,フロンティア LLM と特殊証明モデルに対するアプローチをベンチマークする。
• 参考スコア（独自算出の注目度）: 1.2978846076301875
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We present Ax-Prover, a multi-agent system for automated theorem proving in Lean that can solve problems across diverse scientific domains and operate either autonomously or collaboratively with human experts. To achieve this, Ax-Prover approaches scientific problem solving through formal proof generation, a process that demands both creative reasoning and strict syntactic rigor. Ax-Prover meets this challenge by equipping Large Language Models (LLMs), which provide knowledge and reasoning, with Lean tools via the Model Context Protocol (MCP), which ensure formal correctness. To evaluate its performance as an autonomous prover, we benchmark our approach against frontier LLMs and specialized prover models on two public math benchmarks and on two Lean benchmarks we introduce in the fields of abstract algebra and quantum theory. On public datasets, Ax-Prover is competitive with state-of-the-art provers, while it largely outperform them on the new benchmarks. This shows that, unlike specialized systems that struggle to generalize, our tool-based agentic theorem prover approach offers a generalizable methodology for formal verification across diverse scientific domains. Furthermore, we demonstrate Ax-Prover's assistant capabilities in a practical use case, showing how it enabled an expert mathematician to formalize the proof of a complex cryptography theorem.
• Abstract（参考訳）: 私たちはAx-Proverを紹介します。Ax-Proverはリーンで証明された自動定理のためのマルチエージェントシステムです。 これを達成するために、Ax-Proverは、創造的な推論と厳密な構文的厳密さの両方を要求する形式的証明生成を通じて、科学的な問題解決にアプローチする。 Ax-Proverは、知識と推論を提供するLarge Language Models (LLMs) と、正式な正当性を保証する Model Context Protocol (MCP) を通じてリーンツールを備えることで、この課題に対処する。 自律型証明器としての性能を評価するため,2つの公的な数学ベンチマークと,抽象代数学と量子論の分野に導入する2つのリーンベンチマークにおいて,フロンティア LLM と特殊証明モデルに対する我々のアプローチをベンチマークした。 公開データセットでは、Ax-Proverは最先端のプロバーと競合するが、新しいベンチマークでは大きく上回っている。 このことは、一般化に苦しむ専門的なシステムとは異なり、ツールベースのエージェント的定理証明手法が、様々な科学的領域にわたる形式的検証のための一般化可能な方法論を提供することを示している。 さらに,Ax-Proverのアシスタント機能を実例で実証し,それが複雑な暗号定理の証明の形式化を可能にしたことを示す。

関連論文リスト

• 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)
• Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs [11.87831709160905]
  本稿では,自動定理証明のためのAIエージェントであるProver Agentを紹介する。 大規模な言語モデル(LLM)と公式な証明アシスタントであるLeanを統合している。 MiniF2Fベンチマークで88.1%の成功率を達成した。
  論文  参考訳（メタデータ） (2025-06-24T18:01:52Z)
• From Axioms to Algorithms: Mechanized Proofs of the vNM Utility Theorem [0.0]
  我々は、選好完全性、推移性、連続性、独立性の古典的な公理を実践する。 我々の定式化は、宝くじに対する嗜好関係の数学的構造を捉えている。 この形式化は、経済モデリング、AIアライメント、管理決定システムにおける応用のための厳格な基盤を提供する。
  論文  参考訳（メタデータ） (2025-06-08T10:09:54Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。 DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。 我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
  論文  参考訳（メタデータ） (2025-05-29T17:59:39Z)
• One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs [75.95179490687018]
  証明生成のための数学的大規模言語モデルを活用することは、LLM研究の基本的なトピックである。 現状のLCMが証明できる能力は、学習中に関連する証明プロセスに遭遇したかどうかに大きく依存していると論じる。 人間の数学教育で一般的に用いられる「反例による防御」の教育的手法に触発されて,我々の研究は,反例を通して数学的推論と証明を行うLLMの能力を高めることを目的としている。
  論文  参考訳（メタデータ） (2025-02-12T02:01:10Z)
• LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
  フォーマルな定理証明のための新しい生涯学習フレームワークであるLeanAgentを紹介する。 LeanAgentは継続的に一般化し、拡張可能な数学的知識を改善します。 これは23のリーンリポジトリにわたる155の定理の正式な証明を生成する。
  論文  参考訳（メタデータ） (2024-10-08T17:11:24Z)

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

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