論文の概要: Formal-Verification-Guided Bayesian Optimization for Non-Intrusive Last-Mile Coverage Closure

• arxiv url: http://arxiv.org/abs/2610.17449v1
• Date: Mon, 12 Oct 2026 22:07:37 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-17 18:57:39.758458
• Title: Formal-Verification-Guided Bayesian Optimization for Non-Intrusive Last-Mile Coverage Closure
• Title（参考訳）: 非侵入型ラストミル被覆閉鎖に対する形式的検証誘導型ベイズ最適化
• Abstract要約: 既存の人間による機能カバレッジモデルにおいて、事前に定義されたビンを閉じる非侵入的ワークフローを提案する。 設計仕様から検証対象を合成しない。 OpenTitan AESでは、第一パス還元空間BOは241/271ビンに達する。 エントロピー源では、第1パス還元空間BOは2117/2277個のビンに達する。
• 参考スコア（独自算出の注目度）: 8.138353877479751
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Last-mile functional coverage closure for modern chip designs remains costly because a mature UVM environment exposes many controls while direct hits on the remaining bins are sparse. We present a non-intrusive workflow that closes pre-defined bins in an existing, human-authored functional coverage model; it does not synthesize verification objectives from the design specification. The workflow first uses abstract-syntax-tree (AST) parsing and cone-of-influence (COI) tracing to map each residual target to existing testbench knobs. Under a matched 20-simulation budget, Bayesian optimization (BO) is compared with continued constrained-random verification (CRV) and random search over the same AST/COI-reduced space. Formal reachability then removes only targets supported by complete unreachability proofs, after which retained targets are grouped by formal difficulty and processed by group-specific BO under a second matched 20-simulation budget. Cleanup and grouping never add numerator bins; only simulator coverage artifacts do. On OpenTitan AES, first-pass reduced-space BO reaches 241/271 bins; formal cleanup removes two denominator bins; the integrated post-cleanup stage - difficulty grouping, policy routing, and group-specific BO - adds 20 simulator-confirmed hits, yielding 261/271 raw coverage (96.31%) and 261/269 effective coverage (97.03%). On Entropy Source, first-pass reduced-space BO reaches 2117/2277 bins; formal cleanup removes ten denominator bins; the integrated post-cleanup stage - difficulty grouping, policy routing, and group-specific BO - adds 93 simulator-confirmed hits, yielding 2210/2277 raw coverage (97.06%) and 2210/2267 effective coverage (97.49%). These results characterize the integrated diagnosis-and-search workflow; the present evaluation does not isolate the causal contributions of difficulty classification, policy routing, and post-cleanup BO.
• Abstract（参考訳）: 成熟したUVM環境が多くのコントロールを公開する一方で、残りのビンの直接ヒットは少ないため、最新のチップ設計のラストマイル機能カバレッジクロージャは依然としてコストがかかる。 我々は、既存の人間による機能カバレッジモデルにおいて、事前に定義されたビンを閉じる非侵入的なワークフローを提示し、設計仕様から検証対象を合成しない。 ワークフローはまず抽象構文木(AST)解析とcoe-of-influence(COI)トレースを使用して、各残留ターゲットを既存のテストベンチノブにマッピングする。 一致した20のシミュレーション予算の下で、ベイズ最適化(BO)は、制約付きランダム検証(CRV)と同一のAST/COI還元空間上のランダム探索と比較される。 形式的到達性は、完全な到達不能証明によって支持されるターゲットのみを除去し、その後、保持されたターゲットは形式的な困難によってグループ化され、第2の20シミュレート予算の下でグループ固有のBOによって処理される。 クリーンアップとグループ化は、決してnumerator binを追加しません。 OpenTitan AESでは、最初のパス削減スペースBOが241/271ビンに到達し、正式なクリーンアップは2つの分母ビンを除去する。 Entropy Sourceでは、最初のパス削減スペースBOが2117/2277ビンに到達し、正式なクリーンアップは10個の分母ビンを除去し、統合されたポストクリーンアップステージ - グループ化、ポリシールーティング、グループ固有のBO - 93個のシミュレータ確認ヒット、2210/2277の生のカバレッジ(97.06%)と2210/2267の効果的なカバレッジ(97.49%)が追加されている。 これらの結果は統合診断と検索のワークフローを特徴付けており、本評価では、難易度分類、ポリシールーティング、クリーンアップ後のBOの因果的貢献を分離していない。

関連論文リスト

• SPARCL: Spatially Adaptive Regional Coverage for Active Learning in Chest X-ray Analysis [3.320895640965475]
  胸部X線病変セグメンテーション(CXR)のアクティブラーニングは高価であり,アクティブラーニング(AL)が不可欠である。 既存のAL戦略では、選択されたサンプルの空間分布を考慮できないため、焦点(大動脈石灰化など)と拡散(結節など)の病理に不整合性が生じる。
  論文  参考訳（メタデータ） (2026-10-13T06:34:50Z)
• RFPO: Rectified Flow Policy Optimization for Embodied Control [57.28454299980691]
  フローベースのポリシーは、継続的ロボット制御のための表現力のあるフレームワークを提供するが、その反復ODE統合は、かなりの推論コストをもたらす。 本稿では,信頼性のある数ステップ実行のためのフローポリシー最適化フレームワークRFPOを紹介する。 Unitree Go2、Boston Dynamics Spot、Unitree H1、Unitree G1の他、RFPOはワンステップ実行下でのフルステップ制御性能を一貫して維持する。
  論文  参考訳（メタデータ） (2026-10-07T17:24:46Z)
• DRSR: Learning Set-Level Deletion Risk for Efficient Long-Horizon Agents [55.84813053778976]
  ロングホライゾン言語モデルエージェントは、現在の決定と関係が変化する推論の痕跡、ツール交換、観察を蓄積する。 直接セットリスクスコアは、削除セットの選択としてエージェント履歴圧縮リスクを定式化する。 メカニカル・アナリシスとアブリケーションは、決定に制約のある関係、保持されたコンテキスト情報、ペア・インタラクション、および棄権がそれぞれ信頼できるプルーニングに寄与していることを示している。
  論文  参考訳（メタデータ） (2026-09-23T03:06:01Z)
• Observational Indistinguishability and Integrity Blind Regions in Hybrid Quantum-Classical Workflows [0.0]
  本稿では,ハイブリッド量子古典的ワークフロー整合性のためのクレーム相対的エビデンス/参照フレームワークを提案する。 観測上の不明瞭さは、有限バッチ統計ミスとは異なる構造的な盲点をもたらす。
  論文  参考訳（メタデータ） (2026-09-15T13:16:37Z)
• EAVer: Long-Form Factuality Verification as an End-to-End Agentic Policy [50.665874114632]
  我々は、完全な応答レベルの検証ワークフローを統一ポリシーとして制御することを学ぶ、エンドツーエンドのエージェント検証であるEAVerを紹介する。 EAVerはセマンティック関連クレームをグループ化し、信頼に基づいた直接検証やターゲット検索にルートし、コンパクトなインコンテキストメモで検索によって返される証拠を保持する。
  論文  参考訳（メタデータ） (2026-09-02T21:00:35Z)
• Metric Aggregation Divergence: A Hidden Validity Threat in Agent-Based Policy Optimization and a Contractual Remedy [7.1976264551575895]
  メートル法アグリゲーション分散(英: Metric aggregate divergence、MAD)は、エージェントベースのモデルにおいて、異なるパイプラインステージで発生するサイレント不整合である。 私たちは、ディスパッチ時に実施される単一の呼び出し可能なランタイムであるメトリックコントラクトを、対策として紹介します。
  論文  参考訳（メタデータ） (2026-06-27T18:17:33Z)
• Decompose Sparsely Where You Should, Absorb Densely Where You Should No [4.687417972972663]
  スパースオートエンコーダ(SAE)は、通常、スパース辞書を通してテクスベンター残流を再構築するために訓練される。 この仮定に疑問を呈し、アクティベーションが低ランクで高密度な成分を含んでいるという仮説を立てる。
  論文  参考訳（メタデータ） (2026-06-12T02:29:35Z)
• Cut Your Losses! Learning to Prune Paths Early for Efficient Parallel Reasoning [30.70183055909553]
  経路解析における最初の体系的分類法を提案し,その信号源による分類法(内部対外部)と学習可能性(学習可能対非学習可能)を提案する。 この分類は、学習可能な内部メソッドの未探索の可能性を明らかにし、STOP(Super Token for Pruning)の提案を動機付けます。
  論文  参考訳（メタデータ） (2026-04-17T13:00:22Z)
• Semi-DETR: Semi-Supervised Object Detection with Detection Transformers [105.45018934087076]
  半教師付き物体検出(SSOD)におけるDETRに基づくフレームワークの解析 本報告では,第1次変圧器を用いたエンド・ツー・エンド半教師対象検出器であるSemi-DETRについて述べる。 我々の手法は、最先端の手法をクリアマージンで上回る。
  論文  参考訳（メタデータ） (2023-07-16T16:32:14Z)
• Optimal Clustering with Bandit Feedback [57.672609011609886]
  本稿では,バンディットフィードバックを用いたオンラインクラスタリングの問題点について考察する。 これは、NPハード重み付きクラスタリング問題をサブルーチンとして解決する必要性を回避するための、シーケンシャルなテストのための新しい停止規則を含む。 合成および実世界のデータセットの広範なシミュレーションを通して、BOCの性能は下界と一致し、非適応的ベースラインアルゴリズムよりも大幅に優れることを示す。
  論文  参考訳（メタデータ） (2022-02-09T06:05:05Z)

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

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