論文の概要: Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving on Inequalities

• arxiv url: http://arxiv.org/abs/2505.12680v1
• Date: Mon, 19 May 2025 03:56:05 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-20 14:57:11.390652
• Title: Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving on Inequalities
• Title（参考訳）: Ineq-Comp:不等式を証明した自動定理における人間の直観的構成推論のベンチマーク
• Authors: Haoyu Zhao, Yihan Geng, Shange Tang, Yong Lin, Bohan Lyu, Hongzhou Lin, Chi Jin, Sanjeev Arora,
• Abstract要約: LLMベースの形式的証明アシスタント(例:リーン)は、数学的発見の自動化を大いに約束する。 これらのシステムは、人間と同じように数学的構造を本当に理解していますか? この問題を数学的不等式のレンズを用いて検討する。
• 参考スコア（独自算出の注目度）: 45.8704193793732
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: LLM-based formal proof assistants (e.g., in Lean) hold great promise for automating mathematical discovery. But beyond syntactic correctness, do these systems truly understand mathematical structure as humans do? We investigate this question through the lens of mathematical inequalities -- a fundamental tool across many domains. While modern provers can solve basic inequalities, we probe their ability to handle human-intuitive compositionality. We introduce Ineq-Comp, a benchmark built from elementary inequalities through systematic transformations, including variable duplication, algebraic rewriting, and multi-step composition. Although these problems remain easy for humans, we find that most provers -- including Goedel, STP, and Kimina-7B -- struggle significantly. DeepSeek-Prover-V2-7B shows relative robustness -- possibly because it is trained to decompose the problems into sub-problems -- but still suffers a 20\% performance drop (pass@32). Strikingly, performance remains poor for all models even when formal proofs of the constituent parts are provided in context, revealing that the source of weakness is indeed in compositional reasoning. Our results expose a persisting gap between the generalization behavior of current AI provers and human mathematical intuition.
• Abstract（参考訳）: LLMベースの形式的証明アシスタント(例:リーン)は、数学的発見を自動化するための大きな約束を持っています。 しかし、構文的正しさ以外にも、これらのシステムは人間と同じように数学的構造を本当に理解しているのだろうか? この問題は、多くの領域にまたがる基本的なツールである数学的不等式(英語版)のレンズを通して検討する。 現代のプローバーは基本的な不等式を解くことができるが、人間の直感的な構成性を扱う能力について検討する。 Ineq-Compは、変数重複、代数的書き換え、多段階合成を含む体系的な変換を通じて、初等不等式から構築されたベンチマークである。 これらの問題は人間にとって容易なままだが、Goedel、STP、Kimina-7Bを含むほとんどのプローバーが苦戦している。 DeepSeek-Prover-V2-7Bは相対的な堅牢性 - 問題をサブプロブレムに分解するように訓練されているためか - を示しているが、それでも20倍のパフォーマンス低下(pass@32)を被っている。 厳密には、構成部品の形式的証明が文脈で提供されたとしても、全てのモデルで性能が劣るままであり、弱みの源が実際は構成的推論にあることを明らかにしている。 我々の結果は、現在のAIプロデューサの一般化行動と人間の数学的直観の間に持続的なギャップを露呈する。

関連論文リスト

• Solving Inequality Proofs with Large Language Models [46.71658812761115]
  不等式証明は様々な科学・数学分野において不可欠である。 これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。 我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
  論文  参考訳（メタデータ） (2025-06-09T16:43:38Z)
• Enhancing Mathematical Reasoning in Large Language Models with Self-Consistency-Based Hallucination Detection [0.0]
  数学的推論の信頼性を高めるために,構造化自己整合性フレームワークを導入する。 本手法は,中間ステップと最終出力の自己整合性を強制し,論理的不整合や幻覚を低減させる。 実験の結果,SCは証明精度,記号的推論精度,数値安定性を著しく向上することがわかった。
  論文  参考訳（メタデータ） (2025-04-13T05:47:52Z)
• PromptCoT: Synthesizing Olympiad-level Problems for Mathematical Reasoning in Large Language Models [59.920971312822736]
  本稿では,高品質なオリンピアードレベルの数学問題を自動生成する新しい手法であるPromptCoTを紹介する。 提案手法は,問題構築の背景にある数学的概念と理論的根拠に基づいて複雑な問題を合成する。 提案手法は, GSM8K, MATH-500, AIME2024などの標準ベンチマークで評価され, 既存の問題生成手法を一貫して上回っている。
  論文  参考訳（メタデータ） (2025-03-04T06:32:30Z)
• MATH-Perturb: Benchmarking LLMs' Math Reasoning Abilities against Hard Perturbations [90.07275414500154]
  各種モデルにおけるMATH-P-Hardの性能低下を観察する。 また、学習した問題解決スキルを盲目的に適用する新しい形態の記憶に関する懸念も提起する。
  論文  参考訳（メタデータ） (2025-02-10T13:31:46Z)
• MathGAP: Out-of-Distribution Evaluation on Problems with Arbitrarily Complex Proofs [80.96119560172224]
  MathGAPは、それらの算術的証明構造に関する仕様に従って、問題文と連鎖推論トレースを生成する。 MathGAP を用いて, LLM はより深く, より広くなるにつれて, 性能が著しく低下することがわかった。
  論文  参考訳（メタデータ） (2024-10-17T12:48:14Z)
• Artifical intelligence and inherent mathematical difficulty [0.0]
  まず、計算可能性と複雑性理論による制限的な結果が証明発見が本質的に難しい問題であることを示す従来の議論の更新版を提示する。 次に、人工知能にインスパイアされた最近のいくつかの応用が、数学的な証明の性質に関する新しい疑問を実際に提起する方法について説明する。
  論文  参考訳（メタデータ） (2024-08-01T20:08:31Z)
• MathCAMPS: Fine-grained Synthesis of Mathematical Problems From Human Curricula [33.5782208232163]
  本研究では,高品質な数学問題を大規模に合成する手法であるMath CAMPSを提案する。 それぞれの標準を形式文法でエンコードし、様々な記号問題とその解をサンプリングする。 我々は、記号構造からフォローアップ質問を導き、それらをフォローアップ単語問題に変換する。
  論文  参考訳（メタデータ） (2024-07-01T01:56:28Z)
• A Hybrid System for Systematic Generalization in Simple Arithmetic Problems [70.91780996370326]
  本稿では,記号列に対する合成的および体系的推論を必要とする算術的問題を解くことができるハイブリッドシステムを提案する。 提案システムは,最も単純なケースを含むサブセットでのみ訓練された場合においても,ネストした数式を正確に解くことができることを示す。
  論文  参考訳（メタデータ） (2023-06-29T18:35:41Z)
• Faith and Fate: Limits of Transformers on Compositionality [109.79516190693415]
  3つの代表的構成課題にまたがる変圧器大言語モデルの限界について検討する。 これらのタスクは、問題をサブステップに分割し、これらのステップを正確な答えに合成する必要があります。 実験結果から,多段階合成推論を線形化部分グラフマッチングに還元することにより,トランスフォーマーLLMが構成課題を解くことが示唆された。
  論文  参考訳（メタデータ） (2023-05-29T23:24:14Z)

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

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