論文の概要: Verifiable LLM-Guided Focal SMT Solving for Quantified Arrays

• arxiv url: http://arxiv.org/abs/2610.39435v1
• Date: Thu, 29 Oct 2026 06:13:59 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-11-01 01:32:10.049453
• Title: Verifiable LLM-Guided Focal SMT Solving for Quantified Arrays
• Title（参考訳）: 量子化アレイのLLM誘導型音声SMT解法
• Abstract要約: 大規模な言語モデルは、形式的なアーティファクトで有用な意味構造を識別することができるが、そのアウトプットは証明や解決者決定として信頼できない。 LLMがより狭義の解答可能なインタフェースによって形式的推論システムを導くことができるかどうかを考察する。 本稿では,LLMが小さなセマンティック・フォーカス・セット(地下項/制約)を提案するのに対して,従来のSMTソルバは唯一の証明エンジンであり,全ての結果を証明できるフレームワークを提案する。
• 参考スコア（独自算出の注目度）: 10.767268261124515
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Large language models can often identify useful semantic structure in formal artifacts, but their outputs cannot be trusted as proofs or solver decisions. We study whether LLMs can instead guide formal reasoning systems through a narrow, solver-verifiable interface. We instantiate this idea in quantified array SMT solving, where modern instantiation-based techniques can fail when key ground terms and equalities are hidden by auxiliary variables, axiom guards, and nested array terms. We observe that many instances are largely driven by a small set of focal ground terms or constraints, similar to the backdoor sets in SAT solving. Building on this, we present LinguaArray, a framework where an LLM proposes a small Semantic Focus Set (ground terms/constraints), while a conventional SMT solver remains the sole proof engine and certifies all results. LinguaArray uses these LLM-suggested, solver-validated finite sets to significantly enhance solver capability, solving additional satisfiable and unsatisfiable instances that the backend alone fails to solve. It interacts within a finite time and then falls back to the backend solver to mitigate potential regressions. Evaluation on 1015 SMT-LIB instances across five logics under 1200s timeout (including LLM latency) shows that LinguaArray solves up to 69.1% of instances and increases solved-instance counts by 105%--397% over the corresponding backends.
• Abstract（参考訳）: 大規模な言語モデルは、形式的なアーティファクトで有用な意味構造を識別することができるが、そのアウトプットは証明や解決者決定として信頼できない。 LLMがより狭義の解答可能なインタフェースによって形式的推論システムを導くことができるかどうかを考察する。 量子化アレイSMT法では、鍵基底項と等式が補助変数、公理ガード、ネスト配列項によって隠された場合に、現代のインスタンス化に基づく手法が失敗する可能性がある。 多くのケースは、SAT解決におけるバックドアセットと同様、焦点付き基底項や制約の小さなセットによって主に駆動される。 LLMが小さなセマンティック・フォーカス・セット(地上用語/制約)を提案するフレームワークであるLinguaArrayについて述べる。 LinguaArray はこれらの LLM-suggested,solvr-validated finite set を用いてソルバ能力を大幅に向上させ、バックエンドだけでは解決できない、満足し難い追加のインスタンスを解決している。 有限時間以内に相互作用し、その後、潜在的な回帰を緩和するためにバックエンドのソルバにフォールバックする。 1200sタイムアウト(LLMレイテンシを含む)以下の5つのロジックで1015のSMT-LIBインスタンスを評価すると、LinguaArrayは最大69.1%のインスタンスを解決し、対応するバックエンドに対して105%--397%の削減を実現している。

関連論文リスト

• SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification [2.6426981014417046]
  我々は、意味マッピングと正式な認証を分離するLLM支援SMTフレームワークであるSOVERを紹介する。 また、NLEquiv-150は100の等価性と50の故意に非等価な非線形改質ペアの公的なベンチマークである。
  論文  参考訳（メタデータ） (2026-09-01T05:05:12Z)
• 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)
• How LLMs Fail and Generalize in RTL Coding for Hardware Design? [56.361436215029045]
  我々は,認知理論に触発された問題解決性に基づく新しい誤り分類法を導入する。 我々の分類学は、障害を構文、意味、解決可能な機能、解決不可能な機能タイプに分類する。
  論文  参考訳（メタデータ） (2026-04-26T14:34:49Z)
• LLM-Guided Quantified SMT Solving over Uninterpreted Functions [10.767268261124515]
  非線形実算術上の非解釈関数 (UF) の量子式は、Satifiability Modulo Theories (SMT) の解法に根本的な課題をもたらす。 本稿では,UFインスタンス化のセマンティックガイダンスを提供するために,大規模言語モデルを活用するフレームワークであるAquaForteを紹介する。 提案手法は,制約分離によって計算式を前処理し,構造化プロンプトを用いてLLMから数学的推論を抽出し,従来のSMTアルゴリズムと統合する。
  論文  参考訳（メタデータ） (2026-01-08T07:40:37Z)
• LM4Opt-RA: A Multi-Candidate LLM Framework with Structured Ranking for Automating Network Resource Allocation [0.7933039558471408]
  我々は,複雑な解析的および数学的推論タスクに,文脈的理解が不要であることに対処する。 既存のベンチマークデータセットは、動的な環境、変数、不均一な制約でそのような問題の複雑さに対処できない。 NL4RAは、LP、ILP、MILPとして定式化された50のリソース割り当て最適化問題からなるキュレートデータセットである。 次に,パラメータ数が異なるオープンソースのLLMの性能評価を行った。
  論文  参考訳（メタデータ） (2025-11-13T23:19:43Z)
• 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)
• Small Language Models Fine-tuned to Coordinate Larger Language Models improve Complex Reasoning [41.03267013352519]
  大きな言語モデル(LLM)は、印象的な推論能力を示すチェーン・オブ・シントを生成するように促された。 本稿では、分解生成器を用いて複雑な問題をより少ない推論ステップを必要とするサブプロブレムに分解するDaSLaMを紹介する。 本稿では,DaSLaMがスケール関数としての解の能力に制限されないことを示す。
  論文  参考訳（メタデータ） (2023-10-21T15:23:20Z)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  本研究では,大規模言語モデル (LLM) の推論能力を向上させるために,新しい満足度支援言語モデリング (SatLM) 手法を提案する。 我々はLLMを用いて命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終解を導出する。 我々はSATLMを8つの異なるデータセット上で評価し、命令パラダイムにおいてプログラム支援されたLMよりも一貫して優れていることを示す。
  論文  参考訳（メタデータ） (2023-05-16T17:55:51Z)
• PAL: Program-aided Language Models [112.94785609781503]
  自然言語問題を理解するために,プログラム支援言語モデル(PaL)を提案する。 PaLはソリューションステップをPythonインタプリタのようなプログラムランタイムにオフロードする。 私たちは12のベンチマークで新しい最先端の結果を設定しました。
  論文  参考訳（メタデータ） (2022-11-18T18:56:13Z)

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

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