Fugu-MT 論文翻訳(概要): Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving

論文の概要: Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving

arxiv url: http://arxiv.org/abs/2505.04528v1
Date: Wed, 07 May 2025 16:02:14 GMT
ステータス: 翻訳完了
システム内更新日: 2025-05-08 19:07:36.142588
Title: Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving
Title（参考訳）: 定理証明を超えて - 形式的問題解決のための定式化、フレームワーク、ベンチマーク
Authors: Qi Liu, Xinhao Zheng, Renqiu Xia, Xingzhi Qi, Qinxiang Cao, Junchi Yan,
Abstract要約: 決定論的マルコフ決定過程として,問題解決の原理的定式化を提案する。また,既存のFTP環境を利用してプロセス検証問題解決を行う新しいフレームワークFPSを提案する。我々は, MATH500ベンチマークのサブセットの形式化であるFormalMath500, MiniF2F-Solving, PutnamBench-Solving, FTPベンチマークのMiniF2FとPutnamBenchの適応の3つのベンチマークを構築した。
参考スコア（独自算出の注目度）: 44.5694120006447
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: As a seemingly self-explanatory task, problem-solving has been a significant component of science and engineering. However, a general yet concrete formulation of problem-solving itself is missing. With the recent development of AI-based problem-solving agents, the demand for process-level verifiability is rapidly increasing yet underexplored. To fill these gaps, we present a principled formulation of problem-solving as a deterministic Markov decision process; a novel framework, FPS (Formal Problem-Solving), which utilizes existing FTP (formal theorem proving) environments to perform process-verified problem-solving; and D-FPS (Deductive FPS), decoupling solving and answer verification for better human-alignment. The expressiveness, soundness and completeness of the frameworks are proven. We construct three benchmarks on problem-solving: FormalMath500, a formalization of a subset of the MATH500 benchmark; MiniF2F-Solving and PutnamBench-Solving, adaptations of FTP benchmarks MiniF2F and PutnamBench. For faithful, interpretable, and human-aligned evaluation, we propose RPE (Restricted Propositional Equivalence), a symbolic approach to determine the correctness of answers by formal verification. We evaluate four prevalent FTP models and two prompting methods as baselines, solving at most 23.77% of FormalMath500, 27.47% of MiniF2F-Solving, and 0.31% of PutnamBench-Solving.
Abstract（参考訳）: 一見自己説明的なタスクとして、問題解決は科学と工学の重要な構成要素である。しかし、問題解決そのものの一般的な具体的な定式化が欠落している。近年、AIベースの問題解決エージェントが開発され、プロセスレベルの検証可能性の需要は急速に増加しているが、未調査である。これらのギャップを埋めるために、決定論的マルコフ決定過程としての問題解決の原理的定式化、既存のFTP(形式的定理証明)環境を利用してプロセス検証を行うFPS(Formal Problem-Solving)、D-FPS(Deductive FPS)、解と解の解と解の解の解法を、より優れたヒューマンアライメントのために分離するD-FPS(Deductive FPS)を提案する。フレームワークの表現性、健全性、完全性が証明されている。我々は, MATH500ベンチマークのサブセットの形式化であるFormalMath500, MiniF2F-Solving, PutnamBench-Solving, FTPベンチマークのMiniF2FとPutnamBenchの適応の3つのベンチマークを構築した。 RPE(Restricted Propositional Equivalence, 限定命題等価性)は, 正解の正解を形式的検証によって決定する記号的手法である。代表的な4つのFTPモデルと2つのプロンプトメソッドをベースラインとして評価し、少なくとも23.77%のFormalMath500、27.47%のMiniF2F-Solving、0.31%のPatnamBench-Solvingを解いた。

関連論文リスト

CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics [45.32204834230928]
100の問題をまとめた総合的なベンチマークであるCombiBenchを紹介します。 CombiBenchは2000年以降の問題解決に適している(画像を含むIMO 2004 P3を除く)。また、フォーマル数学のための包括的で標準化された評価フレームワーク「ファイン・エバル」も提供する。
論文参考訳（メタデータ） (2025-05-06T04:32:17Z)
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)
Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
論文参考訳（メタデータ） (2024-10-21T08:04:21Z)
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)
Lila: A Unified Benchmark for Mathematical Reasoning [59.97570380432861]
LILAは、23の多様なタスクと4次元からなる統一的な数学的推論ベンチマークである。我々は,Pythonプログラムの形式でタスク命令とソリューションを収集することにより,20のデータセットベンチマークを拡張してベンチマークを構築した。 LILAで訓練された汎用数学的推論モデルであるBHASKARAを紹介する。
論文参考訳（メタデータ） (2022-10-31T17:41:26Z)
Formally Verified Solution Methods for Infinite-Horizon Markov Decision Processes [7.538482310185133]
確率論の既存の形式化に基づいて、無限水平問題における期待される全報酬基準を解析する。我々の発展はベルマン方程式を形式化し、最適なポリシーが存在する条件を与える。我々のシステムは最先端のシステムと競合し、さらに性能も向上できることを示す。
論文参考訳（メタデータ） (2022-06-05T13:03:34Z)
Logically Consistent Loss for Visual Question Answering [66.83963844316561]
ニューラルネットワークに基づく視覚質問応答(VQA)の現在の進歩は、同じ分布(すなわち、d)の仮定による一貫性を保証することができない。マルチタスク学習フレームワークにおける論理的一貫した損失を定式化することにより,この問題に対処するための新しいモデルに依存しない論理制約を提案する。実験により、提案された損失公式とハイブリッドバッチの導入により、一貫性が向上し、性能が向上することを確認した。
論文参考訳（メタデータ） (2020-11-19T20:31:05Z)

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

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