論文の概要: Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving

• arxiv url: http://arxiv.org/abs/2507.06804v1
• Date: Mon, 07 Jul 2025 22:38:49 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-07-10 17:37:43.584771
• Title: Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving
• Title（参考訳）: 疎結合推論と証明によるIMO問題の改善に向けて
• Authors: Zhenwen Liang, Linfeng Song, Yang Li, Tao Yang, Feng Zhang, Haitao Mi, Dong Yu,
• Abstract要約: 最近の研究では、非公式な精度は80%を超え、公式な成功はPutnamBenchのようなベンチマークで8%以下である。 低レベルの証明生成から高レベルの推論を分離する新しいフレームワークを提案する。 提案手法は,2000年以降のIMO問題に対して,従来のオープンソース証明者が未報告の課題として評価した。
• 参考スコア（独自算出の注目度）: 48.22540519786074
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Automated Theorem Proving (ATP) in formal languages is a foundational challenge for AI. While Large Language Models (LLMs) have driven remarkable progress, a significant gap remains between their powerful informal reasoning capabilities and their weak formal proving performance. Recent studies show that the informal accuracy exceeds 80% while formal success remains below 8% on benchmarks like PutnamBench. We argue this gap persists because current state-of-the-art provers, by tightly coupling reasoning and proving, are trained with paradigms that inadvertently punish deep reasoning in favor of shallow, tactic-based strategies. To bridge this fundamental gap, we propose a novel framework that decouples high-level reasoning from low-level proof generation. Our approach utilizes two distinct, specialized models: a powerful, general-purpose Reasoner to generate diverse, strategic subgoal lemmas, and an efficient Prover to rigorously verify them. This modular design liberates the model's full reasoning potential and bypasses the pitfalls of end-to-end training. We evaluate our method on a challenging set of post-2000 IMO problems, a problem set on which no prior open-source prover has reported success. Our decoupled framework successfully solves 5 of these problems, demonstrating a significant step towards automated reasoning on exceptionally difficult mathematical challenges. To foster future research, we release our full dataset of generated and verified lemmas for a wide range of IMO problems, available at https://tencent-imo.github.io/ .
• Abstract（参考訳）: 形式言語におけるATP(Automated Theorem Proving)は、AIの基本的な課題である。 大きな言語モデル(LLM)は目覚ましい進歩を遂げているが、強力な非公式推論能力と弱い形式的証明性能との間には大きなギャップが残っている。 最近の研究では、非公式な精度は80%を超え、公式な成功はPutnamBenchのようなベンチマークで8%以下である。 このギャップは、現在の最先端のプローバーが、推論と証明の密結合によって、浅く戦術的な戦略を好んで必然的に深い推論を罰するパラダイムで訓練されているため、今後も続くと我々は主張する。 このギャップを埋めるために、我々は、低レベルな証明生成から高レベルな推論を分離する新しいフレームワークを提案する。 このアプローチでは,多種多様な戦略的なサブゴール補題を生成するために,強力で汎用的なReasonerと,それらを厳格に検証するための効率的なProverの2つのモデルを利用する。 このモジュラー設計はモデルの完全な推論能力を解放し、エンドツーエンドのトレーニングの落とし穴を回避します。 提案手法は,2000年以降のIMO問題において,従来のオープンソース証明者が成功を報告していない問題に対して評価を行った。 我々の分離されたフレームワークは、これらの問題の5つをうまく解決し、非常に難しい数学的課題に対する自動推論に向けた重要なステップを示します。 将来の研究を促進するため、私たちは、広範囲のIMO問題に対して生成された検証済みのレムマの全データセットを、https://tencent-imo.github.io/で公開しています。

関連論文リスト

• Solving Inequality Proofs with Large Language Models [46.71658812761115]
  不等式証明は様々な科学・数学分野において不可欠である。 これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。 我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
  論文  参考訳（メタデータ） (2025-06-09T16:43:38Z)
• FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
  本稿では,高校のオリンピアード問題から学部レベルの定理まで,5,560の公証問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。 本稿では,文の自動形式化,セマンティック検証,否定に基づく無防備なフィルタリング戦略を統合した,新たなオートフォーマル化パイプラインを提案する。 現状のLSMに基づく定理証明器の評価は, 重大な限界を呈する。
  論文  参考訳（メタデータ） (2025-05-05T15:37:00Z)
• Causality can systematically address the monsters under the bench(marks) [64.36592889550431]
  ベンチマークはさまざまなバイアス、アーティファクト、リークに悩まされている。 モデルは、調査の不十分な障害モードのため、信頼できない振る舞いをする可能性がある。 因果関係はこれらの課題を体系的に解決するための 理想的な枠組みを提供します
  論文  参考訳（メタデータ） (2025-02-07T17:01:37Z)
• Reasoning Paths Optimization: Learning to Reason and Explore From Diverse Paths [69.39559168050923]
  本稿では,多様な経路から学習の推論と探索を可能にするReasoning Paths Optimization (RPO)を紹介する。 提案手法は,各推論ステップにおいて好意的な分岐を奨励し,好ましくない分岐を罰し,モデル全体の問題解決性能を高める。 我々は,数語問題や理科ベースの試験問題など,多段階の推論タスクに焦点をあてる。
  論文  参考訳（メタデータ） (2024-10-07T06:37:25Z)
• VC Search: Bridging the Gap Between Well-Defined and Ill-Defined Problems in Mathematical Reasoning [46.25056744404318]
  5000以上の不確定な数学的問題を含むPMC(Issue with Missing and Contradictory conditions)というベンチマークを開発した。 VCSEARCHは、解決不可能な問題を特定する精度を、さまざまな大きな言語モデルで少なくとも12%向上させる。
  論文  参考訳（メタデータ） (2024-06-07T16:24:12Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)

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

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