論文の概要: 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駆動ヒューリスティック進化
- 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が厳密な正当性ゲートの下で実用的ヒューリスティックな改善を確実に発見できることを実証した。
関連論文リスト
- MetaRSI / RSI2: A Meta-Recursive Self-Improving System for Recursive Self-Improving Systems Themselves [65.60481414910728]
再帰的な自己改善により、システムは自身の失敗からモデル構築機械を改善することができる。
しかし、RSIは、科学のQAや数学のようなコーディングと形式的なベンチマークにのみ検証されている。
RSIは次に、科学的、工学的、メタ科学的な領域にまたがって運用されなければならない、と我々は主張する。
本稿では,MetaRSI-v1を提案する。改良は,1つの統一パラダイム上での3つの型付き演算子のスケジュール構成である。
論文 参考訳（メタデータ） (2026-09-06T05:15:31Z) - LMSM: LLM Security Framework Inspired by Linux Security Modules [56.93644694627783]
大規模言語モデル(LLM)は階層化されたディフェンスでデプロイされることが多いが、悪意のあるプロンプトはそれらをバイパスすることができる。
我々は,Language Model Security Modules (LMSM) という,Linux Security Modules (LSM) の背後にある分離を LLM サービスに適応させるセキュリティフレームワークを提案する。
論文 参考訳（メタデータ） (2026-08-26T12:13:05Z) - Intent-Level Quantum Programming with Assertion-Guided Execution and Inspectable Intermediate Representation [0.22183164865527472]
量子ドメイン固有言語(Q)は3つのメカニズムを通して問題に対処する。
第1級IRイントロスペクション、回路幅の露光、ワイヤマッピング、操作順序、および実行前の開発者検査のための測定意図。
アサーション誘導モード推論では、エンジンが宣言された検証プロパティを調べて、サンプリング、ステートベクタ、デュアル実行を自動的に選択する。
論文 参考訳（メタデータ） (2026-07-31T18:21:32Z) - Open-Source LLM-Driven Formal Verification: A Multi-Agent Pipeline for RTL Repair [0.0]
本稿では,LLMとオープンソースの形式的バックエンドを結合してRTLを修復するマルチエージェントパイプラインを提案する。
パイプラインが実際の機能的バグを検出・修復できることを示す。
境界被覆空白、仕様曖昧性、時間論理的バグ、マルチプロパティプレッシャーの4つの異なる障害モードを特徴付ける。
論文 参考訳（メタデータ） (2026-07-30T22:43:33Z) - SVR: Self-Verifying Refinement via Joint Verdict-Confidence Reinforcement Learning for Adaptive Test-Time Compute [62.3458279176813]
自己検証リファインメント(Self-Verifying Refinement)は、オラクルフリーのマルチターン強化学習フレームワークである。
自己検証を計算制御ポリシとして使用することを学ぶ。
マクロ平均精度は0.563で、平均で2.99回しか推測できない。
論文 参考訳（メタデータ） (2026-07-30T16:20:58Z) - Gatekeepers and Hallucinations: A Layered Evaluation Framework for LLM-Driven Quantum Circuit Generation [0.0]
材料インフォームド変分量子固有解器(VQE)回路生成のための階層評価フレームワークを提案する。
5つの異なるLCM障害モード(幾何学幻覚、存在しないAPI使用、統合障害、制約違反、検証不可能な出力)を分類する。
評価プラットフォーム自身のソースコードの法医学的な監査により、サイレントフォールバック・テンプレート置換によって、ハーネスに2つの明らかなモデル障害が生じたことが確認された。
論文 参考訳（メタデータ） (2026-06-16T19:17:54Z) - CIAware-Bench: Benchmarking Control Intervention Awareness Across Frontier LLMs [100.38986535324284]
我々は、フロンティアモデル全体でのtextbfcontrol textbfintervention (CI) の認識を測定するベンチマークである textbfCIAware-Bench を紹介する。
CIAware-Benchは、モデルが自身の軌跡を制御介入によって修正されたものと区別できるかどうかをテストする。
論文 参考訳（メタデータ） (2026-06-09T16:24:16Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。