Precise Verification of Transformers through ReLU-Catalyzed Abstraction Refinement

技術サマリー：ReLU 触媒抽象化精緻化によるトランスフォーマーの厳密検証

問題定義
トランスフォーマーモデルの形式検証は、自動運転や医療といった安全クリティカルなアプリケーションへの展開に伴い、極めて重要となっている。しかし、トランスフォーマーの検証は、特に自己注意層内のドット積に起因する推論計算の高度な複雑さにより、従来のフィードフォワードニューラルネットワーク（FFNN）の検証に比べて著しく困難である。既存の検証手法は、出力範囲の凸上近似を構築するために抽象解釈に依存している。これらは効率的ではあるものの、「完全性の問題」に悩まされることが多い。すなわち、上近似によって生じる大きな誤差により、実際の出力は頑健性を満たしているにもかかわらず近似された出力が頑健性を違反するという、頻繁な偽陽性が発生する。具体的には、現在の最先端手法（例：Shi ら [23]）は、ドット積に対して厳密に健全だがしばしば最適ではない剛体な平面境界を使用しており、2 つの変数の積によって形成される双曲放物面を厳密に境界付けすることに失敗している。

手法
著者は、ドット積に対する複数の平面境界を融合し、それらを ReLU 関数を用いて表現することで精度を向上させる新しい検証フレームワーク BuFFeT（BoUnd Fusing-based reFinEment for Transformers）を提案する。

1. 二重境界構築: 本論文は、先行研究で用いられている標準的な平面境界（式 4）が、ドット積（$z=xy$）を表す双曲放物面の片側のみをカバーしていることを特定する。著者は、反対側をカバーする「二重」の平面境界（式 5）を導出する。
2. ReLU ベース表現: 単に 2 つの平面境界の最小値を取ることで生じる非線形な min/max 関数の伝播による指数関数的な複雑さを回避するため、著者は融合された境界を ReLU 関数を用いて表現する。具体的には、より厳密な上界は元の境界から ReLU 項を減じたものとして、より厳密な下界は元の境界に ReLU 項を加えたものとして定式化される（式 8 および 9）。
3. 抽象化精緻化戦略: 中核的な革新は、これらの ReLU 項の線形緩和を最適化することにある。ReLU の線形下界は、傾き $\alpha \in [0, 1]$ によってパラメータ化される。著者は、最適な $\alpha$ を決定するために、従来の FFNN 検証から 2 つの戦略を拡張する。
   • r-BuFFeT（ルールベース）: 先行研究 [24] のヒューリスティックを適用し、ReLU の入力範囲に基づいて $\alpha$（0 または 1）を選択し、上近似の面積を最小化する。これは、特定のインスタンスに対して 2 つの平面境界のうちより良い方を選択することに相当する。
   • o-BuFFeT（最適化ベース）: $\alpha$ を最適化問題における決定変数として扱う。検証タスクを、ReLU 境界から導出された線形制約の下で損失関数（負のマージンの softplus）を最小化する問題として定式化する。現代の勾配ベースソルバー（例：Adam）を用いて、頑健性を証明する解を見つけるために $\alpha$ を反復的に精緻化し、可能な境界の空間を実質的に探索する。

主要な貢献

• 新規な ReLU の活用: 本論文は、ドット積に対する正確な非線形境界を ReLU 関数を用いて表現する方法を導入し、トランスフォーマー検証と従来のニューラルネットワークにおける ReLU 緩和に関する広範な文献との間のギャップを埋める。
• 理論的統合: 著者は、最先端手法 [23] で用いられている平面境界とその二重境界が、それぞれ $\alpha=0$ および $\alpha=1$ に対応する ReLU ベース表現の特定のインスタンスであることを実証し、なぜこれらの固定された戦略がしばしば最適でないのかを説明する。
• 2 つの新しいフレームワーク: r-BuFFeT と o-BuFFeT の提案は、効率的かつ正確な検証のための 2 つの異なる経路を提供する。特に最適化ベースのアプローチは、頑健性が証明されるまで近似を反復的に精緻化するメカニズムを提供する。

実験結果
著者は、感情分析データセット（SST および Yelp）で学習された 10 個のトランスフォーマーモデル（1 レイヤーから 6 レイヤーまでの標準アーキテクチャおよび TinyBERT を含む）において BuFFeT を評価した。評価には、最先端のベースライン [23] に対する 1,400 件の検証タスクが含まれた。

• 精度: 両方の BuFFeT アプローチは、著しい精度の向上を示した。深いモデル（例：$N=6$）の場合、r-BuFFeT は最大検証摂動（$\epsilon$）を最大で 1.8 倍改善し、o-BuFFeT はベースラインに対して最大で 3.6 倍の改善を達成した。o-BuFFeT は、特に複雑なモデルにおいて r-BuFFeT を一貫して上回った。
• 効率性: r-BuFFeT は ReLU 入力範囲の計算により、ベースラインの 1.1 倍から 1.7 倍の modest な時間オーバーヘッドを伴った。o-BuFFeT は反復最適化プロセスにより、ベースラインの 33 倍から 96 倍のより高いオーバーヘッドを導入した。しかし、著者は、6 レイヤーモデルおよび TinyBERT の検証は数分で完了でき、オーバーヘッド比率はモデルの深さに関わらず安定していると指摘している。
• 頑健性: ベースラインが頑健性の検証に失敗した場合（負のマージン）、o-BuFFeT は近似を精緻化してその性質を証明することに成功し、偽陽性を排除する能力を実証した。

意義と主張
本論文は、BuFFeT が偽陽性につながる近似誤差を削減することで、トランスフォーマー検証の信頼性を著しく向上させると主張している。主な意義は、それが構築する方法論的な架け橋にある。すなわち、ReLU 表現を活用することで、従来のニューラルネットワーク検証から確立された分析手法を、トランスフォーマー固有の課題（特に自己注意ドット積）に適用可能にしている。著者は、この研究をトランスフォーマー検証における将来の研究への道を開くものとして位置づけ、ReLU ベースの精緻化の使用は他のドメインへ拡張可能であり、既存の手法と組み合わせて意味のある NLP 検証を実現できると示唆している。本研究はすべての検証課題を解決すると主張するものではないが、効率性と精度の間の実用的なトレードオフを提供し、最先端を著しく改善するものである。