Fugu-MT 論文翻訳(概要): LLM-Guided Quantified SMT Solving over Uninterpreted Functions

論文の概要: LLM-Guided Quantified SMT Solving over Uninterpreted Functions

arxiv url: http://arxiv.org/abs/2601.04675v1
Date: Thu, 08 Jan 2026 07:40:37 GMT
ステータス: 翻訳完了
システム内更新日: 2026-01-09 17:01:53.082196
Title: LLM-Guided Quantified SMT Solving over Uninterpreted Functions
Title（参考訳）: 非解釈関数上のLLM誘導量子SMT解法
Authors: Kunhang Lv, Yuhang Dong, Rui Han, Fuqi Jia, Feifei Ma, Jian Zhang,
Abstract要約: 非線形実算術上の非解釈関数 (UF) の量子式は、Satifiability Modulo Theories (SMT) の解法に根本的な課題をもたらす。本稿では,UFインスタンス化のセマンティックガイダンスを提供するために,大規模言語モデルを活用するフレームワークであるAquaForteを紹介する。提案手法は,制約分離によって計算式を前処理し,構造化プロンプトを用いてLLMから数学的推論を抽出し,従来のSMTアルゴリズムと統合する。
参考スコア（独自算出の注目度）: 10.767268261124515
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: Quantified formulas with Uninterpreted Functions (UFs) over non-linear real arithmetic pose fundamental challenges for Satisfiability Modulo Theories (SMT) solving. Traditional quantifier instantiation methods struggle because they lack semantic understanding of UF constraints, forcing them to search through unbounded solution spaces with limited guidance. We present AquaForte, a framework that leverages Large Language Models to provide semantic guidance for UF instantiation by generating instantiated candidates for function definitions that satisfy the constraints, thereby significantly reducing the search space and complexity for solvers. Our approach preprocesses formulas through constraint separation, uses structured prompts to extract mathematical reasoning from LLMs, and integrates the results with traditional SMT algorithms through adaptive instantiation. AquaForte maintains soundness through systematic validation: LLM-guided instantiations yielding SAT solve the original problem, while UNSAT results generate exclusion clauses for iterative refinement. Completeness is preserved by fallback to traditional solvers augmented with learned constraints. Experimental evaluation on SMT-COMP benchmarks demonstrates that AquaForte solves numerous instances where state-of-the-art solvers like Z3 and CVC5 timeout, with particular effectiveness on satisfiable formulas. Our work shows that LLMs can provide valuable mathematical intuition for symbolic reasoning, establishing a new paradigm for SMT constraint solving.
Abstract（参考訳）: 非線形実算術上の非解釈関数 (UF) の量子式は、Satifiability Modulo Theories (SMT) の解法に根本的な課題をもたらす。従来の量化器のインスタンス化法は、UF制約のセマンティックな理解が欠如しているため、限定的なガイダンスで非有界な解空間を探索せざるを得ない。本稿では,大言語モデルを利用して,制約を満たす関数定義のインスタンス化候補を生成することで,UFインスタンス化のセマンティックガイダンスを提供するフレームワークAquaForteについて述べる。提案手法は,制約分離により計算式を前処理し,構造化プロンプトを用いてLLMから数学的推論を抽出し,適応インスタンス化により従来のSMTアルゴリズムと統合する。 LLM誘導インスタンス化 SAT が元の問題を解決する一方、UNSAT は反復的洗練のための排他的節を生成する。完全性は、学習された制約で強化された伝統的な解法にフォールバックすることで維持される。 SMT-COMPベンチマークの実験的評価は、AquaForteがZ3やCVC5のような最先端の解法をタイムアウトする多くのケースを解くことを示した。我々の研究は、LLMが記号的推論に有用な数学的直観を提供し、SMT制約解決のための新しいパラダイムを確立することを示している。

関連論文リスト

Unlocking Symbol-Level Precoding Efficiency Through Tensor Equivariant Neural Network [84.22115118596741]
シンボルレベルのプリコーディングにおいて,推論の複雑さの低いエンドツーエンドディープラーニング(DL)フレームワークを提案する。提案手法は,従来の手法よりも約80倍の高速化を実現しつつ,SLPの大幅な性能向上を達成できることを示す。
論文参考訳（メタデータ） (2025-10-02T15:15:50Z)
Do LLMs Dream of Discrete Algorithms? [0.7646713951724011]
大規模言語モデル(LLM)は、人工知能の風景を急速に変化させてきた。確率的推論への依存は、厳密な論理的推論を必要とする領域における有効性を制限する。本稿では,論理ベースの推論モジュールでLLMを増強するニューロシンボリックアプローチを提案する。
論文参考訳（メタデータ） (2025-06-29T22:03:01Z)
Worst-Case Symbolic Constraints Analysis and Generalisation with Large Language Models [7.658134651527103]
最悪のケースのシンボリック制約分析では、最悪のケースのプログラムの実行を特徴付けるシンボリック制約を推論する必要がある。我々は,現在最先端の大規模言語モデル (LLM) でさえ,このタスクに直接適用した場合に苦労することを示す。我々は,より小さな具体的入力サイズに対する最悪の制約を計算する,革新的ニューロシンボリックアプローチであるWARPを提案する。
論文参考訳（メタデータ） (2025-06-09T19:33:30Z)
LLM-Symbolic Integration for Robust Temporal Tabular Reasoning [69.27153114778748]
本研究では,システムおよび制御された評価のための合成データセットであるTempTabQA-Cを紹介する。この構造化アプローチにより、LLM(Large Language Models)はsqlクエリの生成と実行を可能にし、一般化とバイアス軽減の強化を行う。
論文参考訳（メタデータ） (2025-06-06T05:14:04Z)
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)
Gap-Filling Prompting Enhances Code-Assisted Mathematical Reasoning [0.0]
パターン・オブ・シント(CoT)とプログラム・オブ・シント(PoT)ファインチューニング(PoT)は、LPMの知識を小さな言語モデル(SLM)に転送する一般的な方法である。本稿では,SLMの問題解決プロセスを強化するために,新たな2段階のプロンプト戦略であるGap-Filling Prompting(GFP)を紹介する。
論文参考訳（メタデータ） (2024-11-08T08:52:59Z)
SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
本研究では,大規模言語モデル (LLM) の推論能力を向上させるために,新しい満足度支援言語モデリング (SatLM) 手法を提案する。我々はLLMを用いて命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終解を導出する。我々はSATLMを8つの異なるデータセット上で評価し、命令パラダイムにおいてプログラム支援されたLMよりも一貫して優れていることを示す。
論文参考訳（メタデータ） (2023-05-16T17:55:51Z)
Exploring Viable Algorithmic Options for Learning from Demonstration (LfD): A Parameterized Complexity Approach [0.0]
本稿では,パラメータ化複雑性解析を用いて,アルゴリズムの選択肢を体系的に探索する方法を示す。環境、実演、ポリシーに対する多くの(しばしば同時に)制限に対して、我々の問題は、一般的にも、あるいは相対的に、効率的に解決できないことを示す。
論文参考訳（メタデータ） (2022-05-10T15:54:06Z)
Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文参考訳（メタデータ） (2022-04-28T17:57:33Z)

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

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