論文の概要: Lipschitz-Based Robustness Certification Under Floating-Point Execution
- arxiv url: http://arxiv.org/abs/2603.13334v2
- Date: Tue, 17 Mar 2026 04:15:22 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-03-23 08:17:42.314095
- Title: Lipschitz-Based Robustness Certification Under Floating-Point Execution
- Title（参考訳）: 浮動小数点実行によるリプシッツに基づくロバストネス認証
- Authors: Toby Murray,
- Abstract要約: 本研究では,浮動小数点実行の感度に拘束される実算術感度に関する理論を開発する。
浮動小数点実行時のロバスト性に関する音条件を導出する。
- 参考スコア（独自算出の注目度）: 4.441866681085517
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Sensitivity-based robustness certification has emerged as a practical approach for certifying neural network robustness, including in settings that require verifiable guarantees. A key advantage of these methods is that certification is performed by concrete numerical computation (rather than symbolic reasoning) and scales efficiently with network size. However, as with the vast majority of prior work on robustness certification and verification, the soundness of these methods is typically proved with respect to a semantic model that assumes exact real arithmetic. In reality deployed neural network implementations execute using floating-point arithmetic. This mismatch creates a semantic gap between certified robustness properties and the behaviour of the executed system. As motivating evidence, we exhibit concrete counterexamples showing that real arithmetic robustness guarantees can fail under floating-point execution, even for previously verified certifiers, with discrepancies becoming pronounced at lower-precision formats such as float16. We then develop a formal, compositional theory relating real arithmetic Lipschitz-based sensitivity bounds to the sensitivity of floating-point execution under standard rounding-error models, specialised to feed-forward neural networks with ReLU activations. We derive sound conditions for robustness under floating-point execution, including bounds on certificate degradation and sufficient conditions for the absence of overflow. We formalize the theory and its main soundness results, and implement an executable certifier based on these principles, which we empirically evaluate to demonstrate its practicality.
- Abstract（参考訳）: 感度に基づくロバストネス認証は、検証可能な保証を必要とする設定を含む、ニューラルネットワークのロバストネスを認証するための実践的なアプローチとして登場した。
これらの手法の重要な利点は、具体的な数値計算(記号的推論ではなく)によって認証が行われ、ネットワークサイズで効率的にスケールできることである。
しかしながら、ロバスト性証明と検証に関する先行研究の大部分がそうであるように、これらの手法の健全性は通常、正確な実算術を仮定する意味モデルに関して証明される。
実際、デプロイされたニューラルネットワークの実装は浮動小数点演算を用いて実行される。
このミスマッチは、認証された堅牢性特性と実行されたシステムの振る舞いの間に意味的なギャップを生じさせる。
実算術的堅牢性保証が浮動小数点実行時に失敗することを示す具体的な反例を示す。
そこで我々は,ReLUアクティベーションを持つフィードフォワードニューラルネットワークに特化して,実算術リプシッツの感度を標準ラウンドリングエラーモデル下での浮動小数点実行の感度に限定した形式的構成理論を開発した。
浮動小数点実行時のロバスト性に関する音条件を導出する。
我々は理論とその主音性結果を定式化し、これらの原理に基づいて実行可能な証明器を実装し、その実用性を実証的に評価する。
関連論文リスト
- TorchLean: Formalizing Neural Networks in Lean [71.68907600404513]
本稿では,学習モデルを一級数学的対象として扱うフレームワークであるTorchLeanを紹介する。
我々はTorchLeanのエンドツーエンドを、証明された堅牢性、PINNの物理インフォームド残差、Lyapunovスタイルのニューラルコントローラ検証で検証する。
論文 参考訳（メタデータ） (2026-02-26T05:11:44Z) - MathLedger: A Verifiable Learning Substrate with Ledger-Attested Feedback [0.0]
現代のAIシステムは異常なパフォーマンスを達成するが、不透明で検証不可能なままである。
我々は,形式的検証,暗号証明,学習ダイナミクスを統合した,検証可能なマシン認知のための基板であるMathLedgerを紹介する。
この貢献は非構造的であり、大規模な監査性を実現する台帳による学習の実践的なプロトタイプである。
論文 参考訳（メタデータ） (2025-12-22T19:27:55Z) - Fast and Flexible Robustness Certificates for Semantic Segmentation [6.1903263165298945]
そこで我々は,リプシッツ制約を組み込んだ,比較的堅牢なセマンティックネットワークを新たに導入する。
我々のアプローチは、初めて、リアルタイム互換の堅牢なセマンティックセマンティックセグメンテーションを解放する。
当社のアプローチはNVIDIA A100 GPUの同等の証明書を推論してランダムにスムースにする方法よりも約600倍高速であることがわかった。
論文 参考訳（メタデータ） (2025-12-03T10:10:16Z) - No Soundness in the Real World: On the Challenges of the Verification of Deployed Neural Networks [1.3108652488669736]
理論的健全性は実用的健全性を意味するものではないと論じる。
私たちは、デプロイメント環境の特徴を検出し、活用する敵ネットワークを作成します。
テスト対象の検証対象がすべて,新たなデプロイメントアタックに対して脆弱であることを実証しています。
論文 参考訳（メタデータ） (2025-06-01T15:47:37Z) - A Formally Verified Robustness Certifier for Neural Networks (Extended Version) [0.0]
ニューラルネットワークは入力中の小さな摂動の影響を受けやすいため、それらが誤分類される。
グローバルなロバストニューラルネットワークは、入力の分類がそのような摂動によって変更できないことを証明するために機能を使用する。
本稿では,プログラムとその仕様,実装と検証に要する重要な設計決定について述べる。
論文 参考訳（メタデータ） (2025-05-11T12:05:14Z) - Adaptive Hierarchical Certification for Segmentation using Randomized Smoothing [87.48628403354351]
機械学習の認証は、特定の条件下では、敵対的なサンプルが特定の範囲内でモデルを回避できないことを証明している。
セグメンテーションの一般的な認証方法は、平らな粒度のクラスを使い、モデルの不確実性による高い断続率をもたらす。
本稿では,複数レベルの階層内で画素を認証し,不安定なコンポーネントに対して粗いレベルに適応的に認証を緩和する,新しい,より実用的な設定を提案する。
論文 参考訳（メタデータ） (2024-02-13T11:59:43Z) - Mixing Classifiers to Alleviate the Accuracy-Robustness Trade-Off [8.169499497403102]
本稿では、標準ニューラルネットワークとロバストニューラルネットワークの出力確率を混合した理論的動機付け型定式化を提案する。
数値実験により,混合分類器は精度・損耗トレードオフを著しく改善することを確認した。
論文 参考訳（メタデータ） (2023-11-26T02:25:30Z) - The Lipschitz-Variance-Margin Tradeoff for Enhanced Randomized Smoothing [85.85160896547698]
ディープニューラルネットワークの現実的な応用は、ノイズの多い入力や敵攻撃に直面した場合、その不安定な予測によって妨げられる。
入力にノイズ注入を頼りに、認証された半径を持つ効率的な分類器を設計する方法を示す。
新たな認証手法により、ランダムな平滑化による事前学習モデルの使用が可能となり、ゼロショット方式で現在の認証半径を効果的に改善できる。
論文 参考訳（メタデータ） (2023-09-28T22:41: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) - Robust Implicit Networks via Non-Euclidean Contractions [63.91638306025768]
暗黙のニューラルネットワークは、精度の向上とメモリ消費の大幅な削減を示す。
彼らは不利な姿勢と収束の不安定さに悩まされる。
本論文は,ニューラルネットワークを高機能かつ頑健に設計するための新しい枠組みを提供する。
論文 参考訳（メタデータ） (2021-06-06T18:05:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。