論文の概要: 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プロデューサの一般化行動と人間の数学的直観の間に持続的なギャップを露呈する。

関連論文リスト

• 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)
• 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)
• A Hybrid System for Systematic Generalization in Simple Arithmetic Problems [70.91780996370326]
  本稿では,記号列に対する合成的および体系的推論を必要とする算術的問題を解くことができるハイブリッドシステムを提案する。 提案システムは,最も単純なケースを含むサブセットでのみ訓練された場合においても,ネストした数式を正確に解くことができることを示す。
  論文  参考訳（メタデータ） (2023-06-29T18:35:41Z)

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

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