Verified-Intelligence/auto_LiRPA

何を解決するか

auto_LiRPA はニューラルネットワークの形式的堅牢性を検証する方法を提供します。入力データやモデルの重みに摂動が加えられた場合に、モデルの出力範囲（境界）を保証できるようにし、特定の制約下でネットワークの予測が安定的かつ予測可能であることを保証します。

動作方法

このライブラリは、PyTorchの計算グラフ上で動作するグラフアルゴリズムに、Linear Relaxation based Perturbation Analysis (LiRPA) アルゴリズムを一般化しています。ユーザーは標準の nn.Module としてモデルを定義し、ライブラリがグラフを走査して任意のノードの境界を自動的に導出し、計算します。実装が微分可能であるため、ネットワークパラメータを最適化して「証明可能な防御」（証明可能な堅牢性を持つモデル）を作成するのに使用できます。

対象ユーザー

AIモデルの形式的堅牢性を証明する必要がある研究者や開発者向けです。特に、ビジョンモデル（ResNet、DenseNet）、シーケンスモデル（LSTM、Transformers）、およびリャプノフ安定性のためのニューラルコントローラーを扱っている方々に適しています。

特徴

• 広範なアルゴリズム対応: CROWN、DeepPoly、$α$-CROWN、$β$-CROWN、IBP、およびハイブリッド手法を実装しています。
• 自動導出: ユーザーが複雑な LiRPA 境界を手動で導出する必要がなく、自動微分のように扱うことができます。
• 多様なモデル対応: ReLU、sigmoid、tanh、maxpool などのさまざまな活性化関数と、Transformers や LSTMs などの複雑なアーキテクチャに対応しています。
• 高性能: メモリ効率の良い GPU 実装とマルチGPUサポートを備えており、ImageNet などの大規模データセットにもスケーラブルです。
• 王冠の成功: $α, β$-CROWN のコアライブラリとして、2021年から2025年まで一貫して VNN-COMP コンペティションで優勝しています。