Repair Instead of Retraining: A Constraint-Guided Framework for Neural Network Repair

技術要約：再学習ではなく修復を：ニューラルネットワーク修復のための制約誘導型フレームワーク

問題提起
安全性が極めて重要なアプリケーションに展開されている深層ニューラルネットワーク（DNN）は、敵対的摂動やバックドア攻撃に対して依然として脆弱である。再学習やファインチューニングはこれらの問題を軽減できるが、こうしたアプローチは計算コストが高く、すでにデプロイされたモデルに対して選択的に適用することが困難であり、観察された特定の欠陥を超えた制御不能な挙動のドリフトを引き起こすリスクがある。既存の修復手法は、解釈性に乏しいヒューリスティック探索（グレーボックス法）に依存するか、あるいはスケーラビリティに課題のある形式的なアーキテクチャ変換や手動で指定されたポリトープ制約（証明可能手法）を必要とすることが多い。そのため、フルリトレーニングを行うことなく、解釈性、挙動の忠実度、および計算コストのバランスをとるポストホック（事後的）な修復アプローチが求められている。

手法
著者らは、ニューラルネットワークの修復を、局所的なパラメータの疎な集合に対する論理認識型の最適化問題として扱う、構成可能な制約誘導型フレームワークを提案している。このフレームワークは、以下の4つの結合されたステージで動作する。

1. 欠陥の局所化（Fault Localization）: システムは DeepSHAP を使用して、良性入力と敵対的入力の両方に対するニューロンレベルの寄与度マスクを計算する。これにより、「攻撃時のみ」に反応するニューロン（敵対的入力下では高い寄与度を示すが、良性入力下では低い寄与度を示すもの）を特定する。この対照的な寄与度が、疎な欠陥関連重みを特定するための信号となる。
2. 修復対象の選択（Repair-Target Selection）: 特定されたニューロンに基づき、ネットワークパラメータ上に疎なバイナリマスク（$\Theta_S$）を生成する。フレームワークは以下の設計空間を探索する：
   • 重みの方向（Weight Direction）: 重要なニューロンへの入力重み、出力重み、またはバイアスを修正する。
   • 選択ポリシー（Selection Policy）: パーセンタイル閾値（例：上位5%の大きさ）による重みの選択、または固定された予算（$k$）によるランダムな選択。
3. パス制約の仕様策定（Path-Constraint Specification）: 修復の意図を、コンコリック実行（PyCT経由）を用いたパスレベルの制約としてエンコードする。
   • ハード制約（Hard Constraints）: 正しい内部分岐ロジックを維持するために、良性トレースから導出される。
   • ソフト制約（Soft Constraints）: 観察された誤ったパスから実行を回避するように強制するために、敵対的トレースから導出される。
   • サロゲートネットワーク（Surrogate Networks）: フルスケールのネットワークをMax-SMTソルバにエンコードすることの困難さに対処するため、フレームワークは2つの解析用サロゲートを導入する：
     • $N^\Delta_w$（三値サロゲート）: 非修復重みを大きさに基づいて $\{-1, 0, +1\}$ にマッピングし、数式の複雑さを軽減する。
     • $N^\Delta_i$（活性化ゲート型サロゲート）: 入力の活性化量に基づいて非修復エッジを削減する。
   • 決定的な点として、修復対象の重み（$\Theta_S$）はすべての定式化において正確な記号的未知数のまま保持されるが、非修復成分は簡略化またはゲート化される。
4. 制約誘導型修復と検証（Constraint-Guided Repair & Validation）: システムは、候補となる重みの更新を合成するために、Z3を用いた Top-K Max-SMT 問題を解く。候補は、元のデプロイメントネットワーク $N$ 上での 忠実な検証（faithful validation）（正確なアフィン演算を使用）を通じて算出されたバランスの取れたスコアに基づいてランク付けされる。これにより、報告されるメトリクスがサロゲートのアーティファクトではなく、実際の実行時の挙動を反映することを保証する。

主な貢献

• 構成可能な論理認識型フレームワーク: DeepSHAPによる局所化、コンコリック・パス制約抽出、三値/活性化ゲート型サロゲート、およびMax-SMT最適化を組み合わせた統一されたパイプライン。
• 形式化された修復設計空間: 著者らは、ニューロンのソース（攻撃時のみ vs 共通）、重みの方向（入力、出力、バイアス）、および列方向の選択ポリシーの相互作用を明示的に特性化し、単一の「レシピ」が普遍的に最適であることはないことを示している。
• エンコーディング時の厳格な簡略化: 数式の複雑さを抑えつつ、修復のセマンティクスを変更せずにコンコリック制約を扱いやすくするために、共通部分式除去、否定正規化、および式削減などの手法が導入されている。
• サロゲート定式化: $N^\Delta_w$ および $N^\Delta_i$ の導入により、修復変数については正確な記号表現を維持したまま、簡略化されたモデル上でパス制約を収集することが可能になる。
• 忠実な検証プロトコル: すべての精度および攻撃成功率（ASR）が元のネットワーク $N$ 上で測定される厳格な評価手法であり、制約の収集と最終的な性能評価を切り離している。

実験結果
本フレームワークは、6つのベンチマーク（Fashion-MNIST, MNIST-BD, CIFAR-10, GTSRB, MNIST-6, ResNet18）における4,737回の試行を通じて評価された。主な知見は以下の通りである：

• バックドア・ベンチマーク: Fashion-MNISTおよびMNIST-BDにおいて、フレームワークはほぼ完全なバックドア除去を達成した。具体的には、ASRは（Fashion-MNISTで 99.77% $\to$ 6.66% のように）極めて高い値から 8% 未満へと低下し、同時にクリーンな精度を維持またはわずかに向上させた。最も効果的な構成は、出力重みの修正と**活性化ゲート型サロゲート（$N^\Delta_i$）**の使用であった。
• 敵対的ベンチマーク: 重要な発見は、**バイアスのみの修復（bias-only repair）**の有効性である。MNIST-6において、バイアス方向の修復はASRを100%から5.81%に減少させ、クリーンな精度を100%維持した。ResNet18においては、ASRを85.51%から40.42%に減少させた。この方向性は、入力または出力重みにのみ焦点を当ててきた従来の手法では見落とされていた、未探索の領域である。
• スケーラビリティの限界: CIFAR-10およびGTSRBは、単一層の修復においては困難であることが示された。部分的な改善は見られたものの、GTSRBではASRの減少は最小限であり、これは単一層の制約が複雑で分散した欠陥には不十分であるという、トレードオフ（計算量と忠実度の相克）を浮き彫りにした。
• CAREとの比較: グレーボックス手法であるCARE（因果関係に基づく局所化 + PSO）と比較して、提案フレームワークは一般に、Fashion-MNISTおよびMNIST-BDにおいて、より低いASRとより高いクリーン精度を実現し、かつ実行時間は大幅に短かった（例：MNIST-BDで 74.4秒 vs 8,745秒）。しかし、CAREはGTSRBにおいて完全なバックドア除去を達成しており、これは提案手法の単一層というスコープが、特定のアーキテクチャにおける制限要因であることを示唆している。

意義と主張
本論文は、単一のヒューリスティックがすべてのシナリオで支配的になることはないため、修復設計空間の体系的な探索が効果的な構成を発見するために不可欠であると主張している。著者らは、バイアス方向の修復が、敵対的修正のための重要かつこれまで未探索であったオプションであり、この体系的なアプローチを通じてのみ発見可能であることを強調している。

本研究は、ヒューリスティック探索と形式検証の中間領域に位置づけられる。グレーボックス手法よりも解釈性と論理的制御を提供しつつ、形式的な証明手法のようなアーキテクチャの変換や手動によるポリトープの指定を必要としない。著者らは、本フレームワークが制約誘導型ではあるが、形式的に保証されたものではないことを謙虚に認めている。つまり、Max-SMTを用いて合成を行っているものの、最終的な保証は、全入力空間に対する形式的な証明ではなく、デプロイメントネットワークに対する忠実な検証に基づく経験的なものである。結果は、強力な簡略化（サロゲートにおける $\Delta$ の増大）は計算時間を短縮する一方で、適切に調整しなければ修復の指針を歪めてしまうという、計算量と忠実度のトレードオフを浮き彫りにしている。