Fugu-MT 論文翻訳(概要): Enumerate-Conjecture-Prove: Formally Solving Answer-Construction Problems in Math Competitions

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

arxiv url: http://arxiv.org/abs/2505.18492v4
Date: Sat, 18 Oct 2025 04:19:19 GMT
ステータス: 翻訳完了
システム内更新日: 2025-10-25 03:08:06.715196
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要約: LLMは難解な解答作業に対処できるが、幻覚や不可解なステップの誤りを生じやすい。創造性と数学的厳密性の両方を保ちながら、どのように解答-構成問題を解決するか? 本稿では,パターン駆動型推論と形式的定理証明を統合したニューロシンボリックな手法であるLLM-Conjecture-Prove(ECP)フレームワークを紹介する。 ConstructiveBenchでは、ECPは33.1%の最先端の精度(32.5%から)を達成し、公式な数学的推論を前進させる可能性を示している。
参考スコア（独自算出の注目度）: 39.102692814217086
License: http://creativecommons.org/licenses/by/4.0/
Abstract: Mathematical reasoning is central to artificial intelligence, with applications in education, code generation, and research-level mathematical discovery. Mathematical competitions highlight two problem types: theorem proving, requiring rigorous proofs, and answer construction, requiring creative generation and formal verification of mathematical objects. Existing research reveals that LLMs can tackle difficult answer-construction tasks but are prone to errors from hallucinations and unverifiable steps, while symbolic methods guarantee rigor but falter in creative answer construction. This raises a key understudied question: how to solve answer-construction problems while preserving both LLM creativity and mathematical rigor? To address this problem, 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 in Lean, and ConstructiveBench, a dataset of 3,640 formal answer-construction problems from math competitions. ECP is model agnostic and shows consistent improvements over pure LLM baselines: on the subset of PutnamBench for answer construction, ECP formally solves 6 out of 337 answer-construction problems end to end (up from 4 without ECP) using GPT-5 mini and DeepSeek-Prover-V2-7B. On ConstructiveBench, ECP achieves 33.1% end-to-end state-of-the-art accuracy (up from 32.5%), demonstrating its potential to advance formal mathematical reasoning by combining LLM conjecturing with formal verification. Our code and dataset are publicly available at GitHub (https://github.com/sunjia72/ECP) and Hugging Face (https://huggingface.co/datasets/sunjia72/ConstructiveBench).
Abstract（参考訳）: 数学的推論は人工知能の中心であり、教育、コード生成、研究レベルの数学的発見に応用されている。数学的競争は、定理証明、厳密な証明、解の構成、創造的な生成と数学的対象の形式的検証の2つの問題タイプを強調している。既存の研究によると、LLMは難解な解答作業に対処できるが、幻覚や検証不可能なステップの誤りを生じやすい。 LLMのクリエイティビティと数学的厳密さを両立させながら、どのように解答構成問題を解決するか? この問題に対処するために,LLMに基づく列挙とパターン駆動推論をリーンで証明した形式定理と統合したモジュール型ニューロシンボリック手法であるEnumerate-Conjecture-Prove (ECP) フレームワークと,数学コンペから3,640個の公式回答構築問題のデータセットであるConstructiveBenchを紹介する。 ECPはGPT-5 miniとDeepSeek-Prover-V2-7Bを用いて、337の回答構成問題のうち6つを公式に解決する。 ConstructiveBenchでは、ECPは33.1%の最先端の精度(32.5%から)を達成し、LCMの推論と形式的検証を組み合わせることで形式的な数学的推論を前進させる可能性を示している。私たちのコードとデータセットはGitHub(https://github.com/sunjia72/ECP)とHugging Face(https://huggingface.co/datasets/sunjia72/ConstructiveBench)で公開されています。

関連論文リスト

Solving Inequality Proofs with Large Language Models [46.71658812761115]
不等式証明は様々な科学・数学分野において不可欠である。これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
論文参考訳（メタデータ） (2025-06-09T16:43:38Z)
Mathesis: Towards Formal Theorem Proving from Natural Languages [40.397691467863886]
パイプライン処理の非公式な問題文を証明する最初のエンドツーエンド定理であるMathesisを開発した。これは、自然言語問題の形式化能力を高めるために強化学習を用いた最初のオートフォーマライザであるMathesis-Autoformalizerに貢献する。また、形式化された文から形式的な証明を生成するMathesis-Proverを提案する。
論文参考訳（メタデータ） (2025-06-08T09:04:14Z)
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)
PromptCoT: Synthesizing Olympiad-level Problems for Mathematical Reasoning in Large Language Models [59.920971312822736]
本稿では,高品質なオリンピアードレベルの数学問題を自動生成する新しい手法であるPromptCoTを紹介する。提案手法は,問題構築の背景にある数学的概念と理論的根拠に基づいて複雑な問題を合成する。提案手法は, GSM8K, MATH-500, AIME2024などの標準ベンチマークで評価され, 既存の問題生成手法を一貫して上回っている。
論文参考訳（メタデータ） (2025-03-04T06:32:30Z)
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)
PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
論文参考訳（メタデータ） (2020-10-06T15:47:53Z)

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

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