論文の概要: Floating-Point Neural Network Verification at the Software Level

• arxiv url: http://arxiv.org/abs/2510.23389v1
• Date: Mon, 27 Oct 2025 14:43:19 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-28 15:28:15.576264
• Title: Floating-Point Neural Network Verification at the Software Level
• Title（参考訳）: ソフトウェアレベルでの浮動小数点ニューラルネットワーク検証
• Authors: Edoardo Manino, Bruno Farias, Rafael Sá Menezes, Fedor Shmarov, Lucas C. Cordeiro,
• Abstract要約: ニューラルネットワークコンポーネントの動作は、安全クリティカルなシステムにデプロイする前に、正しく証明されなければならない。 既存のニューラルネットワーク検証技術は、ソフトウェアレベルでの欠陥の欠如を証明できない。 浮動小数点の実装を明示的に推論することで、ニューラルネットワークが安全であることを特定し、検証する方法を示す。
• 参考スコア（独自算出の注目度）: 2.228696309685013
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The behaviour of neural network components must be proven correct before deployment in safety-critical systems. Unfortunately, existing neural network verification techniques cannot certify the absence of faults at the software level. In this paper, we show how to specify and verify that neural networks are safe, by explicitly reasoning about their floating-point implementation. In doing so, we construct NeuroCodeBench 2.0, a benchmark comprising 912 neural network verification examples that cover activation functions, common layers, and full neural networks of up to 170K parameters. Our verification suite is written in plain C and is compatible with the format of the International Competition on Software Verification (SV-COMP). Thanks to it, we can conduct the first rigorous evaluation of eight state-of-the-art software verifiers on neural network code. The results show that existing automated verification tools can correctly solve an average of 11% of our benchmark, while producing around 3% incorrect verdicts. At the same time, a historical analysis reveals that the release of our benchmark has already had a significantly positive impact on the latter.
• Abstract（参考訳）: ニューラルネットワークコンポーネントの動作は、安全クリティカルなシステムにデプロイする前に、正しく証明されなければならない。 残念ながら、既存のニューラルネットワーク検証技術では、ソフトウェアレベルでの欠陥の欠如を証明できない。 本稿では,その浮動小数点実装を明示的に推論することで,ニューラルネットワークが安全であることを特定し,検証する方法を示す。 そこで我々は、アクティベーション関数、共通層、最大170Kパラメータの完全なニューラルネットワークをカバーする912のニューラルネットワーク検証例からなるベンチマークであるNeuroCodeBench 2.0を構築した。 我々の検証スイートは、平易なCで書かれており、国際ソフトウェア検証コンペティション(SV-COMP)のフォーマットと互換性がある。 これにより、ニューラルネットワークコード上で8つの最先端ソフトウェア検証器の厳密な評価を行うことができる。 その結果、既存の自動検証ツールは、ベンチマークの平均11%を正しく解き、約3%の誤判定を生成できることがわかった。 同時に、過去の分析によると、我々のベンチマークのリリースは、すでに後者に大きなポジティブな影響を与えている。

関連論文リスト

• Verified Neural Compressed Sensing [58.98637799432153]
  精度の高い計算タスクのために、初めて(私たちの知識を最大限に活用するために)証明可能なニューラルネットワークを開発します。 極小問題次元(最大50)では、線形および双項線形測定からスパースベクトルを確実に回復するニューラルネットワークを訓練できることを示す。 ネットワークの複雑さは問題の難易度に適応できることを示し、従来の圧縮センシング手法が証明不可能な問題を解く。
  論文  参考訳（メタデータ） (2024-05-07T12:20:12Z)
• NeuroCodeBench: a plain C neural network benchmark for software verification [4.9975496263385875]
  本稿では,通常のC言語で記述されたニューラルネットワークコードの検証ベンチマークであるNeuroCodeBenchを提案する。 そこには、数学ライブラリ、アクティベーション関数、エラー修正ネットワーク、転送関数近似、確率密度推定、強化学習の6つのカテゴリに分けられる607の安全性特性を持つ32のニューラルネットワークが含まれている。
  論文  参考訳（メタデータ） (2023-09-07T10:19:33Z)
• Fully Automatic Neural Network Reduction for Formal Verification [8.017543518311196]
  到達可能性解析を用いたニューラルネットワークの完全自動・音量低減手法を提案する。 音質は、低減されたネットワークの検証が元のネットワークの検証を必要とすることを保証します。 我々のアプローチは、大きなニューラルネットワークを元のニューロンのごく一部に減らし、検証時間を同様の程度に短縮する。
  論文  参考訳（メタデータ） (2023-05-03T07:13:47Z)
• 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)
• Can pruning improve certified robustness of neural networks? [106.03070538582222]
  ニューラルネット・プルーニングはディープ・ニューラル・ネットワーク(NN)の実証的ロバスト性を向上させることができることを示す。 実験の結果,NNを適切に刈り取ることで,その精度を8.2%まで向上させることができることがわかった。 さらに,認証された宝くじの存在が,従来の密集モデルの標準および認証された堅牢な精度に一致することを観察する。
  論文  参考訳（メタデータ） (2022-06-15T05:48:51Z)
• Verifying Low-dimensional Input Neural Networks via Input Quantization [12.42030531015912]
  本稿では,ACAS Xu ネットワーク検証の当初の問題を再考する。 本稿では,入力量子化層をネットワークにプリペイドすることを提案する。 本手法は,浮動小数点誤差に耐性のない正確な検証結果を提供する。
  論文  参考訳（メタデータ） (2021-08-18T03:42:05Z)
• Fast Falsification of Neural Networks using Property Directed Testing [0.1529342790344802]
  本稿では,反例の探索を指示するニューラルネットワークの偽造アルゴリズムを提案する。 提案アルゴリズムは, 微分自由サンプリングに基づく最適化手法を用いる。 フェールシフィケーション手順は、他の検証ツールが安全でないと報告しているすべての安全でないインスタンスを検出する。
  論文  参考訳（メタデータ） (2021-04-26T09:16:27Z)
• Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming [97.40955121478716]
  本稿では,ネットワークアクティベーションの総数にのみ線形なメモリを必要とする一階二重SDPアルゴリズムを提案する。 L-inf の精度は 1% から 88% ,6% から 40% に改善した。 また,変分オートエンコーダの復号器に対する2次安定性仕様の厳密な検証を行った。
  論文  参考訳（メタデータ） (2020-10-22T12:32:29Z)
• Exploiting Verified Neural Networks via Floating Point Numerical Error [15.639601066641099]
  検証者は、ニューラルネットワークが空間内のすべての入力に対して特定の特性を保証するかどうかに答えようとしている。 浮動小数点誤差の無視は、実際に体系的に活用できる不健全な検証につながることを示す。
  論文  参考訳（メタデータ） (2020-03-06T03:58:26Z)

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

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