Solving Inequality Proofs with Large Language Models

要約

不平等の証明、多様な科学的および数学的分野にわたる重要な、厳しい境界や戦略的定理アプリケーションの発見などの高度な推論スキルをテストします。
これにより、大規模な言語モデル（LLMS）に明確で要求の厳しいフロンティアになり、一般的な数学的な問題解決を超えた洞察を提供します。
この領域の進歩は、しばしば希少性、合成、または厳格に形式的な既存のデータセットによって妨げられています。
これに対処し、非公式でありながら検証可能なタスクの定式化を提案し、2つの自動的にチェック可能なサブタスクの2つの自動的なチェック可能なサブタスクに証明する不平等を再構築します。
これに基づいて、段階的なソリューションと定理注釈が濃縮されたテストセットやトレーニングコーパスを含む、オリンピックレベルの不平等の専門家であるデータセットであるIneqmathをリリースします。
また、新しいLLMとしてのJudge As-Judge評価フレームワークを開発し、最終回答の裁判官と、一般的な推論の欠陥を検出するように設計された4つの段階的な裁判官を組み合わせています。
INEQMATHでの29の主要なLLMの体系的な評価は、驚くべき現実を明らかにしています。O1のようなトップモデルでさえ、段階的な精査では全体的な精度が10％未満です。
これは、最終的な回答の等価のみを考慮して、精度から最大65.5％の低下です。
この矛盾は、単に答えを見つけることと厳密な証拠を構築することとの間に、脆弱な演ductive的なチェーンと現在のLLMの重要なギャップを暴露します。
モデルサイズのスケーリングとテスト時間計算の増加により、全体的な証明の正確性が限られています。
代わりに、私たちの調査結果は、定理誘導の推論や自己修正などの有望な研究方向を強調しています。
コードとデータはhttps://ineqmath.github.io/で入手できます。

要約(オリジナル)

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/.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google