論文の概要: LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization
- arxiv url: http://arxiv.org/abs/2606.05400v1
- Date: Wed, 03 Jun 2026 20:09:39 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-05 22:39:44.378267
- Title: LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization
- Title（参考訳）: LeanMarathon: 長期的なリーンオートモーフィゼーションを通じて、信頼性の高いAIコマンティマティクスを目指す
- Abstract要約: 信頼性の高い研究レベルのLean AutoformalizationのためのマルチエージェントハーネスであるLeanMarathonを紹介します。
4つのコントラクトスコープエージェントがこの青写真を構築し、監査し、証明し、修復する。
我々は4つのErds問題にまたがる最近の2つの研究論文でLeanMarathonを評価した。
- 参考スコア（独自算出の注目度）: 104.06650149974585
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Long-horizon autoformalization of research mathematics fails not only at hard lemmas, but at scale: statements drift, dependencies tangle, context decays, and local repairs corrupt distant work. We present LeanMarathon, a multi-agent harness for reliable research-level Lean autoformalization. Its core abstraction is an evolving blueprint: a Lean file that serves simultaneously as formal proof skeleton, natural-language proof graph, and shared system of record. Four contract-scoped agents construct, audit, prove, and repair this blueprint. These agents are coordinated by a two-stage orchestrator that first stabilizes target fidelity through adversarial review and then discharges the proof directed acyclic graph (DAG) from its dynamic leaves upward in parallel CI-gated rounds. LeanMarathon turns one brittle multi-hour run into many local, recoverable, parallel transactions. We evaluate LeanMarathon on two recent research papers spanning four Erdős problems (#1051, #1196, #164, #1217). Across three autonomous runs, it formalizes all seven target theorems with no sorry, proving 258 lemmas and theorems. These results show that reliable AI co-mathematics requires not only stronger provers, but durable harnesses that preserve target fidelity across long mathematical developments. The code can be found at https://github.com/YuanheZ/LeanMarathon.
- Abstract（参考訳）: 研究数学の長い水平自己形式化は、強硬な補題だけでなく、大規模にも失敗する。
信頼性の高い研究レベルのLean AutoformalizationのためのマルチエージェントハーネスであるLeanMarathonを紹介します。
リーンファイルは、形式的な証明スケルトン、自然言語による証明グラフ、共有された記録システムとして同時に機能します。
4つのコントラクトスコープエージェントがこの青写真を構築し、監査し、証明し、修復する。
これらのエージェントは2段階のオーケストレータによって調整され、まず対向的なレビューを通じて目標の忠実度を安定化し、次に証明指向非環状グラフ(DAG)をその動的葉から平行なCIゲートラウンドで上向きに放出する。
LeanMarathonは、脆弱な複数時間実行を多くのローカル、リカバリ可能な並列トランザクションに変換する。
我々は,4つのエルデシュ問題に関する最近の2つの研究論文(#1051,#1196,#164,#1217)でLeanMarathonを評価した。
3つの自律走行において、7つの目標定理の全てを許さずに形式化し、258の補題と定理を証明している。
これらの結果から、信頼性の高いAIコマトマティクスは、より強力なプローバーだけでなく、長期の数学的発展を通して目標の忠実性を維持するための耐久性のあるハーネスを必要とすることが示唆された。
コードはhttps://github.com/YuanheZ/LeanMarathonで見ることができる。
関連論文リスト
- MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
MathCoPilotは、数学研究のための新しいAI共生パラダイムを具現化したループシステムである。
MathCoPilotは3つのコア機能を統合する: 証明をナビゲート可能なステップに分解するインタラクティブな証明青写真、適応的な知識ベース検索とリーン統合された反復検証を備えた自動証明スキルオーケストレーション、トピック駆動の紙検索と自動形式化を検証可能なリーン知識ベースに統合する。
論文 参考訳（メタデータ） (2026-07-16T05:22:40Z) - A Formalization of the Mean-Field Derivation of the Vlasov Equation: AI-Assisted Lean Formalization as a Strategy Game [0.0]
我々は、数学者がAIシステムに指示することで、Lean 4証明アシスタントの研究結果を形式化し、そのアクティビティを形式化ゲームとしてフレーム化する。
目的は文書をリーンに変えることである。ゲームは開発がコンパイルされたときに勝利し、残念なことは含まない。マシンチェックは、目標定理がリーンの基本公理にのみ依存していることを示している。
ケーススタディは、ドブルシンの平均場経路を通した非線形ブラソフ方程式の正当性に対する完全で公理クリーンな定式化である。
論文 参考訳（メタデータ） (2026-07-09T23:17:54Z) - Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory [7.10978537067254]
Danusは、共有事実グラフを中心とした研究レベルの数学的推論のためのオーケストレーションシステムである。
検証された各事実は証明と論理的依存関係と共に格納され、システムは長い引数を構築できる。
論文 参考訳（メタデータ） (2026-07-07T16:11:30Z) - LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。
本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
論文 参考訳（メタデータ） (2026-06-02T08:16:42Z) - Mechanic: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving [13.446180044466324]
メカニック(Mechanic)は、謝罪駆動の形式的分解戦略を採用した新しいエージェントシステムである。
未解決のサブゴールを正確に分離するために、リーンの残念なプレースホルダーを活用することで、Mechanicは失敗するサブプロブレムを、クリーンで自己完結したコンテキストに抽出し、独立して解決する。
論文 参考訳（メタデータ） (2026-03-25T16:12:08Z) - Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving [36.20164235042574]
本研究では,レムマ型全耐久推論モデルである textbfSeed-Prover を提案する。
IMOレベルの競合問題を解決するために、深い推論と広い推論の両方を可能にする3つのテストタイム推論戦略を設計する。
シード・プロバーは、過去のIMO問題の78.1%ドルを証明し、ミニF2Fを飽和させ、パットナムベンチで50%以上を達成し、それまでの最先端よりも大きな差を付けた。
論文 参考訳（メタデータ） (2025-07-31T17:00:30Z) - TrustGeoGen: Formal-Verified Data Engine for Trustworthy Multi-modal Geometric Problem Solving [106.04001249574786]
TrustGeoGenは、標準的で信頼性の高いベンチマークを確立するために、正式に検証された幾何問題を生成するデータエンジンである。
1)ダイアグラム,テキスト,ステップバイステップのソリューションの生成を同期するマルチモーダルアライメント,2)すべての推論パスがルール準拠であることを保証する形式検証,3)接続思考,ブリッジング,ヒューマンライクな論理ステップとの論理的推論,4)複数のソリューションと自己回帰バックトラックを備えた多種多様な問題を生成できるTextitGeoExploreシリーズアルゴリズム。
論文 参考訳（メタデータ） (2025-04-22T10:45:23Z) - LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
フォーマルな定理証明のための新しい生涯学習フレームワークであるLeanAgentを紹介する。
LeanAgentは継続的に一般化し、拡張可能な数学的知識を改善します。
これは23のリーンリポジトリにわたる155の定理の正式な証明を生成する。
論文 参考訳（メタデータ） (2024-10-08T17:11:24Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳（メタデータ） (2024-02-14T05:57:58Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。