論文の概要: Enumerate-Conjecture-Prove: Formally Solving Answer-Construction Problems in Math Competitions

• arxiv url: http://arxiv.org/abs/2505.18492v1
• Date: Sat, 24 May 2025 03:52:25 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-27 16:58:42.45713
• Title: Enumerate-Conjecture-Prove: Formally Solving Answer-Construction Problems in Math Competitions
• Title（参考訳）: Enumerate-Conjecture-Prove:数学コンペティションにおける解答Answer-Construction問題
• Authors: Jialiang Sun, Yuzhi Tang, Ao Li, Chris J. Maddison, Kuldeep S. Meel,
• Abstract要約: 本稿では,パターン駆動型推論と形式的定理証明を統合するモジュール型ニューロシンボリック手法であるCreativee-Conjecture-Prove(ECP)フレームワークを紹介する。 本稿では,様々な数学コンペティションにおける3,431の解題問題のデータセットであるConstructiveBenchを紹介する。
• 参考スコア（独自算出の注目度）: 37.10426226729792
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Mathematical reasoning lies at the heart of artificial intelligence, underpinning applications in education, program verification, and research-level mathematical discovery. Mathematical competitions, in particular, present two challenging problem types: theorem-proving, requiring rigorous proofs of stated conclusions, and answer-construction, involving hypothesizing and formally verifying mathematical objects. Large Language Models (LLMs) effectively generate creative candidate answers but struggle with formal verification, while symbolic provers ensure rigor but cannot efficiently handle creative conjecture generation. We introduce the Enumerate-Conjecture-Prove (ECP) framework, a modular neuro-symbolic method integrating LLM-based enumeration and pattern-driven conjecturing with formal theorem proving. We present ConstructiveBench, a dataset of 3,431 answer-construction problems in various math competitions with verified Lean formalizations. On the ConstructiveBench dataset, ECP improves the accuracy of answer construction from the Chain-of-Thought (CoT) baseline of 14.54% to 45.06% with the gpt-4.1-mini model. Moreover, combining with ECP's constructed answers, the state-of-the-art DeepSeek-Prover-V2-7B model generates correct proofs for 858 of the 3,431 constructive problems in Lean, achieving 25.01% accuracy, compared to 9.86% for symbolic-only baselines. Our code and dataset are publicly available at GitHub and HuggingFace, respectively.
• Abstract（参考訳）: 数学的推論は人工知能の中心にあり、教育、プログラム検証、研究レベルの数学的発見の基盤となっている。 特に数学の競争は、定理の証明、結論の厳密な証明、数学的対象の仮説化と公式な検証を含む解の構成という2つの挑戦的な問題タイプを提示する。 大規模言語モデル(LLM)は、創造的候補の答えを効果的に生成するが、形式的な検証に苦慮する一方で、記号的プローバーは厳密性を保証するが、創造的予想の生成を効率的に扱えない。 本稿では,LLMに基づく列挙法と形式的定理証明を用いたパターン駆動型帰納法を統合するモジュール型ニューロシンボリック手法であるEnumerate-Conjecture-Prove (ECP) フレームワークを紹介する。 本稿では,様々な数学コンペティションにおける3,431の回答構成問題のデータセットであるConstructiveBenchについて述べる。 ConstructiveBench データセットでは、ECP は gpt-4.1-mini モデルで 14.54% から 45.06% まで解答構築の精度を向上させる。 さらに、ECPが構築した回答と組み合わせて、最先端のDeepSeek-Prover-V2-7Bモデルは、リーンにおける3,431の建設問題の858の正しい証明を生成し、25.01%の精度で達成した。 コードとデータセットはそれぞれGitHubとHuggingFaceで公開されています。

関連論文リスト

• Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving [44.5694120006447]
  決定論的マルコフ決定過程として,問題解決の原理的定式化を提案する。 また,既存のFTP環境を利用してプロセス検証問題解決を行う新しいフレームワークFPSを提案する。 我々は, MATH500ベンチマークのサブセットの形式化であるFormalMath500, MiniF2F-Solving, PutnamBench-Solving, FTPベンチマークのMiniF2FとPutnamBenchの適応の3つのベンチマークを構築した。
  論文  参考訳（メタデータ） (2025-05-07T16:02:14Z)
• FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
  本稿では,高校のオリンピアード問題から学部レベルの定理まで,5,560の公証問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。 本稿では,文の自動形式化,セマンティック検証,否定に基づく無防備なフィルタリング戦略を統合した,新たなオートフォーマル化パイプラインを提案する。 現状のLSMに基づく定理証明器の評価は, 重大な限界を呈する。
  論文  参考訳（メタデータ） (2025-05-05T15:37:00Z)
• DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition [24.50773495427783]
  我々はDeepSeek-Prover-V2を紹介します。 このモデルは、ニューラル定理の証明における最先端のパフォーマンスを達成し、ミニF2Fテストで88.9%のパス比に達し、PutnamBenchの658問題のうち49を解決した。 標準ベンチマークに加えて、325の形式化された問題の集合であるProverBenchを導入し、最近のAIMEコンペティションから選択された15の問題を含む評価を強化した。
  論文  参考訳（メタデータ） (2025-04-30T16:57:48Z)
• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
  我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。 まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。 次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。 最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
  論文  参考訳（メタデータ） (2025-02-11T15:27:35Z)
• 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)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。 この合成データセットでDeepSeekMath 7Bモデルを微調整します。 我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
  論文  参考訳（メタデータ） (2024-05-23T09:03:42Z)

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

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