論文の概要: 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で入手できる。

関連論文リスト

• 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)

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

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