論文の概要: Achieving the Tightest Relaxation of Sigmoids for Formal Verification

• arxiv url: http://arxiv.org/abs/2408.10491v2
• Date: Thu, 22 Aug 2024 00:10:24 GMT
• ステータス: 処理完了
• システム内更新日: 2024-08-23 12:32:33.527328
• Title: Achieving the Tightest Relaxation of Sigmoids for Formal Verification
• Title（参考訳）: 形式的検証のためのシグモイドの最大緩和
• Authors: Samuel Chevalier, Duncan Starkenburg, Krishnamurthy Dvijotham,
• Abstract要約: 本稿では,シグイド関数の上下の調整可能な超平面を導出する。 $alpha$-sigにより、Sigoidアクティベーション関数の可能な、要素単位の凸緩和を形式的な検証フレームワークに容易に組み込むことができる。
• 参考スコア（独自算出の注目度）: 9.118502451414082
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: In the field of formal verification, Neural Networks (NNs) are typically reformulated into equivalent mathematical programs which are optimized over. To overcome the inherent non-convexity of these reformulations, convex relaxations of nonlinear activation functions are typically utilized. Common relaxations (i.e., static linear cuts) of "S-shaped" activation functions, however, can be overly loose, slowing down the overall verification process. In this paper, we derive tuneable hyperplanes which upper and lower bound the sigmoid activation function. When tuned in the dual space, these affine bounds smoothly rotate around the nonlinear manifold of the sigmoid activation function. This approach, termed $\alpha$-sig, allows us to tractably incorporate the tightest possible, element-wise convex relaxation of the sigmoid activation function into a formal verification framework. We embed these relaxations inside of large verification tasks and compare their performance to LiRPA and $\alpha$-CROWN, a state-of-the-art verification duo.
• Abstract（参考訳）: 形式的検証の分野では、ニューラルネットワーク(NN)は通常、最適化された等価な数学的プログラムに書き換えられる。 これらの再構成の本質的にの非凸性を克服するために、非線形活性化関数の凸緩和が典型的に利用される。 しかしながら、「S字型」活性化関数の一般的な緩和(すなわち、静的線形切断)は、過度に緩くなり、全体の検証プロセスが遅くなる。 本稿では,シグモイド活性化関数を上下に有界な調整可能な超平面を導出する。 双対空間でチューニングされると、これらのアフィン境界はシグモイド活性化関数の非線形多様体の周りで滑らかに回転する。 このアプローチは$\alpha$-sigと呼ばれ、シグモイド活性化関数の最も強固で、要素的な凸緩和を形式的な検証フレームワークに組み込むことができる。 大規模な検証タスクにこれらの緩和を組み込み、そのパフォーマンスをLiRPAや最先端の検証デュオである$\alpha$-CROWNと比較する。

関連論文リスト

• Tightening convex relaxations of trained neural networks: a unified approach for convex and S-shaped activations [0.0]
  本研究では,アフィン関数を持つ活性化成分の密接な凸化を導出する公式を開発する。 我々の手法は、分離された超平面を効率的に計算したり、様々な設定に存在しないと判断したりすることができる。
  論文  参考訳（メタデータ） (2024-10-30T18:09:53Z)
• Rotated Runtime Smooth: Training-Free Activation Smoother for accurate INT4 inference [54.2589824716527]
  大規模言語モデルは、その大規模なため、相当な計算とメモリ移動コストを発生させる。 既存のアプローチでは、外れ値と通常の値を2つの行列に分けたり、アクティベーションからウェイトに移行したりしています。 Smooth と Rotation 操作からなる量子化のためのプラグ・アンド・プレイ・アクティベーション・スムーザである Rotated Smooth (RRS) を提案する。 提案手法は,LLaMAおよびQwenファミリーにおける最先端の手法より優れており,IF4推論におけるWikiText-2の難易度は57.33から6.66に向上している。
  論文  参考訳（メタデータ） (2024-09-30T14:59:22Z)
• Stable Nonconvex-Nonconcave Training via Linear Interpolation [51.668052890249726]
  本稿では,ニューラルネットワークトレーニングを安定化(大規模)するための原理的手法として,線形アヘッドの理論解析を提案する。 最適化過程の不安定性は、しばしば損失ランドスケープの非単調性によって引き起こされるものであり、非拡張作用素の理論を活用することによって線型性がいかに役立つかを示す。
  論文  参考訳（メタデータ） (2023-10-20T12:45:12Z)
• Linear Oscillation: A Novel Activation Function for Vision Transformer [0.0]
  線形振動(LoC)活性化関数を$f(x) = x times sin(alpha x + beta)$と定義する。 非線型性を主に導入する従来の活性化関数とは違い、LoCは線形軌道と振動偏差をシームレスにブレンドする。 私たちの経験的研究によると、多様なニューラルネットワークに組み込むと、LoCアクティベーション機能は、ReLUやSigmoidといった確立したアーキテクチャよりも一貫して優れています。
  論文  参考訳（メタデータ） (2023-08-25T20:59:51Z)
• Promises and Pitfalls of the Linearized Laplace in Bayesian Optimization [73.80101701431103]
  線形化ラプラス近似(LLA)はベイズニューラルネットワークの構築に有効で効率的であることが示されている。 ベイズ最適化におけるLLAの有用性について検討し,その性能と柔軟性を強調した。
  論文  参考訳（メタデータ） (2023-04-17T14:23:43Z)
• Neural Network Verification as Piecewise Linear Optimization: Formulations for the Composition of Staircase Functions [2.088583843514496]
  混合整数計画法(MIP)を用いたニューラルネットワーク検証手法を提案する。 ネットワーク内の各ニューロンに対して一方向線形活性化関数を用いた強い定式化を導出する。 また、入力次元において超線形時間で実行される分離手順を導出する。
  論文  参考訳（メタデータ） (2022-11-27T03:25:48Z)
• Active Nearest Neighbor Regression Through Delaunay Refinement [79.93030583257597]
  近接回帰に基づく能動関数近似アルゴリズムを提案する。 我々のActive Nearest Neighbor Regressor (ANNR) は計算幾何学の Voronoi-Delaunay フレームワークに頼り、空間を一定の関数値のセルに分割する。
  論文  参考訳（メタデータ） (2022-06-16T10:24:03Z)
• Exploring Linear Feature Disentanglement For Neural Networks [63.20827189693117]
  Sigmoid、ReLU、Tanhなどの非線形活性化関数は、ニューラルネットワーク(NN)において大きな成功を収めた。 サンプルの複雑な非線形特性のため、これらの活性化関数の目的は、元の特徴空間から線形分離可能な特徴空間へサンプルを投影することである。 この現象は、現在の典型的なNNにおいて、すべての特徴がすべての非線形関数によって変換される必要があるかどうかを探求することに興味をそそる。
  論文  参考訳（メタデータ） (2022-03-22T13:09:17Z)
• LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions [4.03308187036005]
  LinSyn は任意の任意の活性化関数に対して厳密な境界を達成する最初のアプローチである。 提案手法は,2～5倍の出力バウンダリと4倍以上の信頼性を達成できることを示す。
  論文  参考訳（メタデータ） (2022-01-31T17:00:50Z)
• Multiway Non-rigid Point Cloud Registration via Learned Functional Map Synchronization [105.14877281665011]
  我々は、点雲上に定義された学習関数に関する地図を同期させることにより、複数の非剛体形状を登録する新しい方法であるSyNoRiMを提案する。 提案手法は,登録精度において最先端の性能を達成できることを実証する。
  論文  参考訳（メタデータ） (2021-11-25T02:37:59Z)
• Parametric Rectified Power Sigmoid Units: Learning Nonlinear Neural Transfer Analytical Forms [1.6975704972827304]
  本稿では,線形畳み込み重みと非線形活性化関数のパラメトリック形式を共用する双対パラダイムの表現関数を提案する。 関数表現を実行するために提案された非線形形式は、整形パワーシグモイド単位と呼ばれる新しいパラメトリック神経伝達関数のクラスに関連付けられる。 浅層学習と深層学習の両フレームワークにおいて,畳み込み型および整流型シグモイド学習パラメータの連成学習により達成された性能を示す。
  論文  参考訳（メタデータ） (2021-01-25T08:25:22Z)

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

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