論文の概要: LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks

• arxiv url: http://arxiv.org/abs/2606.03303v2
• Date: Wed, 03 Jun 2026 06:16:05 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-04 13:59:43.535361
• Title: LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks
• Title（参考訳）: LEAP: エージェントフレームワークによる形式数学用LLMのスーパーチャージ
• Authors: Po-Nien Kung, Linfeng Song, Dawsen Hwang, Jinsung Yoon, Chun-Liang Li, Simone Severini, Mirek Olšák, Edward Lockhart, Quoc V Le, Burak Gokturk, Thang Luong, Tomas Pfister, Nanyun Peng,
• Abstract要約: 大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。 本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
• 参考スコア（独自算出の注目度）: 85.86474267842907
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large Language Models (LLMs) exhibit strong informal mathematical reasoning but struggle to generate mechanically verifiable proofs in formal languages like Lean. We present LEAP, an agentic framework that enables general-purpose foundation models to achieve state-of-the-art performance on automated formal theorem proving. LEAP leverages foundation model capabilities, such as informal reasoning, instruction following, and iterative self-refinement. By decomposing complex problems into smaller units, the system bridges formal proof construction with informal blueprints through continuous interaction with the Lean compiler. To provide a rigorous evaluation beyond increasingly saturated benchmarks, we introduce Lean-IMO-Bench, a benchmark of IMO-style problems formalized in Lean, with short statements yet highly non-routine and multi-step proofs across a wide range of difficulty levels. Empirically, on the latest 2025 Putnam Competition, an annual mathematics competition for undergraduate students in North America, LEAP solves all 12 problems, matching recent breakthroughs by frontier formal mathematical models. On Lean-IMO-Bench, LEAP boosts the one-shot formal solve rate of general-purpose LLMs from below 10% to 70%, notably surpassing the 48% benchmark set by a specialized, gold-medal-caliber IMO system. Furthermore, we demonstrate LEAP's research-level utility by autonomously formalizing complex proofs for open combinatorial challenges, including a verified proof for a key subproblem in Knuth's Hamiltonian decomposition of even-order Cayley graphs.
• Abstract（参考訳）: 大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で機械的に検証可能な証明を生成するのに苦労している。 本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。 LEAPは、非公式な推論、命令フォロー、反復的な自己修正などの基礎モデル機能を活用する。 複雑な問題を小さなユニットに分解することで、システムはリーンコンパイラとの継続的な相互作用を通じて非公式な青写真で形式的な証明構造を橋渡しします。 飽和度の高いベンチマークを超えて厳密な評価を行うため、リーンで形式化されたIMOスタイルの問題のベンチマークであるLean-IMO-Benchを紹介します。 2025年、北米の大学生を対象とした毎年恒例の数学コンペティションであるパットナム・コンペティションで、LEAPは12の問題を全て解決し、フロンティアの公式な数学的モデルによる最近のブレークスルーと一致する。 Lean-IMO-Benchでは、LEAPが1ショットの汎用LLMの正式な解決率を10%以下から70%に引き上げている。 さらに、開組合せ問題に対する複素証明を自律的に形式化し、クヌースの等階ケイリーグラフのハミルトン分解における鍵部分確率の証明を含むLEAPの研究レベルユーティリティを実証する。

関連論文リスト

• LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories) [7.871706113805829]
  LeanCatは、カテゴリ理論の形式化のためのリーンベンチマークである。 パート I: 1-カテゴリには、完全に形式化されたステートメントレベルのタスクが100個含まれています。 Part II: LeanBridgeはLeanExploreを使ってMathlibを検索し、単一モデルベースラインに対する一貫した利得を観察します。
  論文  参考訳（メタデータ） (2025-12-31T11:33:29Z)
• FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory [44.64175433092553]
  大規模言語モデル (LLM) は、最近、形式定理の証明において顕著な進歩を見せている。 しかし、数学者の実践的なアシスタントとして機能する能力は、複雑な証明の中で欠落したステップを埋めるものであり、まだ解明されていない。 機械学習の基礎理論に基づいて構築された、リーン4ベンチマークであるFormalMLを紹介します。
  論文  参考訳（メタデータ） (2025-09-26T14:40:14Z)
• 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)
• 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)
• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
  我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。 まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。 次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。 最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
  論文  参考訳（メタデータ） (2025-02-11T15:27:35Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)

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

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