論文の概要: A-IC3: Learning-Guided Adaptive Inductive Generalization for Hardware Model Checking

• arxiv url: http://arxiv.org/abs/2604.21688v1
• Date: Thu, 23 Apr 2026 13:53:06 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-24 14:40:06.568842
• Title: A-IC3: Learning-Guided Adaptive Inductive Generalization for Hardware Model Checking
• Title（参考訳）: A-IC3:ハードウェアモデル検査のための学習誘導型適応帰納的一般化
• Authors: Xiaofeng Zhou, Guangyu Hu, Hongce Zhang, Wei Zhang,
• Abstract要約: 帰納的一般化戦略を動的に選択する軽量な機械学習ベースのフレームワークを提案する。 検証プロセスからのリアルタイムフィードバックに基づいて帰納的一般化戦略を適応的に選択するために,マルチアーム・バンディット(MAB)アルゴリズムを用いる。 最先端のモデルチェッカー rIC3 に実装すると,ベースラインよりも26から50のケースを解決し,PAR-2 のスコアを 194.72 から 389.29 に改善する。
• 参考スコア（独自算出の注目度）: 4.894184972043368
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The IC3 algorithm represents the state-of-the-art (SOTA) hardware model checking technique, owing to its robust performance and scalability. A significant body of research has focused on enhancing the solving efficiency of the IC3 algorithm, with particular attention to the inductive generalization process: a critical phase wherein the algorithm seeks to generalize a counterexample to inductiveness (CTI), which typically is a state leading to a bad state, into a broader set of states. This inductive generalization is a primary source of clauses in IC3 and thus plays a pivotal role in determining the overall effectiveness of the algorithm. Despite its importance, existing approaches often rely on fixed inductive generalization strategies, overlooking the dynamic and context-sensitive nature of the verification environment in which spurious counterexamples arise. This rigidity can limit the quality of generated clauses and, consequently, the performance of IC3. To address this limitation, we propose a lightweight machine-learning-based framework that dynamically selects appropriate inductive generalization strategies in response to the evolving verification context. Specifically, we employ a multi-armed bandit (MAB) algorithm to adaptively choose inductive generalization strategies based on real-time feedback from the verification process. The agent is updated by evaluating the quality of generalization outcomes, thereby refining its strategy selection over time. Empirical evaluation on a benchmark suite comprising 914 instances, primarily drawn from the latest HWMCC collection, demonstrates the efficacy of our approach. When implemented on the state-of-the-art model checker rIC3, our method solves 26 to 50 more cases than the baselines and improves the PAR-2 score by 194.72 to 389.29.
• Abstract（参考訳）: IC3アルゴリズムは、その堅牢な性能とスケーラビリティのため、最先端(SOTA)ハードウェアモデル検査技術を表している。 IC3アルゴリズムの解法効率の向上に焦点が当てられ、特に帰納的一般化(英語版)プロセス(英語版)に注意が向けられている: アルゴリズムが帰納的誘導性(英語版)(CTI)に対する反例を一般化しようとする臨界相(英語版)は、通常、悪い状態に至る状態である。 この帰納的一般化は、IC3における節の主要な源であり、アルゴリズムの全体的な有効性を決定する上で重要な役割を果たす。 その重要性にもかかわらず、既存のアプローチはしばしば固定帰納的一般化戦略に依存し、急激な反例が発生する検証環境の動的で文脈に敏感な性質を見越す。 この剛性は生成された節の品質を制限し、結果としてIC3の性能を低下させる。 この制限に対処するために、進化する検証コンテキストに応じて適切な帰納的一般化戦略を動的に選択する軽量機械学習ベースのフレームワークを提案する。 具体的には、検証プロセスからのリアルタイムフィードバックに基づいて帰納的一般化戦略を適応的に選択するために、マルチアーム・バンディット(MAB)アルゴリズムを用いる。 一般化結果の質を評価して、時間とともに戦略選択を洗練することにより、エージェントを更新する。 最新のHWMCCコレクションから抽出された914のインスタンスからなるベンチマークスイートの実証評価により,本手法の有効性が示された。 最先端のモデルチェッカー rIC3 に実装すると,ベースラインよりも26から50のケースを解決し,PAR-2 のスコアを 194.72 から 389.29 に改善する。

関連論文リスト

• Unlocking Out-of-Distribution Generalization in Transformers via Recursive Latent Space Reasoning [50.99796659680724]
  本研究では,GSM8Kスタイルのモジュラー演算をテストベッドとして用いたTransformerネットワークにおけるアウト・オブ・ディストリビューション(OOD)の一般化について検討する。 我々は,OOD一般化の強化を目的とした4つのアーキテクチャ機構のセットを紹介し,検討する。 我々はこれらの実験結果を詳細な機械論的解釈可能性分析で補完し、これらのメカニズムがOOD一般化能力をいかに高めるかを明らかにする。
  論文  参考訳（メタデータ） (2025-10-15T21:03:59Z)
• Learning via Surrogate PAC-Bayes [13.412960492870996]
  PAC-Bayes学習は、学習アルゴリズムの一般化能力を研究するための包括的な設定である。 本稿では,一連の代理学習目標を最適化することで,反復学習アルゴリズムを構築するための新しい原則的戦略を提案する。 PAC-Bayes境界による学習の一般的なレシピを提供するのに加えて、(i)サロゲートの反復最適化が元の一般化境界の最適化を意味することを示す理論的結果を提供する。
  論文  参考訳（メタデータ） (2024-10-14T07:45:50Z)
• Tri-Level Navigator: LLM-Empowered Tri-Level Learning for Time Series OOD Generalization [9.95894026392039]
  事前学習された大言語モデルを用いた時系列OOD一般化について検討する。 まず,textbfSeries textbfOOD 一般化のための新しい textbfTri レベルの学習フレームワーク TTSO を提案する。 本稿では,この三段階最適化問題に適した階層化ローカライゼーションアルゴリズムを開発し,提案アルゴリズムの保証収束を理論的に実証する。
  論文  参考訳（メタデータ） (2024-10-09T16:00:21Z)
• Hierarchical Decision Making Based on Structural Information Principles [19.82391136775341]
  本稿では,階層的意思決定のための構造情報原則に基づく新しいフレームワーク,すなわちSIDMを提案する。 本稿では,過去の状態-行動軌跡を処理し,状態と行動の抽象表現を構築する抽象化機構を提案する。 単エージェントシナリオのためのスキルベース学習手法と,多エージェントシナリオのためのロールベースの協調手法を開発し,そのどちらも,パフォーマンス向上のために様々な基礎アルゴリズムを柔軟に統合することができる。
  論文  参考訳（メタデータ） (2024-04-15T13:02:00Z)
• Randomized Adversarial Style Perturbations for Domain Generalization [49.888364462991234]
  本稿では,RASP(Randomized Adversarial Style Perturbation)と呼ばれる新しい領域一般化手法を提案する。 提案アルゴリズムは, ランダムに選択されたクラスに対して, 対角方向の特徴のスタイルを乱し, 予期せぬ対象領域で観測される予期せぬスタイルに誤解されないよう, モデルを学習させる。 提案アルゴリズムは,様々なベンチマークによる広範な実験により評価され,特に大規模ベンチマークにおいて,領域一般化性能が向上することを示す。
  論文  参考訳（メタデータ） (2023-04-04T17:07:06Z)
• Understanding and Constructing Latent Modality Structures in Multi-modal Representation Learning [53.68371566336254]
  優れたパフォーマンスの鍵は、完全なモダリティアライメントではなく、有意義な潜在モダリティ構造にある、と我々は主張する。 具体的には,1)モダリティ内正規化のための深い特徴分離損失,2)モダリティ間正規化のためのブラウン橋損失,3)モダリティ内正規化およびモダリティ間正規化のための幾何学的整合損失を設計する。
  論文  参考訳（メタデータ） (2023-03-10T14:38:49Z)
• Exploring the Algorithm-Dependent Generalization of AUPRC Optimization with List Stability [107.65337427333064]
  AUPRC(Area Under the Precision-Recall Curve)の最適化は、機械学習にとって重要な問題である。 本研究では, AUPRC最適化の単依存一般化における最初の試行について述べる。 3つの画像検索データセットの実験は、我々のフレームワークの有効性と健全性に言及する。
  論文  参考訳（メタデータ） (2022-09-27T09:06:37Z)
• Target-Embedding Autoencoders for Supervised Representation Learning [111.07204912245841]
  本稿では,対象空間が高次元な純粋教師付き環境における一般化の枠組みを解析する。 我々は、教師付き予測のための目標埋め込みオートエンコーダ(TEA)の一般的なフレームワークのモチベーションと形式化を行い、特徴とターゲットの予測の両方から予測可能なように最適化された中間潜在表現を学習する。
  論文  参考訳（メタデータ） (2020-01-23T02:37:10Z)

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

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