論文の概要: 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)
• Brains vs. Bytes: Evaluating LLM Proficiency in Olympiad Mathematics [2.489157527463306]
  大規模言語モデル(LLM)は、数学的推論タスクにおいて顕著な進歩を示している。 大規模言語モデル(LLM)の最近の進歩は、数学的推論タスクの顕著な進歩を示している。
  論文  参考訳（メタデータ） (2025-04-01T00:10:10Z)
• 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)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  証明の進捗を予測する手法であるLeanProgressを紹介します。 実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
  論文  参考訳（メタデータ） (2025-02-25T07:46:36Z)
• Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
  本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。 我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。 我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
  論文  参考訳（メタデータ） (2024-11-04T05:57:40Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。 LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。 本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
  論文  参考訳（メタデータ） (2024-10-05T05:21:48Z)
• 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)
• CHAMP: A Competition-level Dataset for Fine-Grained Analyses of LLMs' Mathematical Reasoning Capabilities [25.857946070979576]
  概念とHint-Annotated Math Problems (CHAMP) は、概念に注釈を付けた高校数学の競争問題である。 このベンチマークは困難で、最高のモデルは標準設定で58.1%しか得点できない。 モデルはしばしば、間違った推論ステップを通じて、正しい最終回答に到達します。
  論文  参考訳（メタデータ） (2024-01-13T03:18:16Z)

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

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