論文の概要: SLED-IFV: Solver-Validated LLM-Guided Decomposition for Scalable Hardware Information-Flow Verification
- arxiv url: http://arxiv.org/abs/2609.25637v1
- Date: Tue, 22 Sep 2026 03:48:28 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-23 18:04:04.197443
- Title: SLED-IFV: Solver-Validated LLM-Guided Decomposition for Scalable Hardware Information-Flow Verification
- Title（参考訳）: SLED-IFV:スケーラブルハードウェア情報フロー検証のためのLLM誘導分解法
- Abstract要約: 形式的ハードウェア情報フロー検証(IFV)は、秘密に依存したタイミングと制御動作に対する強力な保証を提供する。
我々は,自己構成型IFVにおいて,実装複雑性と帰納的複雑性の2つの再帰的証明障壁を同定した。
機能的単純化と関係性強化という2つの意味的証明分解形式を導入する。
SLED-IFV(SLED-IFV)は、これらの形態とその具体的ターゲットの選択を自動化する、解凍式LCM誘導流である。
- 参考スコア（独自算出の注目度）: 0.23799118675414221
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Formal hardware information-flow verification (IFV) provides strong guarantees against secret-dependent timing and control behavior, but often scales poorly on realistic RTL. We identify two recurring proof barriers in self-composed IFV: implementation complexity, where proof-hard datapath logic dominates even though the property needs only a compact boundary relation, and relational inductive complexity, where the proof depends on cross-copy public-control facts that the backend prover does not infer efficiently. To address them, we introduce two semantic proof decomposition forms: functional simplification, which replaces a proof-hard RTL region with a validated over-approximate summary, and relational strengthening, which exposes and proves the cross-copy relations needed for induction. We further present SLED-IFV, a solver-validated LLM-guided flow that automates the selection of these forms and their concrete targets. Given a self-composed miter and an oracle-free decision sheet, the LLM proposes a decomposition, then materializes it into proof artifacts under controller checks. The controller compiles the checked artifacts into proof obligations, and the formal verification backend remains the sole authority for acceptance. Across nine nontrivial benchmarks constructed from real RTL, SLED-IFV achieves up to 603x solver-only speedup and converts two 12-hour timeouts into completed proofs. The closed-loop flow produces verifier-accepted decompositions for all cases.
- Abstract（参考訳）: 形式的ハードウェア情報フロー検証(IFV)は、秘密に依存したタイミングと制御行動に対する強力な保証を提供するが、現実的なRTLでは不十分であることが多い。
実装複雑性, 特性がコンパクトな境界関係のみを必要とするにもかかわらず, 証明ハードなデータパス論理が支配する実装複雑性, リレーショナル帰納的複雑性, 証明は, バックエンドの証明者が効率的に推論しないクロスコピーな公開制御事実に依存する。
そこで本論文では,証明に難渋したRTL領域を補完する機能的単純化と,帰納化に必要なクロスコピー関係を公開・証明するリレーショナル強化という2つの意味的証明分解形式を提案する。
さらに,SLED-IFVは,これらの形状とその具体的対象の選択を自動化するLLM誘導流である。
自己合成ミッターとオラクルフリーの意思決定シートが与えられた後、LLMは分解を提案し、それをコントローラチェックの下で証明アーティファクトに加工する。
コントローラはチェック済みのアーティファクトを証明義務にコンパイルし、正式な検証バックエンドは受け入れの唯一の権限のままである。
実RTLから構築された9つの非自明なベンチマークの中で、SLED-IFVは最大603倍の高速化を実現し、2つの12時間のタイムアウトを完了した証明に変換する。
閉ループ流は全てのケースに対して検証器が受け入れる分解を生成する。
関連論文リスト
- Open-Source LLM-Driven Formal Verification: A Multi-Agent Pipeline for RTL Repair [0.0]
本稿では,LLMとオープンソースの形式的バックエンドを結合してRTLを修復するマルチエージェントパイプラインを提案する。
パイプラインが実際の機能的バグを検出・修復できることを示す。
境界被覆空白、仕様曖昧性、時間論理的バグ、マルチプロパティプレッシャーの4つの異なる障害モードを特徴付ける。
論文 参考訳（メタデータ） (2026-07-30T22:43:33Z) - Guarded Equivalence Predicates for Scalable Formal Hardware Information-Flow Verification [0.0]
自己構成は、情報フロー検証を2つの回路コピー上の安全性チェックに還元する。
近年のPDRに基づく手法では、複写対称性と大域的クロスコピー等価式を用いて、この重複構造を利用する。
我々はこれらの関係をPDRに公開するために、ガード付き等価述語を導入する。
論文 参考訳（メタデータ） (2026-06-20T14:25:13Z) - Logic-Regularized Verifier Elicits Reasoning from LLMs [63.65875399266337]
論理規則で正規化された教師なしの検証器であるLOVERを提案する。
ローバーは、定理を二項潜在変数として扱い、内部の活性化を活用し、3つの論理的制約を課す。
ローバーは教師なしのベースラインを大幅に上回る。
論文 参考訳（メタデータ） (2026-05-07T09:03:49Z) - Trust but Verify: Introducing DAVinCI -- A Framework for Dual Attribution and Verification in Claim Inference for Language Models [53.279391576560755]
大規模言語モデル(LLM)は、広範囲のNLPタスクにおいて顕著な流速と汎用性を示してきたが、実際的な不正確さと制限が伴う傾向にある。
これは、信頼と妥当性が最優先される医療、法律、科学コミュニケーションといった、高リスク領域に重大なリスクをもたらす。
LLM出力の事実的信頼性と解釈可能性を高めるために設計されたDAVinCI - Dual Attribution and Verificationフレームワークを紹介する。
論文 参考訳（メタデータ） (2026-04-23T01:37:50Z) - AgentV-RL: Scaling Reward Modeling with Agentic Verifier [63.55502685076245]
試験時間スケーリング(TTS)によるLCM推論を強化する検証器が実証されている。
本稿では,報酬モデリングを多ターンツール拡張型検討プロセスに変換するフレームワークであるエージェント検証を提案する。
Agentic Verifier は並列およびシーケンシャルTS の両方で一貫した性能向上が得られることを示す。
論文 参考訳（メタデータ） (2026-04-17T12:27:36Z) - Training LLMs for Multi-Step Tool Orchestration with Constrained Data Synthesis and Graduated Rewards [76.49428173793386]
LLMは、中間出力を伝搬しながら、正しい順序で複数の依存APIを呼び出す必要がある。
既存の環境は、シミュレーションデータを使った単純なターン毎の関数呼び出しとバイナリ報酬に重点を置いている。
まず、実APIレスポンスの大規模キャッシュを背景とした強化学習環境を構築し、有効なマルチステップオーケストレーショントレースをサンプリングするデータ合成パイプラインを実現する。
第二に、正当性を原子の妥当性とオーケストレーションに分解する、段階的な報酬設計を提案する。
論文 参考訳（メタデータ） (2026-03-25T18:31:39Z) - zkCraft: Prompt-Guided LLM as a Zero-Shot Mutation Pattern Oracle for TCCT-Powered ZK Fuzzing [7.274627641804014]
zkCraftは決定論的、R1CS対応のローカライゼーションと証明付き検索を組み合わせて意味的不整合を検出するフレームワークである。
証明付きローカライゼーションは, 偽陽性が低い多彩な下限および過制約の断層を検出し, コストのかかるソルバ相互作用を低減できることを示す。
論文 参考訳（メタデータ） (2026-01-31T11:31:00Z) - Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation [4.723302382132762]
シリコングレードの正しさは、 (i) シミュレーション中心の評価の限られたカバレッジと信頼性、 (ii) 回帰と修復幻覚、 (iii) エージェントハンドオフ間で意図が再解釈される意味的ドリフトによってボトルネックが残っている。
エージェントの意図を整合させる設計契約を確立するマルチエージェントフレームワークであるVeri-Sureを提案する。
論文 参考訳（メタデータ） (2026-01-27T16:10:23Z) - Towards Comprehensive Stage-wise Benchmarking of Large Language Models in Fact-Checking [64.97768177044355]
大規模言語モデル(LLM)は、現実のファクトチェックシステムにますます多くデプロイされている。
FactArenaは、完全に自動化されたアリーナスタイルの評価フレームワークである。
本研究では,静的クレーム検証精度とエンドツーエンドのファクトチェック能力の相違点を明らかにした。
論文 参考訳（メタデータ） (2026-01-06T02:51:56Z) - Formal that "Floats" High: Formal Verification of Floating Point Arithmetic [0.0]
本稿では,金の基準モデルに対する直接RTL-RTLモデルによる浮動小数点演算の検証方法を提案する。
この方法論はエージェントAIベースの形式的プロパティ生成によって拡張され、大規模言語モデル(LLM)駆動の自動化とHuman-in-the-Loop(HITL)の洗練を統合する。
その結果, RTL-to-RTLモデルの直接チェックは, 適用効率が向上し, スタンドアロンの検証よりもアサーションが少なくなることがわかった。
論文 参考訳（メタデータ） (2025-12-07T14:03:44Z) - Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
LLMの複雑な推論には2行のアプローチが採用されている。
1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。
他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。
具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
論文 参考訳（メタデータ） (2023-11-16T11:26:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。