論文の概要: Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph

• arxiv url: http://arxiv.org/abs/2510.04520v1
• Date: Mon, 06 Oct 2025 06:25:11 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-07 16:52:59.70524
• Title: Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph
• Title（参考訳）: Aria: 依存関係グラフによる検索と反復的な自動形式化のためのエージェント
• Authors: Hanyu Wang, Ruohan Xie, Yutong Wang, Guoxiong Gao, Xintao Yu, Bin Dong,
• Abstract要約: リーンの予想レベルの形式化のためのシステムであるAriaを紹介します。 Ariaは、2フェーズのGraph-of-Thoughtプロセスを通じて、人間の専門家による推論をエミュレートする。 AriaScorerは、用語レベルの接地のためにMathlibから定義を検索する。
• 参考スコア（独自算出の注目度）: 7.606625807305093
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Accurate auto-formalization of theorem statements is essential for advancing automated discovery and verification of research-level mathematics, yet remains a major bottleneck for LLMs due to hallucinations, semantic mismatches, and their inability to synthesize new definitions. To tackle these issues, we present Aria (Agent for Retrieval and Iterative Autoformalization), a system for conjecture-level formalization in Lean that emulates human expert reasoning via a two-phase Graph-of-Thought process: recursively decomposing statements into a dependency graph and then constructing formalizations from grounded concepts. To ensure semantic correctness, we introduce AriaScorer, a checker that retrieves definitions from Mathlib for term-level grounding, enabling rigorous and reliable verification. We evaluate Aria on diverse benchmarks. On ProofNet, it achieves 91.6% compilation success rate and 68.5% final accuracy, surpassing previous methods. On FATE-X, a suite of challenging algebra problems from research literature, it outperforms the best baseline with 44.0% vs. 24.0% final accuracy. On a dataset of homological conjectures, Aria reaches 42.9% final accuracy while all other models score 0%.
• Abstract（参考訳）: 定理ステートメントの正確な自己形式化は、研究レベルの数学の自動発見と検証の推進に不可欠であるが、幻覚、意味的ミスマッチ、そして新しい定義を合成できないことによるLLMにとって、依然として大きなボトルネックとなっている。 これらの問題に取り組むために、Aria (Agent for Retrieval and Iterative Autoformalization)というリーンの予想レベルの形式化システムを紹介します。 セマンティックな正当性を保証するために,Mathlibから定義を検索して,厳密で信頼性の高い検証を可能にするチェッカーであるAriaScorerを導入する。 多様なベンチマークでAriaを評価する。 ProofNetでは、91.6%のコンパイル成功率と68.5%の最終的な精度を達成した。 FATE-Xは研究論文からの挑戦的代数問題の一組であり、44.0%対24.0%の最終精度で最高のベースラインを上回っている。 ホモロジー予想のデータセットでは、アリアは最終精度が42.9%に達し、他の全てのモデルでは0%である。

関連論文リスト

• Solving Inequality Proofs with Large Language Models [46.71658812761115]
  不等式証明は様々な科学・数学分野において不可欠である。 これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。 我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
  論文  参考訳（メタデータ） (2025-06-09T16:43:38Z)
• REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning [12.343823629674368]
  私たちはREAL-Proverという,Lean 4.0用の新たなオープンソースステップワイドな定理証明ツールを紹介します。 我々の証明者は、特に大学レベルの数学問題の解法における性能を高める。 実験では、教師付き微チューン定理のみを用いた証明器は23.7%の成功率で競合する結果が得られる。
  論文  参考訳（メタデータ） (2025-05-27T01:26:11Z)
• LIMO: Less is More for Reasoning [23.312893016642096]
  数例の例で、洗練された数学的推論が実現可能であることを実証する。 LIMOはAIME24では63.3%,MATH500では95.6%の精度を実現している。 LIMOは、様々なベンチマークで45.8%の絶対的な改善を実現している。
  論文  参考訳（メタデータ） (2025-02-05T17:23:45Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Improving Autoformalization using Type Checking [15.58948808529849]
  我々は、現在の自己形式化手法とそれらの評価に使用されるプロセスの両方を分析し、特にLean 4の定理証明言語に注目します。 ProofNetの絶対精度は18.4%まで向上し,既存の手法上での自己整合性による型チェックフィルタリングが性能を著しく向上することを示した。 我々はまた、新しい研究レベルの数学データセット RLM25、修正されたProofNet、ラベル付き正誤オートフォーマライゼーションペアでメトリクスを評価するProofNetVerifといった新しいベンチマークもリリースした。
  論文  参考訳（メタデータ） (2024-06-11T13:01:50Z)
• 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)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。 本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。 我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
  論文  参考訳（メタデータ） (2020-10-06T15:47:53Z)

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

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