論文の概要: Training Language Models to Use Prolog as a Tool

• arxiv url: http://arxiv.org/abs/2512.07407v1
• Date: Mon, 08 Dec 2025 10:39:38 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-09 22:03:54.844014
• Title: Training Language Models to Use Prolog as a Tool
• Title（参考訳）: Prologをツールとして使うための言語モデルトレーニング
• Authors: Niklas Mellgren, Peter Schneider-Kamp, Lukas Galke Poech,
• Abstract要約: 検証可能な計算のための外部ツールとしてPrologを使用するための言語モデルを微調整する。 この結果から,形式的検証システムにおける基礎モデル推論は,安全クリティカルなアプリケーションに対する信頼性と監査性を大幅に向上させることがわかった。
• 参考スコア（独自算出の注目度）: 2.4305775926851334
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Ensuring reliable tool use is critical for safe agentic AI systems. Language models frequently produce unreliable reasoning with plausible but incorrect solutions that are difficult to verify. To address this, we investigate fine-tuning models to use Prolog as an external tool for verifiable computation. Using Group Relative Policy Optimization (GRPO), we fine-tune Qwen2.5-3B-Instruct on a cleaned GSM8K-Prolog-Prover dataset while varying (i) prompt structure, (ii) reward composition (execution, syntax, semantics, structure), and (iii) inference protocol: single-shot, best-of-N, and two agentic modes where Prolog is invoked internally or independently. Our reinforcement learning approach outperforms supervised fine-tuning, with our 3B model achieving zero-shot MMLU performance comparable to 7B few-shot results. Our findings reveal that: 1) joint tuning of prompt, reward, and inference shapes program syntax and logic; 2) best-of-N with external Prolog verification maximizes accuracy on GSM8K; 3) agentic inference with internal repair yields superior zero-shot generalization on MMLU-Stem and MMLU-Pro. These results demonstrate that grounding model reasoning in formal verification systems substantially improves reliability and auditability for safety-critical applications. The source code for reproducing our experiments is available under https://github.com/niklasmellgren/grpo-prolog-inference
• Abstract（参考訳）: 安全なエージェントAIシステムには、信頼性の高いツールの使用を保証することが重要です。 言語モデルは信頼できない推論を、検証が難しいが間違ったソリューションで生成することが多い。 そこで本研究では,Prologを外部ツールとして用いた微調整モデルを検証した。 Group Relative Policy Optimization (GRPO) を用いて、クリーン化GSM8K-Prolog-ProverデータセットにQwen2.5-3Bを微調整する。 即時構造; 即時構造; 即時構造 (二 報酬構成(執行、構文、意味論、構造)及び (iii)推論プロトコル:シングルショット、ベストオブN、2つのエージェントモードで、Prologは内部または独立して呼び出される。 我々の強化学習手法は教師付き微調整よりも優れており、3Bモデルでは0ショットMMLUの性能を7ショットに匹敵する精度で達成している。 私たちの発見は、こう示しています。 1) プログラムの構文及び論理のプロンプト、報酬及び推論形状の合同チューニング 2)外部Prolog検証によるNのベストプラクティスは,GSM8Kの精度を最大化する。 3) 内部補修によるエージェント推論はMMLU-StemとMMLU-Proに優れたゼロショット一般化をもたらす。 これらの結果から,形式的検証システムにおける基礎モデル推論は,安全クリティカルなアプリケーションに対する信頼性と監査性を大幅に向上させることが示された。 実験を再現するソースコードはhttps://github.com/niklasmellgren/grpo-prolog-inferenceで入手できる。

関連論文リスト

• NeuroProlog: Multi-Task Fine-Tuning for Neurosymbolic Mathematical Reasoning via the Cocktail Effect [0.12277343096128711]
  大規模言語モデル (LLM) は自然言語処理において高い性能を発揮するが、数学的推論では信頼性に欠ける。 我々は,数学用語の問題を実行可能なPrologプログラムにコンパイルすることで,検証可能な推論を保証する,ニューロシンボリックなフレームワークである textbfNeuroProlog を提案する。
  論文  参考訳（メタデータ） (2026-03-03T01:26:42Z)
• Prism: Efficient Test-Time Scaling via Hierarchical Search and Self-Verification for Discrete Diffusion Language Models [96.0074341403456]
  LLM推論を改善するための実用的な方法として、推論時計算が再導入されている。 テスト時間スケーリング(TTS)アルゴリズムの多くは、自動回帰デコーディングに依存している。 そこで我々は,dLLM のための効率的な TTS フレームワーク Prism を提案する。
  論文  参考訳（メタデータ） (2026-02-02T09:14:51Z)
• Improving Symbolic Translation of Language Models for Logical Reasoning [14.474630644806723]
  小さな言語モデル(LM)は、しばしば自然言語(NL)を一階述語論理(FOL)に変換するのに苦労する。 既存のアプローチは通常、これらのエラーを修正するために自己イテレーションに依存するが、そのような方法は基礎となるモデルの能力に大きく依存する。 本稿では,予測を述語生成とFOL翻訳の2段階に分割し,モデル動作の制御性を高めるインクリメンタル推論を提案する。
  論文  参考訳（メタデータ） (2026-01-14T12:47:14Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。 提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
  論文  参考訳（メタデータ） (2025-11-26T06:39:19Z)
• THOR: Tool-Integrated Hierarchical Optimization via RL for Mathematical Reasoning [25.605096023894834]
  大規模言語モデル (LLM) は数学的推論において顕著な進歩を遂げた。 最近の進歩にもかかわらず、既存の手法は3つの重要な課題に直面している。 我々はこれらの制限を克服するためにTHOR(Tool-Integrated Hierarchical Optimization via RL)を提案する。 提案手法は多種多様なモデルに対して強い一般化を示し,推論モデルと非推論モデルの両方で効果的に機能する。
  論文  参考訳（メタデータ） (2025-09-17T07:16:12Z)
• Fractional Reasoning via Latent Steering Vectors Improves Inference Time Compute [60.151643048803145]
  本稿では,推論時の推論強度を連続的に制御するフレームワークであるフラクショナル推論を提案する。 提案手法は, より深い推論を伴う潜在ステアリングベクトルを抽出し, 調整可能なスケーリング係数で再適用することによって機能する。 GSM8K、MATH500、GPQAの実験により、フラクショナル推論は様々な推論タスクやモデルのパフォーマンスを一貫して改善することを示した。
  論文  参考訳（メタデータ） (2025-06-18T21:15:59Z)
• Networks of Networks: Complexity Class Principles Applied to Compound AI Systems Design [63.24275274981911]
  多くの言語モデル推論コールからなる複合AIシステムは、ますます採用されている。 本研究では,提案した回答の生成と正当性検証の区別を中心に,ネットワークネットワーク(NoN)と呼ばれるシステムを構築した。 我々は,Kジェネレータを備えた検証器ベースの判定器NoNを導入し,"Best-of-K"あるいは"judge-based"複合AIシステムのインスタンス化を行う。
  論文  参考訳（メタデータ） (2024-07-23T20:40:37Z)
• Log Probabilities Are a Reliable Estimate of Semantic Plausibility in Base and Instruction-Tuned Language Models [50.15455336684986]
  意味的妥当性を評価するため,LogProbsの有効性と基本的なプロンプトを評価した。 LogProbsは、直接ゼロショットプロンプトよりも、より信頼性の高いセマンティックな妥当性を提供する。 我々は,プロンプトベースの評価の時代においても,LogProbsは意味的妥当性の有用な指標である,と結論付けた。
  論文  参考訳（メタデータ） (2024-03-21T22:08:44Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。 本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。 我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
  論文  参考訳（メタデータ） (2023-10-23T17:58:40Z)

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

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