技術的概要：ホモグラフィの形式的検証におけるリプシッツ最適化

1. 問題定義

自動運転、航空宇宙、医療などの安全クリティカルな分野における深層ニューラルネットワーク（DNN）の展開には、形式的なロバスト性保証が不可欠である。現在の形式的検証手法は、主に画素空間に直接作用する$\ell_p$ノルム有界な摂動（例：ノイズ、コントラスト変化）に焦点を当てている。しかし、これらのアプローチは、カメラの運動、視点の変化、またはシーン幾何学のシフトなど、物理的な 3D 世界に由来する摂動を十分にモデル化できていない。

理論的には$\ell_p$ボールが物理的摂動の結果生じる画像を包含し得るが、それらは摂動画像の真の多様体を過大評価し、緩く、情報に乏しい境界をもたらす。その結果、ネットワークのロバスト性を証明できないことが頻繁に起こる。3D ロバスト性に関する既存の手法は、統計的アプローチ（より弱い保証）、2D アフィン変換（透視効果をモデル化できない）、または明示的な 3D シーンモデルを必要とする複雑なシミュレーションに限定されている。3D カメラ運動下における平面の異なる視点間の平面から平面への写像を記述するホモグラフィ、すなわち射影幾何学変換の形式的検証において、重要なギャップが存在する。

2. 手法

著者らは、主に平面構造（例：道路標示、交通標識、地面）を有するシーンにおいて、撮影カメラの 3D 運動摂動に対するロバスト性を対象とした形式的検証フレームワークを提案する。

2.1. 閉形式ホモグラフィ導出

この手法は、カメラ姿勢の摂動から画素値への閉形式写像の確立から始まる。

• 幾何学モデリング: ピンホールカメラモデルと平面シーンの特徴（例：世界座標系における$z=0$）を仮定し、6 自由度のカメラ姿勢摂動（ロール、ピッチ、ヨー、および並進）によって誘発されるホモグラフィ行列$H(\kappa)$を導出する。
• パラメータ化: ホモグラフィは、基準カメラに対する姿勢の差分を表すベクトル$\kappa$によってパラメータ化される。特定のシナリオ（例：純粋なヨー回転）において、著者らは$H(\kappa)$およびその逆行列$H^{-1}(\kappa)$に対する明示的な解析式を導出する。
• 画素値関数: 変換された画素$G(\kappa)$の値は、変換された座標を$T^{-1}(\kappa)$を介して元の画像に写像し、双線形補間を適用することで計算される。これにより、非線形関数$G(\kappa) = I \circ T^{-1}(\kappa)$が得られる。

2.2. 区分的線形（PWL）近似とリプシッツ最適化

ネットワークを検証するためには、非線形関数$G(\kappa)$を検証器を通じて伝播可能な線形境界によって過大評価する必要がある。

• 区分的線形境界: パラメータ空間$B$を部分領域に分割する。各部分領域内において、関数$G(\kappa)$は Batten ら [7] のアプローチに従い、サンプリングされた点から導出された線形境界（$LB$および$UB$）によって近似される。
• リプシッツ連続性: 境界が健全であること（すなわち、真の関数値を厳密に包含すること）を確保するため、著者らは$G(\kappa)$のリプシッツ連続性を分析する。逆変換$T^{-1}(\kappa)$の勾配を計算することで、リプシッツ定数$L$の解析的上界を導出する。
• 不連続性の処理: 著者らは、臨界角度（分母がゼロに近づく点）におけるホモグラフィ逆行列の不連続性に対処する。微分可能性の定義域$Diff(B)$を定義し、最大勾配の候補位置（境界および特定の arctangent 値）を特定して、有効なリプシッツ定数を計算する。
• 最適化: リプシッツ最適化を用いて、アルゴリズムは反復的に境界を精緻化する。サンプリング点において関数を評価し、リプシッツ定数を用いて境界違反のグローバル最大値を境界付ける。境界違反が閾値$\epsilon$を超えた場合、部分領域を分割し、収束するまでこのプロセスを繰り返す。

2.3. 実装

この手法は、任意の下流の検証器に対して線形境界を生成するフロントエンドとして実装されている。著者らはVENUS検証器を適応させ、これらの区分的線形境界を処理可能とし、固定区間ではなく線形入力制約から活性化前の境界を導出するように、その境界伝播フレームワークを強化した。

3. 主要な貢献

1. 射影変換の形式的検証: 本論文は、6 自由度の姿勢摂動によって誘発される閉形式ホモグラフィを導出し、それらが区分的線形制約およびリプシッツ最適化と互換性があることを実証する。これにより、非アフィン（射影）変換下における画素値に対して証明可能な厳密な境界が可能となる。
2. 効率的な実装: 著者らは、既存の PWL アルゴリズム [7] を上回る効率的な実装を提供する。改良点には、正確な勾配のための半画素補正、リプシッツ候補セットに省略されたパラメータ値を含めること、パラメータ空間における二分法、および画素レベルの並列化が含まれる。
3. ベンチマークとケーススタディ: この手法は、VNN-COMP ベンチマーク（MNIST、CIFAR-10、GTSRB）および実世界の滑走路視認性分類器において評価された。

4. 結果

• パフォーマンスの向上: PWL アルゴリズム [7] の再実装と比較して、提案手法は実行時間で最大89% の高速化、複雑な画素曲線における境界の7% の厳密化を達成した。小規模な変換においては、Branch-and-Bound（BaB）反復が 71% 以上削減された。
• 脆弱性の発見: VNN-COMP ベンチマークにおける評価により、標準的なデータ拡張（$\ell_p$ノルム攻撃を含む）で訓練されたネットワークは、3D 幾何学的摂動に対して体系的な弱点を示すことが明らかになった。例えば、GTSRB（自動運転）モデルは、3D 摂動（ロール、ピッチ、ヨー、および並進）に対して0% の証明済みロバスト性を示した。MNIST および CIFAR モデルさえも、$\ell_p$ノルム摂動と比較して、ピッチ、ヨー、および並進に対して著しく低いロバスト性を示した。
• 実世界のケーススタディ: LARD データセットで訓練された滑走路視認性分類器に適用した結果、10 cm の並進下ではテスト画像のわずか16%、1 度の回転下では**1%**のみがロバスト性証明を受けた。これは、安全クリティカルな知覚システムにおける実用的な脆弱性を浮き彫りにした。
• 感度分析: 本研究は、変換の振幅（例：ヨー角）が増大するにつれて証明済みロバスト性が低下することを確認した。これは、領域分割を必要とする形式的検証における既知の課題である。

5. 意義と主張

本論文は、複雑なシミュレーション、代理ネットワーク、または明示的な画像形成モデルに依存しない、射影幾何学変換のための最初の形式的検証フレームワークを提示すると主張している。平面シーンにおけるホモグラフィの解析的な扱いやすさを活用することで、著者らは 2D アフィン検証と完全な 3D シーンモデリングの間のギャップを埋めている。

その意義は以下の点にある：

• 規制遵守: カメラ運動が不確実性の主要な源である安全クリティカルな産業（航空、自動運転車）において、AI の認証に必要な数学的保証を提供すること。
• 方法論的進展: 以前は形式的検証において解析的に扱い不可能と考えられていた、非アフィンで透視歪みを伴う変換を処理するために、リプシッツ最適化および PWL 手法を拡張すること。
• 実用的洞察: 最先端のネットワークが現実的な 3D 摂動に対して脆いことを実証し、ロバスト性訓練または検証が物理的世界のバリエーションに対処するために、$\ell_p$ノルム制約を超えて進化しなければならないことを示唆すること。

著者らは謙虚なトーンを維持し、大規模な変換は非線形性を悪化させ、この手法は現在、限られたパララックスと遮蔽を有する主に平面のシーンに最も適していることを認めている。彼らは、ロボット工学およびコンピュータビジョンにおける多様なユースケースを検証するための原理的な中間解として、自身の研究を位置づけている。