論文の概要: Abstraction-Based Proof Production in Formal Verification of Neural Networks

• arxiv url: http://arxiv.org/abs/2506.09455v1
• Date: Wed, 11 Jun 2025 07:00:09 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-06-13 06:35:02.670441
• Title: Abstraction-Based Proof Production in Formal Verification of Neural Networks
• Title（参考訳）: ニューラルネットワークの形式的検証における抽象化に基づく証明生成
• Authors: Yizhak Yisrael Elboher, Omri Isac, Guy Katz, Tobias Ladner, Haoze Wu,
• Abstract要約: 本稿では,抽象的検証を実証する新しいフレームワークを提案する。 この作業は、共通の抽象化技術をサポートすることにより、スケーラブルで信頼性の高い検証を可能にすることを目的としている。
• 参考スコア（独自算出の注目度）: 0.7048747239308888
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Modern verification tools for deep neural networks (DNNs) increasingly rely on abstraction to scale to realistic architectures. In parallel, proof production is becoming a critical requirement for increasing the reliability of DNN verification results. However, current proofproducing verifiers do not support abstraction-based reasoning, creating a gap between scalability and provable guarantees. We address this gap by introducing a novel framework for proof-producing abstraction-based DNN verification. Our approach modularly separates the verification task into two components: (i) proving the correctness of an abstract network, and (ii) proving the soundness of the abstraction with respect to the original DNN. The former can be handled by existing proof-producing verifiers, whereas we propose the first method for generating formal proofs for the latter. This preliminary work aims to enable scalable and trustworthy verification by supporting common abstraction techniques within a formal proof framework.
• Abstract（参考訳）: ディープニューラルネットワーク(DNN)の現代的な検証ツールは、現実的なアーキテクチャにスケールするために、抽象化にますます依存している。 並行して、DNN検証結果の信頼性を高める上で、証明生成が重要な要件となっている。 しかし、現在の証明証明検証器は抽象化に基づく推論をサポートしておらず、スケーラビリティと証明可能な保証の間にギャップを生じさせる。 このギャップに対処するために,抽象的なDNN検証を実証する新しいフレームワークを導入する。 私たちのアプローチでは、検証タスクをモジュール的に2つのコンポーネントに分けています。 一 抽象的ネットワークの正しさを証明し、 (II)元のDNNに対する抽象化の健全性を証明すること。 前者は既存の証明生成検証器で処理できるが、後者は形式的証明を生成するための最初の方法を提案する。 この予備的な作業は、形式的な証明フレームワーク内で共通の抽象化技術をサポートすることにより、スケーラブルで信頼性の高い検証を可能にすることを目的としている。

関連論文リスト

• ProofNet++: A Neuro-Symbolic System for Formal Proof Verification with Self-Correction [0.0]
  本稿では,自動定理証明を強化するニューロシンボリックフレームワークProofNet++を提案する。 ProofNet++は,従来のモデルよりも検証精度,正確性,形式的妥当性を著しく向上することを示す。
  論文  参考訳（メタデータ） (2025-05-30T05:44:34Z)
• Advancing Neural Network Verification through Hierarchical Safety Abstract Interpretation [52.626086874715284]
  我々は、安全でない出力の階層構造を検証する抽象的DNN検証と呼ばれる新しい問題定式化を導入する。 出力到達可能な集合に関する抽象的解釈と推論を活用することにより,形式的検証プロセスにおいて,複数の安全性レベルを評価することができる。 我々の貢献には、新しい抽象的安全性の定式化と既存のアプローチとの関係を理論的に探求することが含まれる。
  論文  参考訳（メタデータ） (2025-05-08T13:29:46Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• 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)
• Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks [9.85360493553261]
  ディープニューラルネットワーク(DNN)の実践はますます進んでいるが、ロバストさの欠如により、安全クリティカルなドメインへの応用が妨げられている。 本稿では,スケーラブルで正確なDNN検証のための新しい抽象化・リファインメント手法を提案する。
  論文  参考訳（メタデータ） (2022-07-02T07:04:20Z)
• Toward Certified Robustness Against Real-World Distribution Shifts [65.66374339500025]
  我々は、データから摂動を学ぶために生成モデルを訓練し、学習したモデルの出力に関して仕様を定義する。 この設定から生じるユニークな挑戦は、既存の検証者がシグモイドの活性化を厳密に近似できないことである。 本稿では,古典的な反例誘導的抽象的洗練の概念を活用するシグモイドアクティベーションを扱うための一般的なメタアルゴリズムを提案する。
  論文  参考訳（メタデータ） (2022-06-08T04:09:13Z)
• Neural Network Verification with Proof Production [7.898605407936655]
  そこで本研究では,Simplex ベースの DNN 検証器を実証生産能力で拡張するための新しいメカニズムを提案する。 我々の証明生産は、よく知られたファルカスの補題の効率的な適応に基づいている。 航空機衝突回避のための安全クリティカルシステムの評価は, ほぼすべてのケースにおいて, 証明生産が成功することを示すものである。
  論文  参考訳（メタデータ） (2022-06-01T14:14:37Z)
• Shared Certificates for Neural Network Verification [8.777291205946444]
  既存のニューラルネットワーク検証器は、与えられた摂動の下で各入力が正しく処理されるという証明を計算する。 このプロセスは、各入力に対して独立してスクラッチから繰り返される。 精度を損なわずにこの検証コストを削減する新しい方法を提案する。
  論文  参考訳（メタデータ） (2021-09-01T16:59:09Z)
• Scalable Quantitative Verification For Deep Neural Networks [44.570783946111334]
  ディープニューラルネットワーク(DNN)のためのテスト駆動検証フレームワークを提案する。 本手法は,形式的確率特性の健全性が証明されるまで,十分な試験を行う。 われわれの研究は、現実世界のディープニューラルネットワークが捉えた分布の性質を、証明可能な保証で検証する方法を開拓している。
  論文  参考訳（メタデータ） (2020-02-17T09:53:50Z)

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

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