論文の概要: IneqAgent: Agentic Inequality Proving in Lean with Symbolic Computation

• arxiv url: http://arxiv.org/abs/2610.20681v1
• Date: Wed, 14 Oct 2026 16:29:11 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-16 19:13:15.979249
• Title: IneqAgent: Agentic Inequality Proving in Lean with Symbolic Computation
• Title（参考訳）: IneqAgent: シンボリック計算によるリーンのエージェント不平等証明
• Abstract要約: IneqAgentは、LLM推論と記号計算を組み合わせたエージェントフレームワークで、Lean4で不等式を証明する。 4つのベンチマークで、IneqAgent with DeepSeek-V4-Flashは186の問題の175つ(94.09%)を解き、評価された方法の中で最も高い総合的な成功率を達成した。 また、ディッター予想を 4 次元と 5 次元で証明し、ホレンス=ジョコビッチ$(4,4)$不等式を証明し、メリス予想を 4 次元で証明する。
• 参考スコア（独自算出の注目度）: 13.360369528048382
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal inequality proving requires mathematical reasoning and exact computation, often connected through intermediate lemmas and goal reformulations. We introduce IneqAgent, an agentic framework combining LLM reasoning with symbolic computation for inequality proving in Lean4. Lemma-level Monte Carlo Tree Search coordinates lemma construction, goal reformulation, and symbolic backend selection. Complementary sum-of-squares, Bernstein, and successive difference-substitution backends produce exact certificates for local Lean proof generation. The agent integrates these proofs with LLM-generated steps and uses Lean feedback to construct complete proofs checked against the original theorem statements. On four benchmarks, IneqAgent with DeepSeek-V4-Flash solves 175 of 186 problems (94.09%), achieving the highest overall success rate among the evaluated methods. Across four backbones, it achieves higher success rates at low LLM inference cost thresholds than Direct Agent using the same backbone, with lower mean inference costs over each method's successful runs. We also obtain Lean-verified strengthenings of Dittert's conjecture in dimensions four and five, and certify the Holens--Djokovic $(4,4)$ inequality, implying Merris's conjecture in dimension four.
• Abstract（参考訳）: 形式的不等式証明には数学的推論と正確な計算が必要であり、しばしば中間補題やゴール修正を通じて接続される。 本稿では,LLM推論と記号計算を組み合わせたエージェントフレームワークであるIneqAgentを紹介する。 LemmaレベルのMonte Carlo Tree Searchは、レムマの構築、ゴールの再編成、シンボリックバックエンドの選択をコーディネートする。 補足的な2乗和、バーンスタインおよび連続した差分置換バックエンドは、局所的なリーン証明生成のための正確な証明書を生成する。 エージェントはこれらの証明をLLM生成ステップと統合し、リーンフィードバックを使用して、元の定理文に対してチェックされた完全な証明を構築する。 4つのベンチマークで、IneqAgent with DeepSeek-V4-Flashは186の問題の175つ(94.09%)を解き、評価された方法の中で最も高い総合的な成功率を達成した。 4つのバックボーンにまたがって、同じバックボーンを使用するダイレクトエージェントよりも低LSM推論コスト閾値で高い成功率を達成する。 また、ディッター予想を 4 次元と 5 次元で証明し、ホレンス=ジョコビッチ$(4,4)$不等式を証明し、メリス予想を 4 次元で証明する。

関連論文リスト

• Cost-Efficient Theorem Proving via Agent Orchestration in Program Verification [19.12388440070344]
  プログラム検証は、定理証明器で構築された機械チェック可能な証明を通じてソフトウェア正当性を確立する。 しかし、ほとんどの既存のプローバーは、サンプリングや検索の予算でのみパスレートを追求している。 CoCo-Proverは、メタレベルの意思決定としてコスト効率の高いプログラムを定式化している。
  論文  参考訳（メタデータ） (2026-10-07T08:42:24Z)
• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。 本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
  論文  参考訳（メタデータ） (2026-06-02T08:16:42Z)
• Hilbert: Recursively Building Formal Proofs with Informal Reasoning [38.36481253622752]
  大規模言語モデル(LLM)は、驚くべき数学的推論能力を示しているが、そのソリューションには自動検証できないエラーが含まれていることが多い。 非公式な推論と形式的検証の相補的な強みを組み合わせたエージェントフレームワークであるHilbertを紹介する。 我々のシステムは4つのコンポーネントを編成する: 数学的推論に優れる非公式のLLM、リーン4の戦術に最適化された特殊なLLM、形式検証器、意味定理検索器。
  論文  参考訳（メタデータ） (2025-09-26T18:24:23Z)
• Eigen-1: Adaptive Multi-Agent Refinement with Monitor-Based RAG for Scientific Reasoning [53.45095336430027]
  暗黙的な検索と構造化された協調を組み合わせた統合フレームワークを開発する。 Humanity's Last Exam (HLE) Bio/Chem Goldでは,48.3%の精度を実現している。 SuperGPQAとTRQAの結果はドメイン間の堅牢性を確認した。
  論文  参考訳（メタデータ） (2025-09-25T14:05:55Z)
• Solving Inequality Proofs with Large Language Models [42.667163027148916]
  不等式証明は様々な科学・数学分野において不可欠である。 これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。 我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
  論文  参考訳（メタデータ） (2025-06-09T16:43:38Z)
• 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)
• Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
  LLMの複雑な推論には2行のアプローチが採用されている。 1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。 他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。 具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
  論文  参考訳（メタデータ） (2023-11-16T11:26:21Z)

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

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