論文の概要: LLM-Assisted Bi-Approximate CHC Solving
- arxiv url: http://arxiv.org/abs/2610.23771v1
- Date: Fri, 16 Oct 2026 17:08:03 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-21 06:32:45.337097
- Title: LLM-Assisted Bi-Approximate CHC Solving
- Title（参考訳）: LLM-Assisted Bi-Approximate CHC Solving (特集 バイオサイバネティックスとバイオサイバネティックス)
- Abstract要約: 我々は大言語モデル(LLM)を用いて導出パワーアンダー近似(DPU)を生成する。
HornCraftは、過剰近似のための不変生成と低近似のためのDPU生成を組み合わせたCHC解法である。
260の線形および整数型CHC-COMPベンチマークは30分間のスペーサー実行で未解決のまま残され、ホーンクラフトは228インスタンスの検証を返却した。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Constrained Horn clause (CHC) solvers often struggle to discover deep counterexamples whose derivations may require extensive rule unfolding. Although large language models (LLMs) can propose long-range symbolic relations, prior work on formally checked LLM-assisted verification has mainly focused on generating inductive invariants and concrete traces. We exploit this broader capability through Derivation Power Under-approximations (DPUs). Each DPU is a solver-certified under-approximation of the relation induced by a multi-step CHC derivation. An LLM proposes each DPU with symbolic intermediate-state witnesses that enable SMT validation without introducing additional quantifiers. Validated DPUs can be composed and reused soundly. Building on this mechanism, our LLM-assisted framework HornCraft combines invariant generation for over-approximation with DPU generation for under-approximation in CHC solving. On 260 linear and nonlinear integer-arithmetic CHC-COMP benchmarks left unresolved by a 30-minute Spacer run, HornCraft returns certified verdicts for 228 instances. It certifies 42 instances as unsafe, compared with 22 when DPU construction and reuse are disabled.
- Abstract（参考訳）: 制約されたホーン節(CHC)の解法は、導出が広い規則の展開を必要とするかもしれない深い反例を発見するのに苦労することが多い。
大規模言語モデル (LLMs) は長距離の記号関係を提案できるが, LLM支援検証の先行研究は主に帰納的不変量や具体的なトレースの生成に重点を置いている。
我々は、導出パワーアンダー近似(DPU)により、このより広い能力を利用する。
各DPUは、多段階CHC誘導体によって誘導される関係の解法認定下近似である。
LLMは、追加の量化器を導入することなくSMT検証を可能にする象徴的な中間状態証人を持つ各DPUを提案する。
検証済みのDPUは、健全に合成および再利用することができる。
この機構に基づいて,我々のLLM支援フレームワークであるHhornCraftは,CHCの解法において,過剰近似の不変生成と低近似のDPU生成を併用する。
260の線形および非線形整数パラメータCHC-COMPベンチマークは30分間のスペーサー実行によって未解決のまま残され、ホーンクラフトは228のインスタンスに対して証明された判定を返却した。
DPUの構築と再利用を無効にする22のインスタンスと比較して、42のインスタンスを安全でないと認定する。
関連論文リスト
- LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。
本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
論文 参考訳（メタデータ） (2026-06-02T08:16:42Z) - CktFormalizer: Autoformalization of Natural Language into Circuit Representations [23.44745731124114]
CktFormalizerは、Lean 4.0に組み込まれた依存型HDLを通じてハードウェア生成をリダイレクトするフレームワークである。
VerilogEval(156問題)、RTLLM(50問題)、ResBench(56問題)では、CktFormalizerは直接Verilog生成と競合するシミュレーションパスレートを達成する。
論文 参考訳（メタデータ） (2026-05-08T14:20:06Z) - Latent-Condensed Transformer for Efficient Long Context Modeling [60.72493959155964]
大規模言語モデルに対するLCA(Latent-Condensed Attention)を提案する。
LCAはMLAの潜伏空間内のコンテキストを凝縮し、表現はセマンティック潜伏ベクトルと位置キーに切り離される。
LCAは、最大2.5$times$プリフィルスピードアップと128Kコンテキストでの90%のKVキャッシュ削減を実現している。
論文 参考訳（メタデータ） (2026-04-14T08:40:31Z) - PLUME: Latent Reasoning Based Universal Multimodal Embedding [52.35354073629127]
ユニバーサルマルチモーダル埋め込み(UME)は、異種入力を単一のモデルで共有検索空間にマッピングする。
最近のアプローチでは、埋め込みを抽出する前に明確なチェーン・オブ・シント(CoT)論理を生成することにより、UMEを改善している。
PLUMEは,言語化されたCoTを連続的潜伏状態の短時間の自己回帰ロールアウトに置き換えることで,UMEを進化させる潜在的推論フレームワークである。
論文 参考訳（メタデータ） (2026-04-02T14:04:53Z) - APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [16.8655558789989]
本稿では,自動定理証明のためのモデルに依存しないエージェントフレームワークであるAPOLLO (Automated PrOof repair viaLLM and Lean cOllaboration)を提案する。
エージェントのセットは、証明を分析し、シンタックスのエラーを修正し、リーンを使って証明の誤りを特定し、失敗するサブレムマを分離し、自動化されたソルバを利用し、残りの目標に対してLLMを呼び出す。
この結果から,LLM出力を目標としたコンパイラ誘導型修復は,効率と正確性の両方において劇的に向上することが示された。
論文 参考訳（メタデータ） (2025-05-09T03:38:31Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。