論文の概要: Extending SMT Solving with Non-Ground Clause Learning
- arxiv url: http://arxiv.org/abs/2609.11509v1
- Date: Thu, 10 Sep 2026 13:17:14 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-11 23:53:35.36597
- Title: Extending SMT Solving with Non-Ground Clause Learning
- Title（参考訳）: 非球形クロース学習による拡張SMT解法
- Abstract要約: 本稿では,地上のインスタンス化,CDCL(T)スタイルのルール,非地上衝突解析からなる計算法を提案する。
我々の計算は、CDCL(T)スタイルのSMT解決、インスタンスベースプロシージャの範囲、非地下節学習に共通した設定を提供する。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Quantifier instantiation is currently the main approach to non-ground SMT solving: solvers generate ground instances and solve the resulting ground SMT problems with CDCL(T)-style reasoning. When a conflict is found, conflict analysis learns only a ground clause, even though the conflict comes from instances of non-ground clauses. Yet non-ground reasoning can give exponentially shorter proofs than purely ground reasoning. We propose a calculus that consists of ground instantiations, CDCL(T)-style rules, and non-ground conflict analysis. The solver reasons on ground instances, but the resolution steps of conflict analysis are performed on their original non-ground clauses. This produces learned clauses that are typically more general than the ground conflict. With a suitable strategy, the learned clauses are even non-redundant. We also show how chronological backtracking can be included in SMT solving. Our calculus gives a common setting for CDCL(T)-style SMT solving, a range of instantiation-based procedures, and non-ground clause learning, and we prove that it simulates CDCL, SCL(FOL), SCL(T), and even Resolution.
- Abstract（参考訳）: 量子化器のインスタンス化は、現在、非基底SMT解決の主なアプローチである: ソルバは、基底インスタンスを生成し、結果として生じる基底SMT問題をCDCL(T)スタイルの推論で解決する。
紛争が見つかると、紛争分析は、紛争が非基底的条項の事例から生じたとしても、基礎的条項のみを学習する。
しかし、非基底的推論は純粋に基底的推論よりも指数関数的に短い証明を与えることができる。
本稿では,地上のインスタンス化,CDCL(T)スタイルのルール,非地上衝突解析からなる計算法を提案する。
しかし, 紛争解析の解決手順は, 原文以外の節で実施されている。
これは典型的には地上紛争よりも一般的である学習された節を生成する。
適切な戦略では、学習された節は非冗長である。
また,SMT法では,時間的バックトラックが有効であることを示す。
本計算は,CDCL(T)スタイルのSMT解法,インスタンスベースプロシージャ,非地下節学習に共通する設定を与え,CDCL,SCL(FOL),SCL(T),さらには分解能をシミュレートすることを示した。
関連論文リスト
- SALA: Semantic-Aware Logical Alignment for Complex Reasoning in In-Context Learning [61.13104919370034]
セマンティック・アウェア・論理アライメント・フレームワークであるSALAを提案する。
固定在庫に頼る代わりに、SALAはタスク固有の推論操作を自動的に学習する。
その後、これらの操作を連続的なセマンティック空間に埋め込み、動的時間ワープを使用して推論シーケンスを整列する。
論文 参考訳（メタデータ） (2026-09-02T09:12:03Z) - Training LLMs for Divide-and-Conquer Reasoning Elevates Test-Time Scalability [129.1296673737603]
大規模言語モデル(LLM)は、ステップ・バイ・ステップ・チェーン・オブ・シークレット(CoT)推論を通じて強力な推論能力を示している。
潜在的には、解のより効率的な探索を容易にするために複雑な問題をサブプロブレムに分解するDAC推論がある。
本稿では,DAC型推論能力を高めるために,エンドツーエンド強化学習(RL)フレームワークを提案する。
論文 参考訳（メタデータ） (2026-02-02T18:54:54Z) - Reason-KE++: Aligning the Process, Not Just the Outcome, for Faithful LLM Knowledge Editing [63.96040994220329]
SFTに基づく手法、例えばReason-KEは「偽りのギャップ」に悩まされている。
このギャップにより、LLMの強力なパラメトリック先行は、新しい文脈事実をオーバーライドすることができる。
本稿では,プロセスレベルの忠実性を具現化するSFT+RLフレームワークReason-KE++を提案する。
論文 参考訳（メタデータ） (2025-11-16T15:49:01Z) - Thinking Before You Speak: A Proactive Test-time Scaling Approach [54.8205006555199]
emphThinking Before You Speak (TBYS)という名前の推論フレームワークとして、私たちのアイデアを実装しています。
インテリジェンス生成のためのコンテキスト内サンプルを自動的に収集・フィルタリングするパイプラインを設計する。
挑戦的な数学的データセットの実験は、TBYSの有効性を検証する。
論文 参考訳（メタデータ） (2025-08-26T03:43:32Z) - Grounding Rule-Based Argumentation Using Datalog [3.1457219084519004]
ASPIC+は、AIのルールベースの議論のための主要な一般的なフレームワークの1つである。
本稿では,解析過程の正しさを保ちながら,接地の大きさを管理可能なインテリジェント接地手法を提案する。
また, ASPIC+形式に特有な簡易化を提案し, 推論プロセスに影響を与えない規則の根拠付けを避ける。
論文 参考訳（メタデータ） (2025-08-14T17:57:32Z) - Syzygy of Thoughts: Improving LLM CoT with the Minimal Free Resolution [59.39066657300045]
CoT(Chain-of-Thought)は、問題を逐次ステップに分解することで、大きな言語モデル(LLM)の推論を促進する。
思考のシジー(Syzygy of Thoughts, SoT)は,CoTを補助的,相互関連的な推論経路を導入して拡張する新しいフレームワークである。
SoTはより深い論理的依存関係をキャプチャし、より堅牢で構造化された問題解決を可能にする。
論文 参考訳（メタデータ） (2025-04-13T13:35:41Z) - Large Language Models as an Indirect Reasoner: Contrapositive and Contradiction for Automated Reasoning [74.90592233107712]
本稿では,直接推論 (DR) と間接推論 (IR) を並列な複数の推論経路として考慮し,最終解を導出する直接間接推論 (DIR) 手法を提案する。
我々のDIR法は単純だが有効であり、既存のCoT法と簡単に統合できる。
論文 参考訳（メタデータ） (2024-02-06T03:41:12Z) - DCR: Divide-and-Conquer Reasoning for Multi-choice Question Answering with LLMs [9.561022942046279]
大規模言語モデル(LLM)の推論能力を高めるため,DCR(Divide and Conquer Reasoning)を提案する。
まず、信頼性スコア(mathcalCS$)に基づいて質問を2つのサブセットに分類する。
特に,質問を信頼性スコア(mathcalCS$)に基づいて2つのサブセットに分類する。
論文 参考訳（メタデータ） (2024-01-10T14:38:46Z) - SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning [0.3867363075280543]
SCL(FOL)は等式のない一階述語論理の重ね合わせにより非冗長節の導出をシミュレートできることを示す。
重畳に基づく推論は、固定縮小順序付けに対して行われる。
論文 参考訳（メタデータ） (2023-05-22T11:12:39Z) - Too much information: CDCL solvers need to forget and perform restarts [0.0]
競合駆動型節学習(CDCL)は命題論理の満足度問題を解くための極めて成功したパラダイムである。
この論文は、節学習がランタイムを改善するだけでなく、それを劇的に劣化させることがあることを非常に驚くべきことに示します。
論文 参考訳（メタデータ） (2022-02-01T10:16:04Z) - A Deep Dive into Conflict Generating Decisions [3.222802562733787]
私たちは、Satisfiability(SAT)問題を解決するためにConflict Driven Clause Learningを使用します。
そこで我々は,CDCLがコンフリクトから節を学習することを示した。
我々は、mc決定の学習節から一部の変数の選択優先度を下げる新しい決定戦略として、共通推論変数還元(CRVR)を開発した。
論文 参考訳（メタデータ） (2021-05-10T18:17:52Z) - On the Effect of Learned Clauses on Stochastic Local Search [0.0]
SATソルバでは、競合駆動型節学習(CDCL)と局所探索(SLS)が使用されている。
多数の正しいリテラルを持つ節がSLSのランタイムに有益であることを実験的に実証した。
我々は、前処理のステップとして高品質な節を追加する最も有益な戦略を導出する。
論文 参考訳（メタデータ） (2020-05-07T13:33:16Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。