論文の概要: Step-Wise Formal Verification for LLM-Based Mathematical Problem Solving

• arxiv url: http://arxiv.org/abs/2505.20869v1
• Date: Tue, 27 May 2025 08:21:07 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-28 17:05:58.503323
• Title: Step-Wise Formal Verification for LLM-Based Mathematical Problem Solving
• Title（参考訳）: LLMに基づく数学的問題解決のためのステップワイズ形式検証
• Authors: Kuo Zhou, Lu Zhang,
• Abstract要約: LLM(Large Language Models)は、数学的な問題を解く上で、強大な能力を示す。 本稿では,形式化と批判を含むMATH-VFフレームワークを提案する。 我々は,MATH500とProcessBenchという,広く利用されている数学ベンチマークの枠組みを評価した。
• 参考スコア（独自算出の注目度）: 3.2233767737586674
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Large Language Models (LLMs) have demonstrated formidable capabilities in solving mathematical problems, yet they may still commit logical reasoning and computational errors during the problem-solving process. Thus, this paper proposes a framework, MATH-VF, which includes a Formalizer and a Critic, for formally verifying the correctness of the solutions generated by large language models. Our framework first utilizes a Formalizer which employs an LLM to translate a natural language solution into a formal context. Afterward, our Critic (which integrates various external tools such as a Computer Algebra System and an SMT solver) evaluates the correctness of each statement within the formal context, and when a statement is incorrect, our Critic provides corrective feedback. We empirically investigate the effectiveness of MATH-VF in two scenarios: 1) Verification: MATH-VF is utilized to determine the correctness of a solution to a given problem. 2) Refinement: When MATH-VF identifies errors in the solution generated by an LLM-based solution generator for a given problem, it submits the corrective suggestions proposed by the Critic to the solution generator to regenerate the solution. We evaluate our framework on widely used mathematical benchmarks: MATH500 and ProcessBench, demonstrating the superiority of our approach over existing approaches.
• Abstract（参考訳）: LLM(Large Language Models)は、数学的な問題を解く上で重大な能力を示したが、問題解決の過程で論理的推論や計算上の誤りを犯す可能性がある。 そこで本稿では,大規模言語モデルが生成する解の正当性を正式に検証するフレームワークMATH-VFを提案する。 我々のフレームワークはまず,LLMを用いて自然言語の解を形式的文脈に変換するフォーマライザを利用する。 その後、Crytic(Computer Algebra SystemやSMT solverなど様々な外部ツールを統合した)は、形式的文脈における各文の正当性を評価し、文が正しくない場合、修正フィードバックを提供する。 2つのシナリオにおけるMATH-VFの有効性を実証的に検討する。 1) 検証:MATH-VFを用いて、与えられた問題に対する解の正当性を決定する。 2) 補充: MATH-VF が LLM をベースとした解生成器が生成した解の誤りを与えられた問題に対して特定すると, 批判者が提案する補正提案を解生成器に送信して解を再生する。 我々は、MATH500とProcessBenchという、広く使われている数学ベンチマークの枠組みを評価し、既存のアプローチよりもアプローチの優位性を実証した。

関連論文リスト

• Learning by Analogy: Enhancing Few-Shot Prompting for Math Word Problem Solving with Computational Graph-Based Retrieval [22.865124583257987]
  同様に構造化された質問の類似性によって,大規模言語モデルの問題解決能力が向上することを示す。 具体的には、与えられた質問に類似した計算グラフを持つ問題の検索を頼りに、プロンプトの見本として機能する。 6つの数学単語問題データセットに対する実験結果から,提案手法の有効性が示された。
  論文  参考訳（メタデータ） (2024-11-25T15:01:25Z)
• Autoformulation of Mathematical Optimization Models Using LLMs [50.030647274271516]
  商用問題解決者のための自然言語記述から最適化モデルを作成するための自動アプローチを開発する。 本稿では,(1)問題依存仮説空間の定義,(2)不確実性の下でこの空間を効率的に探索すること,(3)定式化の正しさを評価すること,の3つの課題を同定する。
  論文  参考訳（メタデータ） (2024-11-03T20:41:38Z)
• ErrorRadar: Benchmarking Complex Mathematical Reasoning of Multimodal Large Language Models Via Error Detection [60.297079601066784]
  エラー検出におけるMLLMの能力を評価するために設計された最初のベンチマークであるErrorRadarを紹介する。 ErrorRadarはエラーステップ識別とエラー分類という2つのサブタスクを評価している。 2500の高品質なマルチモーダルK-12数学問題で構成され、実世界の学生相互作用から収集される。 GPT-4oの優れた性能は、まだ人間の評価に約10%遅れているため、大きな課題が残っている。
  論文  参考訳（メタデータ） (2024-10-06T14:59:09Z)
• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。 LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。 本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
  論文  参考訳（メタデータ） (2024-10-05T05:21:48Z)
• V-STaR: Training Verifiers for Self-Taught Reasoners [71.53113558733227]
  V-STaR はモデル生成解の正しさを判断する DPO を用いて検証器を訓練する。 複数のイテレーションでV-STaRを実行すると、徐々により良い推論器と検証器が得られる。
  論文  参考訳（メタデータ） (2024-02-09T15:02:56Z)
• Language Models for Business Optimisation with a Real World Case Study in Production Scheduling [3.224702011999591]
  大規模言語モデル (LLM) は、様々な言語関連タスクにまたがる卓越した性能を示している。 ビジネス最適化における問題定式化を自動化するためのLLMベースのフレームワークを提案する。
  論文  参考訳（メタデータ） (2023-09-22T23:45:21Z)
• Explaining Competitive-Level Programming Solutions using LLMs [3.560501183771493]
  競合レベルのプログラミング問題を解く上では性能が劣っているにもかかわらず、最先端のLLMは、ソリューションの説明と説明に強い能力を持っていることを示す。 我々の説明生成手法は、説明と分析を含む問題に対する構造化された解決説明を生成することができる。
  論文  参考訳（メタデータ） (2023-07-11T15:26:49Z)
• Highlighting Named Entities in Input for Auto-Formulation of Optimization Problems [0.0]
  本稿では,線形プログラム語問題を数学的定式化に変換する手法を提案する。 入力に名前付きエンティティを活用し、これらのエンティティをハイライトするためにインプットを拡張します。 提案手法は,NL4Optコンペティションへの応募者の中で最も高い精度を実現し,生成トラックにおける第1位を確保した。
  論文  参考訳（メタデータ） (2022-12-26T16:13:57Z)

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

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