論文の概要: Solving Inequality Proofs with Large Language Models

• arxiv url: http://arxiv.org/abs/2506.07927v1
• Date: Mon, 09 Jun 2025 16:43:38 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-06-10 16:33:11.060685
• Title: Solving Inequality Proofs with Large Language Models
• Title（参考訳）: 大規模言語モデルを用いた不等式証明の解法
• Authors: Jiayi Sheng, Luna Lyu, Jikai Jin, Tony Xia, Alex Gu, James Zou, Pan Lu,
• Abstract要約: 不等式証明は様々な科学・数学分野において不可欠である。 これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。 我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
• 参考スコア（独自算出の注目度）: 46.71658812761115
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Inequality proving, crucial across diverse scientific and mathematical fields, tests advanced reasoning skills such as discovering tight bounds and strategic theorem application. This makes it a distinct, demanding frontier for large language models (LLMs), offering insights beyond general mathematical problem-solving. Progress in this area is hampered by existing datasets that are often scarce, synthetic, or rigidly formal. We address this by proposing an informal yet verifiable task formulation, recasting inequality proving into two automatically checkable subtasks: bound estimation and relation prediction. Building on this, we release IneqMath, an expert-curated dataset of Olympiad-level inequalities, including a test set and training corpus enriched with step-wise solutions and theorem annotations. We also develop a novel LLM-as-judge evaluation framework, combining a final-answer judge with four step-wise judges designed to detect common reasoning flaws. A systematic evaluation of 29 leading LLMs on IneqMath reveals a surprising reality: even top models like o1 achieve less than 10% overall accuracy under step-wise scrutiny; this is a drop of up to 65.5% from their accuracy considering only final answer equivalence. This discrepancy exposes fragile deductive chains and a critical gap for current LLMs between merely finding an answer and constructing a rigorous proof. Scaling model size and increasing test-time computation yield limited gains in overall proof correctness. Instead, our findings highlight promising research directions such as theorem-guided reasoning and self-refinement. Code and data are available at https://ineqmath.github.io/.
• Abstract（参考訳）: 不等式証明は、様々な科学や数学の分野において不可欠であり、厳密な境界の発見や戦略的定理の適用のような高度な推論スキルのテストである。 これにより、大きな言語モデル(LLM)の明確なフロンティアとなり、一般的な数学的問題解決以上の洞察を提供する。 この領域の進歩は、しばしば不足し、合成され、または厳格に形式化された既存のデータセットによって妨げられている。 本稿では,不等式を2つの自動チェック可能なサブタスク(境界推定と関係予測)に再キャストすることで,非公式に検証可能なタスクの定式化を提案する。 これに基づいて、我々は、Olympiadレベルの不等式を専門家が計算したデータセットであるIneqMathをリリースした。 また,LLM-as-judge評価フレームワークを開発し,一般的な推論欠陥を検出するための4つのステップワイズ・ジャッジと最終回答ジャッジを組み合わせた。 IneqMath上の29個のLLMを体系的に評価すると、驚くべき事実が明らかになる: o1のようなトップモデルでさえステップワイズで全体の10%未満の精度を達成する; これは最終回答の等価性のみを考慮して、その精度から65.5%まで低下する。 この不一致は、単に答えを見つけることと厳密な証明を構築することの間の、脆弱な縮退鎖と、現在のLLMに対する臨界ギャップを露呈する。 モデルのサイズを拡大し、テストタイムの計算量が増加すると、全体の証明精度が制限される。 その代わり,本研究では,定理誘導推論や自己補充など,有望な研究の方向性を強調した。 コードとデータはhttps://ineqmath.github.io/で公開されている。

関連論文リスト

• FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
  本稿では,高校のオリンピアード問題から学部レベルの定理まで,5,560の公証問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。 本稿では,文の自動形式化,セマンティック検証,否定に基づく無防備なフィルタリング戦略を統合した,新たなオートフォーマル化パイプラインを提案する。 現状のLSMに基づく定理証明器の評価は, 重大な限界を呈する。
  論文  参考訳（メタデータ） (2025-05-05T15:37:00Z)
• Challenging the Boundaries of Reasoning: An Olympiad-Level Math Benchmark for Large Language Models [86.45058529521258]
  OlymMATHは、LLMの複雑な推論能力を厳格にテストするために設計された、Olympiadレベルの新しい数学ベンチマークである。 OlymMATHは200の厳密にキュレートされた問題があり、それぞれが手動で検証され、英語と中国語の並行バージョンで利用可能である。
  論文  参考訳（メタデータ） (2025-03-27T11:20:17Z)
• Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
  本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。 我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。 我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
  論文  参考訳（メタデータ） (2024-11-04T05:57:40Z)
• Evaluating Mathematical Reasoning Beyond Accuracy [50.09931172314218]
  推論ステップの品質を評価するための新しい方法論であるReasonEvalを紹介します。 ReasonEvalはメタ評価データセットのベースライン手法よりも一貫して優れていることを示す。 我々は、ReasonEvalがデータ選択において重要な役割を果たすことを観察する。
  論文  参考訳（メタデータ） (2024-04-08T17:18:04Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)

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

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