論文の概要: MPBMC: Multi-Property Bounded Model Checking with GNN-guided Clustering

• arxiv url: http://arxiv.org/abs/2603.04450v1
• Date: Thu, 26 Feb 2026 19:56:52 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-03-06 22:06:10.888427
• Title: MPBMC: Multi-Property Bounded Model Checking with GNN-guided Clustering
• Title（参考訳）: MPBMC: GNN誘導クラスタリングによるマルチパフォーマンス境界モデルチェック
• Authors: Soumik Guha Roy, Sumana Ghosh, Ansuman Banerjee, Raj Kumar Gajavelly, Sudhakar Surendran,
• Abstract要約: 本稿では,ハードウェア回路の神経機能表現とランタイム設計統計量を利用するハイブリッド手法を提案する。 提案手法は,機能的埋め込みと設計統計に基づいて知的にプロパティをグループ化し,検証結果を高速化する。
• 参考スコア（独自算出の注目度）: 0.22369578015657957
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal verification of designs with multiple properties has been a long-standing challenge for the verification research community. The task of coming up with an effective strategy that can efficiently cluster properties to be solved together has inspired a number of proposals, ranging from structural clustering based on the property cone of influence (COI) to leverage runtime design and verification statistics. In this paper, we present an attempt towards functional clustering of properties utilizing graph neural network (GNN) embeddings for creating effective property clusters. We propose a hybrid approach that can exploit neural functional representations of hardware circuits and runtime design statistics to speed up the performance of Bounded Model Checking (BMC) in the context of multi-property verification (MPV). Our method intelligently groups properties based on their functional embedding and design statistics, resulting in speedup in verification results. Experimental results on the HWMCC benchmarks show the efficacy of our proposal with respect to the state-of-the-art.
• Abstract（参考訳）: 複数の特性を持つ設計の形式的検証は、検証研究コミュニティにとって長年の課題である。 解決すべきプロパティを効率的にクラスタリングできる効果的な戦略を考案する作業は、COI(Property cone of influence)に基づいた構造的クラスタリングから、ランタイム設計と検証統計の活用に至るまで、数多くの提案を刺激した。 本稿では,グラフニューラルネットワーク (GNN) を用いた効率的なプロパティクラスタ構築のための機能クラスタリングの試みを行う。 本稿では,ハードウェア回路のニューラル関数表現とランタイム設計統計を利用して,マルチプロパティ検証(MPV)における境界モデル検査(BMC)の性能向上を図るハイブリッド手法を提案する。 提案手法は,機能的埋め込みと設計統計に基づいて知的にプロパティをグループ化し,検証結果を高速化する。 HWMCCベンチマークの実験結果から,提案手法の有効性が示された。

関連論文リスト

• MCFCN: Multi-View Clustering via a Fusion-Consensus Graph Convolutional Network [9.300953069946969]
  マルチビュークラスタリングを改善するために, MCFCN (Fusion-Consensus Graph Convolutional Network) を提案する。 マルチビューデータのコンセンサスグラフをエンドツーエンドで学習し、効果的なコンセンサス表現を学習する。 MCFCNは8つのマルチビューベンチマークデータセットで最先端のパフォーマンスを示す。
  論文  参考訳（メタデータ） (2025-11-03T14:46:04Z)
• ACTGNN: Assessment of Clustering Tendency with Synthetically-Trained Graph Neural Networks [4.668678950572517]
  ACTGNNは、データのグラフ表現を利用してクラスタリング傾向を評価するために設計されたグラフベースのフレームワークである。 グラフニューラルネットワーク(GNN)は、合成データセットのみにトレーニングされており、クラスタ構造を堅牢に学習することができる。 その結果,提案手法の一般化性と有効性を強調し,ロバストなクラスタリング傾向評価のための有望なツールとなった。
  論文  参考訳（メタデータ） (2025-01-30T03:31:26Z)
• Structure-guided Deep Multi-View Clustering [13.593229506936682]
  深いマルチビュークラスタリングは、クラスタリング性能を改善するために、複数のビューから豊富な情報を活用することを目指している。 既存のクラスタリング手法の多くは、多視点構造情報の完全なマイニングを無視することが多い。 構造誘導型深層多視点クラスタリングモデルを提案し,多視点データの分布を探索する。
  論文  参考訳（メタデータ） (2025-01-17T12:42:30Z)
• Matcha: Mitigating Graph Structure Shifts with Test-Time Adaptation [66.40525136929398]
  テスト時間適応(TTA)は、ソースドメインに再アクセスすることなく、トレーニング済みのモデルをターゲットドメインに適応できる能力によって注目を集めている。 グラフの構造シフトへの効果的かつ効率的な適応を目的とした,革新的なフレームワークであるMatchaを提案する。 合成と実世界の両方のデータセットに対するMatchaの有効性を検証し、構造と属性シフトの様々な組み合わせにおける頑健さを実証した。
  論文  参考訳（メタデータ） (2024-10-09T15:15:40Z)
• Adaptive Self-supervised Robust Clustering for Unstructured Data with Unknown Cluster Number [12.926206811876174]
  適応型自己教師型ロバストクラスタリング(Adaptive Self-supervised Robust Clustering, ASRC)と呼ばれる非構造化データに適した,新たな自己教師型ディープクラスタリング手法を提案する。 ASRCはグラフ構造とエッジ重みを適応的に学習し、局所構造情報と大域構造情報の両方をキャプチャする。 ASRCは、クラスタ数の事前知識に依存するメソッドよりも優れており、非構造化データのクラスタリングの課題に対処する上での有効性を強調している。
  論文  参考訳（メタデータ） (2024-07-29T15:51:09Z)
• Efficient Multi-View Graph Clustering with Local and Global Structure Preservation [59.49018175496533]
  局所・グローバル構造保存を用いた効率的なマルチビューグラフクラスタリング(EMVGC-LG)という,アンカーベースのマルチビューグラフクラスタリングフレームワークを提案する。 具体的には、EMVGC-LGがクラスタリング品質を向上させるために、アンカー構築とグラフ学習を共同で最適化する。 さらに、EMVGC-LGはサンプル数に関する既存のAMVGCメソッドの線形複雑性を継承する。
  論文  参考訳（メタデータ） (2023-08-31T12:12:30Z)
• Feature construction using explanations of individual predictions [0.0]
  本稿では,予測モデルのインスタンスベース説明の集約に基づく探索空間の削減手法を提案する。 これらのグループに対する探索の削減が特徴構築の時間を大幅に短縮することを実証的に示す。 いくつかの分類器の分類精度を大幅に向上させ,大規模データセットにおいても提案する特徴構築の実現可能性を示した。
  論文  参考訳（メタデータ） (2023-01-23T18:59:01Z)
• Unified Multi-View Orthonormal Non-Negative Graph Based Clustering Framework [74.25493157757943]
  我々は,非負の特徴特性を活用し,多視点情報を統合された共同学習フレームワークに組み込む,新しいクラスタリングモデルを定式化する。 また、深層機能に基づいたクラスタリングデータに対するマルチモデル非負グラフベースのアプローチを初めて検討する。
  論文  参考訳（メタデータ） (2022-11-03T08:18:27Z)
• Batch-Ensemble Stochastic Neural Networks for Out-of-Distribution Detection [55.028065567756066]
  Out-of-Distribution(OOD)検出は、機械学習モデルを現実世界のアプリケーションにデプロイすることの重要性から、マシンラーニングコミュニティから注目を集めている。 本稿では,特徴量の分布をモデル化した不確実な定量化手法を提案する。 バッチアンサンブルニューラルネットワーク(BE-SNN)の構築と機能崩壊問題の克服を目的として,効率的なアンサンブル機構,すなわちバッチアンサンブルを組み込んだ。 We show that BE-SNNs yield superior performance on the Two-Moons dataset, the FashionMNIST vs MNIST dataset, FashionM。
  論文  参考訳（メタデータ） (2022-06-26T16:00:22Z)
• Attention-driven Graph Clustering Network [49.040136530379094]
  我々は、注意駆動グラフクラスタリングネットワーク(AGCN)という新しいディープクラスタリング手法を提案する。 AGCNは、ノード属性特徴とトポロジグラフ特徴を動的に融合するために、不均一な融合モジュールを利用する。 AGCNは、教師なしの方法で特徴学習とクラスタ割り当てを共同で行うことができる。
  論文  参考訳（メタデータ） (2021-08-12T02:30:38Z)
• Adversarial Feature Augmentation and Normalization for Visual Recognition [109.6834687220478]
  最近のコンピュータビジョンの進歩は、分類モデルの一般化能力を改善するために、逆データ拡張を利用する。 本稿では,中間的特徴埋め込みにおける敵対的拡張を提唱する効率的かつ効率的な代替手法を提案する。 代表的なバックボーンネットワークを用いて,多様な視覚認識タスクにまたがる提案手法を検証する。
  論文  参考訳（メタデータ） (2021-03-22T20:36:34Z)
• New advances in enumerative biclustering algorithms with online partitioning [80.22629846165306]
  さらに、数値データセットの列に定数値を持つ最大二クラスタの効率的で完全で正しい非冗長列挙を実現できる二クラスタリングアルゴリズムであるRIn-Close_CVCを拡張した。 改良されたアルゴリズムはRIn-Close_CVC3と呼ばれ、RIn-Close_CVCの魅力的な特性を保ちます。
  論文  参考訳（メタデータ） (2020-03-07T14:54:26Z)

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

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