論文の概要: LAMP: Lean-based Agentic framework with MCP and Proof Repair
- arxiv url: http://arxiv.org/abs/2606.28841v1
- Date: Sat, 27 Jun 2026 09:58:09 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-30 18:07:15.703285
- Title: LAMP: Lean-based Agentic framework with MCP and Proof Repair
- Title（参考訳）: LAMP: MCPとProofによるリーンベースのエージェントフレームワーク
- Abstract要約: LAMPは、推論時に明示的に構造化されたドメイン知識を提供することで、カーネル検証されたLean 4証明を合成するフレームワークです。
LAMPは96.7%の定理の証明証明を合成し、未スケールのベースラインと既存の特殊プローバーをほぼ超えている。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Large language models are increasingly capable of mathematical reasoning, but the proofs they generate are often unreliable and hard to verify. Interactive theorem provers such as Lean 4 address this by accepting only kernel-checked proofs; however, their reach is bounded by the formalized knowledge available. While Mathlib, a repository of formalized Lean 4 theorems that covers diverse mathematical areas, certain specialized areas remain underrepresented; notably, the domain of Combinatorics on Words (CoW). CoW studies sequences, exploring their properties such as periodicity, borders, conjugacy, and morphisms. As a result, specialized provers, trained on Mathlib-centered data, lack the lemmas to operate in CoW. We present two contributions. First, we introduce a Lean 4 formalization of CoW containing eight modules and \textbf{93} declarations of core definitions and foundational lemmas. Second, we present LAMP, a multi-agent framework that synthesizes kernel-verified Lean 4 proofs by providing explicit, structured domain knowledge at inference time through an ontology, rather than by fine-tuning a prover. LAMP coordinates a Planner, Builder, and Verifier with Model Context Protocol based access to a domain-specific CoW ontology. In a suite of 90 CoW theorems that span all eight modules and three difficulty levels, LAMP synthesizes verified proofs for 96.7% of theorems, substantially exceeding both an unscaffolded baseline and existing specialized provers. An ablation shows that removing LAMP's tool-grounded architecture or its Planner/Builder separation each cost roughly 12 percentage points, even with the backbone model held fixed.
- Abstract（参考訳）: 大規模言語モデルは、数学的推論がますます可能になっているが、それらが生成する証明はしばしば信頼性が低く、検証が難しい。
Lean 4のようなインタラクティブな定理証明者は、カーネルチェックされた証明のみを受け入れることでこの問題に対処するが、それらの到達範囲は利用可能な形式化された知識によって制限される。
Mathlibは、様々な数学領域をカバーする形式化されたLean 4定理のリポジトリであるが、特定の専門分野はいまだ少数派であり、特に Combinatorics on Words (CoW) の領域である。
CoWは、周期性、境界、共役性、および射などのそれらの性質を探索する。
その結果、Mathlib中心のデータに基づいて訓練された特殊プローバーは、CoWで運用するレムマを欠いている。
コントリビューションは2つです。
まず、8つのモジュールとコア定義と基本補題の‘textbf{93}宣言を含むCoWのLean 4形式化を紹介します。
第二に、LAMPは、証明子を微調整するのではなく、オントロジーを通して推論時に明示的で構造化されたドメイン知識を提供することにより、カーネル検証されたLean 4証明を合成するマルチエージェントフレームワークである。
LAMPは、Planner、Builder、VerifierとModel Context Protocolをベースとしたドメイン固有のCoWオントロジーへのアクセスをコーディネートする。
8つの加群と3つの難解レベルにまたがる90のCoW定理のスイートにおいて、LAMPは96.7%の定理の証明証明を合成し、非スキャフォールド基底線と既存の特殊プローバーをほぼ超えている。
アブレーションによると、LAMPのツール基底アーキテクチャやPlanner/Builder分離の除去は、バックボーンモデルが固定されている場合でも、それぞれ約12パーセントのコストがかかる。
関連論文リスト
- MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4 [5.103695715197289]
本稿では,真正な自己形式化とユークリッド幾何学の証明構築を共同で扱うMathlibネイティブエージェントフレームワークであるMechGeoを紹介する。
GeoFormalizerはGeoIRの非公式な問題を表し、決定論的にそれらをLean 4に翻訳し、候補ステートメントを反復的に修復する。
GeoProverは幾何学的証明計画を構築し、中間補題を導出し、Leanで検証されたライブラリを通して適切なサブゴールを選択的に代数化する。
論文 参考訳（メタデータ） (2026-08-03T14:24:12Z) - Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics [20.90238876313568]
大きな言語モデル(LLM)は、人間の検出を避ける微妙なエラーを生成する。
最近の傾向は、汎用LLMがリーンのために明確に調整されたより小さなモデルを上回っていることを示している。
汎用LLMを用いたエージェントオートフォーマル化フレームワークを提案する。
論文 参考訳（メタデータ） (2026-06-30T05:05:03Z) - ComBench: A Benchmark for Rigorous Proof Reasoning and Constructive Realization in Olympiad-Level Combinatorics [95.15900681087088]
我々は,Olympiadレベルの診断用ベンチマークであるComBenchと,大規模言語モデルの推論機能を紹介する。
ComBenchには、補完的な2つの設定で整理された100の人間注釈の競合レベルの問題が含まれている。
実験の結果、最強モデルはAvg.全体65.4%、Best@4.3%に達した。
論文 参考訳（メタデータ） (2026-06-09T06:50:15Z) - LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。
本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
論文 参考訳（メタデータ） (2026-06-02T08:16:42Z) - Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline [0.0]
我々は、ハイブリッドAI+Lean 4パイプラインとして、特許分析のための正式に検証されたフレームワークを提示します。
DAG被覆コア(Algorithm1b)は、有界マッチスコアが固定されると完全に機械検証される。
クレームは、Lean 4でDAGとしてエンコードされ、強みを検証された完全な格子の要素と一致させ、信頼スコアは、証明された正しいモノトーン関数を通じて依存関係を通じて伝播する。
論文 参考訳（メタデータ） (2026-04-20T22:02:57Z) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-11-26T06:39:19Z) - 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) - MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving [30.112351299773632]
この問題を解決するために,我々はLean4定理の包括的なフレームワークを提案する。
一般的なNLの認識タスクを完全防御生成と証明修正のための誤り解析に分離する。
我々のフレームワークは、MiniF2F-TestデータセットのLean4バージョンにおいて**61.07%*の精度を達成する。
論文 参考訳（メタデータ） (2025-03-05T05:50:31Z) - Theorem-Validated Reverse Chain-of-Thought Problem Generation for Geometric Reasoning [53.13514542825493]
TRCoT(Theorem-d Reverse Chain-of-Thought Reasoning Synthesis)フレームワークについて述べる。
最初の段階であるTR-Engineは、構造的な記述と性質を持つ定理基底幾何学図を合成する。
第2段階であるTR-Reasonerは、幾何特性と記述フラグメントを交互に検証することで、反復的に質問と回答のペアを洗練するためのリバース推論を採用している。
論文 参考訳（メタデータ） (2024-10-23T13:58:39Z) - DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。
この合成データセットでDeepSeekMath 7Bモデルを微調整します。
我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
論文 参考訳（メタデータ） (2024-05-23T09:03:42Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳（メタデータ） (2024-02-14T05:57:58Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。