論文の概要: Formalizing Piecewise Affine Activation Functions of Neural Networks in Coq

• arxiv url: http://arxiv.org/abs/2301.12893v1
• Date: Mon, 30 Jan 2023 13:53:52 GMT
• ステータス: 処理完了
• システム内更新日: 2023-01-31 14:31:49.737993
• Title: Formalizing Piecewise Affine Activation Functions of Neural Networks in Coq
• Title（参考訳）: CoqにおけるニューラルネットワークのPiecewise Affine活性化関数の形式化
• Authors: Andrei Aleksandrov and Kim V\"ollinger
• Abstract要約: 本稿では,Coq内のニューラルネットワークの検証に適した対話型定理証明器として,pwaアクティベーション関数の最初の形式化を提案する。 概念実証として、一般的なpwaアクティベーション関数ReLUを構築する。 私たちのフォーマル化は、自動証明が失敗する際のフォールバック証明として、ニューラルネットワーク検証のフレームワークにCoqを統合するための道を開くものです。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Verification of neural networks relies on activation functions being piecewise affine (pwa) -- enabling an encoding of the verification problem for theorem provers. In this paper, we present the first formalization of pwa activation functions for an interactive theorem prover tailored to verifying neural networks within Coq using the library Coquelicot for real analysis. As a proof-of-concept, we construct the popular pwa activation function ReLU. We integrate our formalization into a Coq model of neural networks, and devise a verified transformation from a neural network N to a pwa function representing N by composing pwa functions that we construct for each layer. This representation enables encodings for proof automation, e.g. Coq's tactic lra -- a decision procedure for linear real arithmetic. Further, our formalization paves the way for integrating Coq in frameworks of neural network verification as a fallback prover when automated proving fails.
• Abstract（参考訳）: ニューラルネットワークの検証は、部分的アフィン(pwa)である活性化関数に依存している。 本稿では,実解析のためのライブラリCoquelicotを用いて,Coq内のニューラルネットワークを検証するための対話型定理証明器として,pwaアクティベーション関数の最初の形式化を提案する。 概念実証として、一般的なpwaアクティベーション関数ReLUを構築する。 我々は、ニューラルネットワークのCoqモデルにフォーマル化を統合し、ニューラルネットワーク N から N を表す pwa 関数への検証済み変換を、各層で構築する pwa 関数を構成することによって考案する。 この表現は、例えば coq の戦術 lra - a decision procedure for linear real arithmetic など、証明自動化のためのエンコーディングを可能にする。 さらに,当社の形式化は,自動証明が失敗した場合のフォールバック証明として,ニューラルネットワーク検証のフレームワークにcoqを統合する方法を提供します。

関連論文リスト

• ReLUs Are Sufficient for Learning Implicit Neural Representations [17.786058035763254]
  暗黙的神経表現学習におけるReLUアクティベーション関数の使用について再考する。 2次B-スプラインウェーブレットにインスパイアされ、ディープニューラルネットワーク(DNN)の各層にReLUニューロンに一連の簡単な制約を組み込む。 我々は、一般的な信念とは対照的に、ReLUニューロンのみからなるDNNに基づいて最先端のINRを学習できることを実証した。
  論文  参考訳（メタデータ） (2024-06-04T17:51:08Z)
• Permutation Equivariant Neural Functionals [92.0667671999604]
  この研究は、他のニューラルネットワークの重みや勾配を処理できるニューラルネットワークの設計を研究する。 隠れた層状ニューロンには固有の順序がないため, 深いフィードフォワードネットワークの重みに生じる置換対称性に着目する。 実験の結果, 置換同変ニューラル関数は多種多様なタスクに対して有効であることがわかった。
  論文  参考訳（メタデータ） (2023-02-27T18:52:38Z)
• 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)
• A Sparse Coding Interpretation of Neural Networks and Theoretical Implications [0.0]
  深層畳み込みニューラルネットワークは、様々なコンピュータビジョンタスクにおいて前例のない性能を達成した。 本稿では、ReLUアクティベーションを持つニューラルネットワークのスパース符号化解釈を提案する。 正規化やプーリングなしに完全な畳み込みニューラルネットワークを導出する。
  論文  参考訳（メタデータ） (2021-08-14T21:54:47Z)
• Optimal Approximation with Sparse Neural Networks and Applications [0.0]
  深い疎結合ニューラルネットワークを用いて、関数クラスの複雑性を$L(mathbb Rd)$で測定する。 また、ニューラルネットワークを誘導する関数の可算コレクションである表現システムについても紹介する。 次に、レート歪曲理論とウェッジレット構成を用いて、$beta$マンガ的関数と呼ばれるクラスの複雑性を分析する。
  論文  参考訳（メタデータ） (2021-08-14T05:14:13Z)
• On reaction network implementations of neural networks [0.0]
  本稿では,(フィードフォワード)ニューラルネットワークの実装に決定論的にモデル化された化学反応ネットワークの利用について述べる。 ニューラルネットワークのある種の反応ネットワーク実装に付随する常微分方程式(ODE)が望ましい性質を持つことを示す。
  論文  参考訳（メタデータ） (2020-10-26T02:37:26Z)
• How Neural Networks Extrapolate: From Feedforward to Graph Neural Networks [80.55378250013496]
  勾配勾配降下法によりトレーニングされたニューラルネットワークが、トレーニング分布の支持の外で学んだことを外挿する方法について検討する。 グラフニューラルネットワーク(GNN)は、より複雑なタスクでいくつかの成功を収めている。
  論文  参考訳（メタデータ） (2020-09-24T17:48:59Z)
• UNIPoint: Universally Approximating Point Processes Intensities [125.08205865536577]
  学習可能な関数のクラスが任意の有効な強度関数を普遍的に近似できることを示す。 ニューラルポイントプロセスモデルであるUNIPointを実装し,各イベントの基底関数の和をパラメータ化するために,リカレントニューラルネットワークを用いた。
  論文  参考訳（メタデータ） (2020-07-28T09:31:56Z)
• Modeling from Features: a Mean-field Framework for Over-parameterized Deep Neural Networks [54.27962244835622]
  本稿では、オーバーパラメータ化ディープニューラルネットワーク(DNN)のための新しい平均場フレームワークを提案する。 このフレームワークでは、DNNは連続的な極限におけるその特徴に対する確率測度と関数によって表現される。 本稿では、標準DNNとResidual Network(Res-Net)アーキテクチャを通してフレームワークを説明する。
  論文  参考訳（メタデータ） (2020-07-03T01:37:16Z)
• Measuring Model Complexity of Neural Networks with Curve Activation Functions [100.98319505253797]
  本稿では,線形近似ニューラルネットワーク(LANN)を提案する。 ニューラルネットワークのトレーニングプロセスを実験的に検討し、オーバーフィッティングを検出する。 我々は、$L1$と$L2$正規化がモデルの複雑さの増加を抑制することを発見した。
  論文  参考訳（メタデータ） (2020-06-16T07:38:06Z)
• Scalable Partial Explainability in Neural Networks via Flexible Activation Functions [13.71739091287644]
  ディープニューラルネットワーク(NN)によって与えられる高次元の特徴と決定は、そのメカニズムを公開するために新しいアルゴリズムと方法を必要とする。 現在の最先端のNN解釈手法は、NN構造や操作自体よりも、NN出力と入力との直接的な関係に重点を置いている。 本稿では,スケーラブルなトポロジの下でのアクティベーション関数(AF)の役割を象徴的に説明することにより,部分的に説明可能な学習モデルを実現する。
  論文  参考訳（メタデータ） (2020-06-10T20:30:15Z)

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

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