論文の概要: IC3-Evolve: Proof-/Witness-Gated Offline LLM-Driven Heuristic Evolution for IC3 Hardware Model Checking
- arxiv url: http://arxiv.org/abs/2604.03232v1
- Date: Sun, 18 Jan 2026 12:37:27 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-19 19:09:11.333806
- Title: IC3-Evolve: Proof-/Witness-Gated Offline LLM-Driven Heuristic Evolution for IC3 Hardware Model Checking
- Title（参考訳）: IC3-Evolve: IC3ハードウェアモデルチェックのためのオフラインLCM駆動ヒューリスティック進化
- Authors: Mingkai Miao, Guangyu Hu, Ziyi Yang, Hongce Zhang,
- Abstract要約: IC3-Evolveはオフラインのコード進化フレームワークで、IC3の実装に小さな、スロット制限付き、監査可能なパッチを提案する。
すべての候補パッチは、証明/ビヘイビアゲートによる検証によってのみ承認される。
我々は、HWMCCベンチマークで進化し、未確認の公開および産業モデル検査ベンチマークにおける一般化可能性を評価する。
- 参考スコア（独自算出の注目度）: 18.919431566830497
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: IC3, also known as property-directed reachability (PDR), is a commonly-used algorithm for hardware safety model checking. It checks if a state transition system complies with a given safety property. IC3 either returns UNSAFE (indicating property violation) with a counterexample trace, or SAFE with a checkable inductive invariant as the proof to safety. In practice, the performance of IC3 is dominated by a large web of interacting heuristics and implementation choices, making manual tuning costly, brittle, and hard to reproduce. This paper presents IC3-Evolve, an automated offline code-evolution framework that utilizes an LLM to propose small, slot-restricted and auditable patches to an IC3 implementation. Crucially, every candidate patch is admitted only through proof- /witness-gated validation: SAFE runs must emit a certificate that is independently checked, and UNSAFE runs must emit a replayable counterexample trace, preventing unsound edits from being deployed. Since the LLM is used only offline, the deployed artifact is a standalone evolved checker with zero ML/LLM inference overhead and no runtime model dependency. We evolve on the public hardware model checking competition (HWMCC) benchmark and evaluate the generalizability on unseen public and industrial model checking benchmarks, showing that IC3-Evolve can reliably discover practical heuristic improvements under strict correctness gates.
- Abstract（参考訳）: IC3(プロパティ指向リーチビリティ、英: property-directed reachability、PDR)は、ハードウェアの安全モデルチェックに使用されるアルゴリズムである。
状態遷移システムが所定の安全特性に準拠しているかどうかをチェックする。
IC3 は NSAFE (indicating property violation) を反例トレースで返却するか、安全の証明としてチェック可能なインダクティブ不変量で SAFE を返す。
実際、IC3の性能は相互作用するヒューリスティックと実装の選択の大きなウェブに支配されており、手動チューニングはコストがかかり、脆く、再現が難しい。
本稿では、LCMを利用してIC3実装に小さな、スロット制限付き、監査可能なパッチを提案する、自動オフラインコード進化フレームワークIC3-Evolveを提案する。
SAFEの実行は独立してチェックされた証明書を発行しなければならないし、NSAFEの実行は再生可能な反例トレースを発行しなければならない。
LLMはオフラインでのみ使用されるため、デプロイされたアーティファクトは、ML/LLM推論オーバーヘッドがゼロで、ランタイムモデル依存性がないスタンドアロンの進化したチェッカーである。
我々は,HWMCCベンチマーク上で進化し,未確認の公開および産業モデル検査ベンチマークの一般化可能性を評価し,IC3-Evolveが厳密な正当性ゲートの下で実用的ヒューリスティックな改善を確実に発見できることを実証した。
関連論文リスト
- Compiling Activation Steering into Weights via Null-Space Constraints for Stealthy Backdoors [48.881343993730844]
安全性に整合した大規模言語モデル(LLM)は、現実世界のパイプラインにますますデプロイされている。
敵は通常の評価では動作しないバックドアのチェックポイントを配布することができる。
最近のポストホック重み付け法は、そのようなバックドアを注入するための効率的なアプローチを提供する。
論文 参考訳（メタデータ） (2026-04-14T06:48:33Z) - Automated Self-Testing as a Quality Gate: Evidence-Driven Release Management for LLM Applications [51.56484100374058]
我々は,エビデンスに基づくリリース決定を伴う品質ゲートを導入する自動自己テストフレームワークを提案する。
内部展開型多エージェント対話型AIシステムの縦型ケーススタディにより,本フレームワークの評価を行った。
論文 参考訳（メタデータ） (2026-03-13T20:44:15Z) - Detect Repair Verify for Securing LLM Generated Code: A Multi-Language Empirical Study [10.18490328199727]
セキュリティは、問題を検出し、修正を適用し、結果を検証するDerction-Repair--Verify (DRV)ループを通じて対処されることが多い。
この研究は、プロジェクトレベルのアーティファクトのワークフローを研究し、以下の4つのギャップに対処する: L1、実行可能な機能とセキュリティテストを備えたプロジェクトレベルのベンチマークの欠如 L2、検出や修復のみを研究すること以外のパイプラインレベルの有効性に関する限られた証拠 L3、修正ガイダンスとしての検出レポートの不確実な信頼性、そしてL4、検証中の不確実な修復信頼性と副作用。
論文 参考訳（メタデータ） (2026-03-01T03:41:24Z) - 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) - RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
LLM(Large Language Models)は、コード生成において顕著な能力を示しているが、セキュアなコードを生成する能力は依然として重要で、未調査の領域である。
我々はRealSec-benchを紹介します。RealSec-benchは、現実世界の高リスクなJavaリポジトリから慎重に構築されたセキュアなコード生成のための新しいベンチマークです。
論文 参考訳（メタデータ） (2026-01-30T08:29:01Z) - SecIC3: Customizing IC3 for Hardware Security Verification [5.709679444204919]
SecIC3は、IC3に基づくハードウェアモデルチェックアルゴリズムであり、この自己構成構造を利用するようにカスタマイズされている。
我々は、SecIC3を2つのオープンソースIC3実装上に実装し、10つの設計からなる非干渉チェックベンチマークで評価する。
論文 参考訳（メタデータ） (2026-01-29T07:24:08Z) - 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) - ImpossibleBench: Measuring LLMs' Propensity of Exploiting Test Cases [58.411135609139855]
タスク完了のための「ショートカット」は、大規模言語モデルの信頼性評価と展開に重大なリスクをもたらす。
我々は,LLMエージェントがテストケースを利用するための正当性を測定するベンチマークフレームワークであるImpossibleBenchを紹介する。
実践的なフレームワークとして、ImpossibleBenchは単なる評価ではなく、汎用的なツールである。
論文 参考訳（メタデータ） (2025-10-23T06:58:32Z) - Are You Getting What You Pay For? Auditing Model Substitution in LLM APIs [71.7892165868749]
LLM(Commercial Large Language Model) APIは基本的な信頼の問題を生み出します。
ユーザーは特定のモデルに課金するが、プロバイダが忠実に提供できることを保証することはない。
我々は,このモデル置換問題を定式化し,現実的な逆条件下での検出方法を評価する。
我々は,信頼された実行環境(TEE)を実用的で堅牢なソリューションとして使用し,評価する。
論文 参考訳（メタデータ） (2025-04-07T03:57:41Z) - Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。
SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。
我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
論文 参考訳（メタデータ） (2024-10-21T08:15:45Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。