論文の概要: Towards Reliable Proof Generation with LLMs: A Neuro-Symbolic Approach

• arxiv url: http://arxiv.org/abs/2505.14479v1
• Date: Tue, 20 May 2025 15:13:32 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-21 14:49:53.456303
• Title: Towards Reliable Proof Generation with LLMs: A Neuro-Symbolic Approach
• Title（参考訳）: LLMを用いた信頼性証明生成に向けて:ニューロシンボリックアプローチ
• Authors: Oren Sultan, Eitan Stern, Dafna Shahaf,
• Abstract要約: 大型言語モデル(LLM)は厳密な論理的推論と記号的推論を必要とする形式的ドメインと競合する。 本稿では,LLMの生成強度と構造成分を組み合わせ,この課題を克服するニューロシンボリックアプローチを提案する。
• 参考スコア（独自算出の注目度）: 14.213719696233934
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Large language models (LLMs) struggle with formal domains that require rigorous logical deduction and symbolic reasoning, such as mathematical proof generation. We propose a neuro-symbolic approach that combines LLMs' generative strengths with structured components to overcome this challenge. As a proof-of-concept, we focus on geometry problems. Our approach is two-fold: (1) we retrieve analogous problems and use their proofs to guide the LLM, and (2) a formal verifier evaluates the generated proofs and provides feedback, helping the model fix incorrect proofs. We demonstrate that our method significantly improves proof accuracy for OpenAI's o1 model (58%-70% improvement); both analogous problems and the verifier's feedback contribute to these gains. More broadly, shifting to LLMs that generate provably correct conclusions could dramatically improve their reliability, accuracy and consistency, unlocking complex tasks and critical real-world applications that require trustworthiness.
• Abstract（参考訳）: 大規模言語モデル(LLM)は、厳密な論理的推論と数学的証明生成のような記号的推論を必要とする形式的ドメインと競合する。 本稿では,LLMの生成強度と構造成分を組み合わせ,この課題を克服するニューロシンボリックアプローチを提案する。 概念実証として、幾何問題に焦点をあてる。 提案手法は,(1)類似した問題を検索し,それらの証明を用いて LLM を導出すること,(2) 形式検証器が生成した証明を評価し,フィードバックを提供することにより,モデルの誤りな証明の修正を支援すること,の2つの方法である。 提案手法は,OpenAIのo1モデル(58%～70%の改善)の検証精度を大幅に向上することを示した。 より広範に言えば、確実に正しい結論を生み出すLLMへの移行は、信頼性、正確性、一貫性を劇的に向上させ、複雑なタスクと信頼性を必要とするクリティカルな現実世界のアプリケーションをアンロックする。

関連論文リスト

• Can Large Language Models Learn Formal Logic? A Data-Driven Training and Evaluation Framework [2.9334627971166336]
  本稿では,大規模言語モデル(LLM)の論理的推論能力について検討する。 訓練されたLLMは、一連の仮定とゴールを入力として受け取り、その仮定からゴールを正式に導出する証明を出力として生成する。 トレーニングにとって重要な障害は、現実世界の証明が不足していることだ。
  論文  参考訳（メタデータ） (2025-04-28T19:25:29Z)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  証明の進捗を予測する手法であるLeanProgressを紹介します。 実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
  論文  参考訳（メタデータ） (2025-02-25T07:46:36Z)
• 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)
• Proof Automation with Large Language Models [6.587933406842906]
  大規模言語モデル(LLM)は、自然言語で非公式な証明を自動的に生成する可能性を示している。 本稿では,まず LLM に初期証明を生成することを促し,次に目標とする記号法を利用して低レベルの問題を反復的に修復する,新しい生成・修復手法である PALM を提案する。 その結果、PALMは他の最先端の手法よりも大幅に優れており、76.6%から180.4%の定理を証明できた。
  論文  参考訳（メタデータ） (2024-09-22T00:19:27Z)
• Deconfounded Causality-aware Parameter-Efficient Fine-Tuning for Problem-Solving Improvement of LLMs [12.48241058167222]
  大規模言語モデル(LLM)は、人間の指示に基づいて様々なタスクに取り組む際に、顕著な効率性を示した。 しかし、数学や物理学の限界など、推論を必要とするタスクに苦しむことが研究によって明らかになっている。 このことは、LLMが組み込み知識を本当に理解しているか、それとも、コンテンツに対する真の理解なしにトークン分布を複製することを学ぶだけなのかという疑問を提起する。 モデルの推論能力を高めるために,新しいパラメータ効率細調整法であるDecon Causal Adaptation (DCA)を提案する。
  論文  参考訳（メタデータ） (2024-09-04T13:17:09Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
  LLMの複雑な推論には2行のアプローチが採用されている。 1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。 他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。 具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
  論文  参考訳（メタデータ） (2023-11-16T11:26:21Z)

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

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