論文の概要: Neural Model Checking

• arxiv url: http://arxiv.org/abs/2410.23790v1
• Date: Thu, 31 Oct 2024 10:17:04 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-11-01 16:59:51.626458
• Title: Neural Model Checking
• Title（参考訳）: ニューラルモデル検査
• Authors: Mirco Giacobbe, Daniel Kroening, Abhinandan Pal, Michael Tautschnig,
• Abstract要約: 時間論理をモデル化するための機械学習手法を導入し,ハードウェアの形式的検証に適用する。 我々の新しいアプローチは、ニューラルネットワークを線形時間論理の形式証明証明として用いることによって、機械学習と記号推論を組み合わせる。 提案手法は,SystemVerilogで記述された標準的なハードウェア設計において,最先端の学術的,商業的なモデルチェッカーよりも優れていることを示す。
• 参考スコア（独自算出の注目度）: 10.376573742987917
• License:
• Abstract: We introduce a machine learning approach to model checking temporal logic, with application to formal hardware verification. Model checking answers the question of whether every execution of a given system satisfies a desired temporal logic specification. Unlike testing, model checking provides formal guarantees. Its application is expected standard in silicon design and the EDA industry has invested decades into the development of performant symbolic model checking algorithms. Our new approach combines machine learning and symbolic reasoning by using neural networks as formal proof certificates for linear temporal logic. We train our neural certificates from randomly generated executions of the system and we then symbolically check their validity using satisfiability solving which, upon the affirmative answer, establishes that the system provably satisfies the specification. We leverage the expressive power of neural networks to represent proof certificates as well as the fact that checking a certificate is much simpler than finding one. As a result, our machine learning procedure for model checking is entirely unsupervised, formally sound, and practically effective. We experimentally demonstrate that our method outperforms the state-of-the-art academic and commercial model checkers on a set of standard hardware designs written in SystemVerilog.
• Abstract（参考訳）: 時間論理をモデル化するための機械学習手法を導入し,ハードウェアの形式的検証に適用する。 モデルチェックは、与えられたシステムのすべての実行が望ましい時間論理仕様を満たすかどうかという問題に答える。 テストとは異なり、モデルチェックは正式な保証を提供する。 その応用はシリコン設計の標準として期待されており、EDA産業は数十年にわたって、パフォーマンスの象徴的なモデル検査アルゴリズムの開発に投資してきた。 我々の新しいアプローチは、ニューラルネットワークを線形時間論理の形式証明証明として用いることによって、機械学習と記号推論を組み合わせる。 我々は、システムのランダムに生成された実行からニューラルネットワーク証明書をトレーニングし、その妥当性を、肯定的な回答に基づいて、システムが確実に仕様を満たすことを確立した満足度解決を用いて、象徴的に検証する。 我々は、ニューラルネットワークの表現力を活用して証明証明書を表現し、証明書のチェックがそれを見つけるよりもずっと簡単であるという事実も活用する。 その結果、モデル検査のための機械学習手法は、完全に教師なし、公式には健全であり、実用的には有効であることがわかった。 提案手法は,SystemVerilogで記述された標準的なハードウェア設計において,最先端の学術的,商業的なモデルチェッカーよりも優れていることを示す。

関連論文リスト

• Bisimulation Learning [55.859538562698496]
  我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。 提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
  論文  参考訳（メタデータ） (2024-05-24T17:11:27Z)
• Requirement falsification for cyber-physical systems using generative models [1.90365714903665]
  OGANは、システムが運用される前に設計、ソフトウェア、ハードウェアの欠陥を明らかにするシステムの安全性の反例となるインプットを見つけることができる。 OGANはアトミックにテストを実行し、テスト中のシステムの以前のモデルを必要としない。 OGANは、ほとんど努力せずに新しいシステムに適用でき、テスト中のシステムの要件がほとんどなく、最先端のCPSファルシフィケーション効率と有効性を示す。
  論文  参考訳（メタデータ） (2023-10-31T14:32:54Z)
• Representing Timed Automata and Timing Anomalies of Cyber-Physical Production Systems in Knowledge Graphs [51.98400002538092]
  本稿では,学習されたタイムドオートマトンとシステムに関する公式知識グラフを組み合わせることで,CPPSのモデルベース異常検出を改善することを目的とする。 モデルと検出された異常の両方を知識グラフに記述し、モデルと検出された異常をより容易に解釈できるようにする。
  論文  参考訳（メタデータ） (2023-08-25T15:25:57Z)
• How neural networks learn to classify chaotic time series [77.34726150561087]
  本研究では,通常の逆カオス時系列を分類するために訓練されたニューラルネットワークの内部動作について検討する。 入力周期性とアクティベーション周期の関係は,LKCNNモデルの性能向上の鍵となる。
  論文  参考訳（メタデータ） (2023-06-04T08:53:27Z)
• Quantization-aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks [58.195261590442406]
  我々は、逆向きに頑健な量子化ニューラルネットワーク(QNN)の訓練と証明の課題について検討する。 近年の研究では、浮動小数点ニューラルネットワークが量子化後の敵攻撃に対して脆弱であることが示されている。 本稿では、堅牢なQNNをトレーニングするための新しい方法であるQA-IBP(quantization-aware interval bound propagation)を提案する。
  論文  参考訳（メタデータ） (2022-11-29T13:32:38Z)
• Stateless and Rule-Based Verification For Compliance Checking Applications [1.7403133838762452]
  本稿では,インテリジェントなコンプライアンスチェックシステムを構築するための形式的な論理ベースのフレームワークを提案する。 SARVは、ステートレスおよびルールベースの検証問題の全体的な検証プロセスを単純化するために設計された検証フレームワークである。 300のデータ実験に基づいて、SARVベースのコンプライアンスソリューションは、3125レコードのソフトウェア品質データセット上で機械学習メソッドよりも優れています。
  論文  参考訳（メタデータ） (2022-04-14T17:31:33Z)
• Active Learning of Markov Decision Processes using Baum-Welch algorithm (Extended) [0.0]
  本稿では,マルコフ決定過程とマルコフ連鎖を学習するためのBaum-Welchアルゴリズムを再検討し,適応する。 本研究では,本手法を最先端のツールと実証的に比較し,提案手法が正確なモデルを得るために必要な観測回数を大幅に削減できることを実証する。
  論文  参考訳（メタデータ） (2021-10-06T18:54:19Z)
• A Novel Anomaly Detection Algorithm for Hybrid Production Systems based on Deep Learning and Timed Automata [73.38551379469533]
  DAD:DeepAnomalyDetectionは,ハイブリッド生産システムにおける自動モデル学習と異常検出のための新しいアプローチである。 深層学習とタイムドオートマトンを組み合わせて、観察から行動モデルを作成する。 このアルゴリズムは実システムからの2つのデータを含む少数のデータセットに適用され、有望な結果を示している。
  論文  参考訳（メタデータ） (2020-10-29T08:27:43Z)
• Understanding Classifier Mistakes with Generative Models [88.20470690631372]
  ディープニューラルネットワークは教師付き学習タスクに有効であるが、脆弱であることが示されている。 本稿では、生成モデルを利用して、分類器が一般化に失敗するインスタンスを特定し、特徴付ける。 我々のアプローチは、トレーニングセットのクラスラベルに依存しないため、半教師付きでトレーニングされたモデルに適用できる。
  論文  参考訳（メタデータ） (2020-10-05T22:13:21Z)
• Verification of ML Systems via Reparameterization [6.482926592121413]
  確率的プログラムを定理証明器で自動的に表現する方法を示す。 また、ベイズ仮説テストで用いられるヌルモデルは、人口統計学的パリティ(英語版)と呼ばれる公平性基準を満たすことを証明した。
  論文  参考訳（メタデータ） (2020-07-14T02:19:25Z)
• High-level Modeling of Manufacturing Faults in Deep Neural Network Accelerators [2.6258269516366557]
  Googleのユニットプロセッシング(TPU)は、ニューラルネットワークアクセラレータで、ニューラルネットワークのクラック内での計算にsystolic配列ベースの行列乗算ハードウェアを使用する。 行列乗算ユニットの任意の状態要素における欠陥は、これらの推論ネットワークにおいて予期せぬ誤りを引き起こす可能性がある。 離散時間マルコフ連鎖(DTMC)形式を用いたTPUにおける永久断層の定式化とその伝播モデルを提案する。
  論文  参考訳（メタデータ） (2020-06-05T18:11:14Z)

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

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