論文の概要: SAT-RL: Training Language Models for Logical Reasoning with Symbolic Solvers

• arxiv url: http://arxiv.org/abs/2610.14402v1
• Date: Fri, 09 Oct 2026 23:46:15 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-15 21:06:15.044678
• Title: SAT-RL: Training Language Models for Logical Reasoning with Symbolic Solvers
• Title（参考訳）: SAT-RL:記号解を用いた論理推論のための学習言語モデル
• Abstract要約: 大規模言語モデル(LLM)は、数学的および論理的推論において高いパフォーマンスを達成しているが、それでも複雑さの呪いに悩まされている。 SAT-RLは,マルチターンツールの実行を通じて,シンボルソルバと対話するようにLLMを訓練する強化学習フレームワークである。
• 参考スコア（独自算出の注目度）: 2.2574964618006663
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large language models (LLMs) have achieved strong performance in mathematical and logical reasoning, yet they still suffer from the curse of complexity and struggle as problem difficulty increases with the number of constraint interactions and the size of the search space. In contrast, satisfiability solvers such as Z3 provide scalable and verifiable reasoning through constraint solving under formal theories, but lack the flexibility to interpret natural-language problem descriptions. In this work, we propose SAT-RL, a reinforcement-learning (RL) framework that trains LLMs to interact with symbolic solvers through multi-turn tool execution. SAT-RL leverages synthetic data generation with verifiable solutions, supervised warm-up on solver-augmented traces, and solver-grounded reinforcement learning with tool-aware rewards. Experiments show that SAT-RL substantially improves symbolic reasoning with tools on both in-domain and out-of-domain logic tasks. Our code is available on https://github.com/sunjia72/SAT-RL.
• Abstract（参考訳）: 大規模言語モデル (LLM) は数理的および論理的推論において高い性能を保っているが, 制約相互作用の数や探索空間のサイズが増加するにつれて, 問題の難しさが増大するにつれて, 複雑さと苦難の呪いに悩まされている。 対照的に、Z3のような満足度解決器は、形式理論の下での制約解決を通じてスケーラブルで検証可能な推論を提供するが、自然言語による問題記述を解釈する柔軟性は欠如している。 本研究では,マルチターンツールの実行により,LLMがシンボリック・ソルバと対話するように訓練する強化学習(RL)フレームワークSAT-RLを提案する。 SAT-RLは、検証可能なソリューションによる合成データ生成、ソルバ拡張トレースの教師付きウォームアップ、ツール認識報酬によるソルバ基底強化学習を利用する。 実験の結果、SAT-RLはドメイン内およびドメイン外の両方のロジックタスクのツールによるシンボリック推論を大幅に改善することが示された。 私たちのコードはhttps://github.com/sunjia72/SAT-RLで利用可能です。

関連論文リスト

• Formalize, Don't Optimize: The Heuristic Trap in LLM-Generated Combinatorial Solvers [52.23061619664667]
  大規模言語モデル(LLM)は直接推論によって複雑な問題を解くのに苦慮しているため、近年のニューロシンボリックシステムは、それを実行可能な解法を合成するためにますます利用している。 我々は,100の問題をベンチマークしたCP-SynC-XL(4,577インスタンス)を導入し,ネイティブアルゴリズム検索(Python),PythonソルバAPI(Python + OR-Tools)による制約モデリング,宣言的制約モデリングという3つのコンストラクションパラダイムを評価した。
  論文  参考訳（メタデータ） (2026-05-12T17:15:45Z)
• When Do Symbolic Solvers Enhance Reasoning in Large Language Models? [9.02964480989444]
  大きな推論モデル(LRM)は思考の長い鎖(CoT)を生成することによって複雑な推論タスクにおいて強い性能を達成する これはLLMのコード生成機能を利用して推論タスクを実行可能なコードに変換し、シンボリック・ソルバで解決する。 実験結果から,記号解法は暗黙的推論を必要とするが,十分な探索空間を必要とする場合にのみ有効であることがわかった。
  論文  参考訳（メタデータ） (2025-12-02T22:23:26Z)
• Making Mathematical Reasoning Adaptive [61.45161826629692]
  大規模言語モデル(LLM)における適応推論を実現するためのAdaRフレームワークを提案する。 AdaRは可変値によって論理的に等価なクエリを合成し、これらのデータに基づいてRLVRでモデルを訓練し、スプリアス論理をペナルライズする。 実験により, AdaRはロバスト性や一般化を向上し, 数学的推論の大幅な改善を実現していることが示された。
  論文  参考訳（メタデータ） (2025-10-06T09:30:05Z)
• Computational Thinking Reasoning in Large Language Models [69.28428524878885]
  計算思考モデル(CTM)は、計算思考パラダイムを大規模言語モデル(LLM)に組み込んだ新しいフレームワークである。 ライブコード実行は推論プロセスにシームレスに統合され、CTMが計算によって考えることができる。 CTMは、精度、解釈可能性、一般化可能性の観点から、従来の推論モデルとツール拡張ベースラインを上回っている。
  論文  参考訳（メタデータ） (2025-06-03T09:11:15Z)
• SATBench: Benchmarking LLMs' Logical Reasoning via Automated Puzzle Generation from SAT Formulas [33.329938165116886]
  本稿では,大規模言語モデルの論理的推論能力を評価するベンチマークであるSATBenchを紹介する。 SATBenchの各インスタンスはSAT式から生成され、LLMを使用してパズルに変換される。 実験によると、最強のモデルであるo4-miniでさえ、ハードUNSAT問題において65.0%の精度しか達成していない。
  論文  参考訳（メタデータ） (2025-05-20T17:00:22Z)
• Solving Zebra Puzzles Using Constraint-Guided Multi-Agent Systems [25.0042181817455]
  本稿では,大言語モデルとオフ・ザ・シェルフ定理証明器を統合したマルチエージェントシステムZPSを紹介する。 このシステムは、問題をより小さく管理可能な部分に分割することで、複雑なパズル解決作業に取り組む。 また,問題解の正当性を評価するための自動グリッドパズルグレーダを導入し,ユーザスタディで評価することで,自動グレーダが信頼性が高いことを示す。
  論文  参考訳（メタデータ） (2024-07-04T14:22:25Z)
• Language Models can be Logical Solvers [99.40649402395725]
  論理解法の推論過程を直接エミュレートする新しい言語モデルであるLoGiPTを導入する。 LoGiPTは、導出的ソルバの見えない推論過程を明らかにして精錬することから導かれる、新しく構築された命令チューニングデータセットに基づいて微調整される。
  論文  参考訳（メタデータ） (2023-11-10T16:23:50Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)

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

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