技術要約：ソフトウェアレベルにおける浮動小数点ニューラルネットワークの検証

問題提起

ニューラルネットワークの検証は、理想化された実数値モデルに対して形式的な保証を提供することで大きく進歩してきましたが、これらのアプローチは、展開されるシステムの具体的な実装詳細を考慮できていないことがよくあります。サイバー物理システム（CPS）やIoTなどの安全性が極めて重要なアプリケーションにおいて、ニューラルネットワークは有限精度の浮動小数点演算（通常は32ビットIEEE 754）を使用して実装され、標準的な数学ライブラリ（例：math.h）に依存しています。これらの低レベルの詳細な仕様は、無限精度のモデルから導出された安全性の証明を無効にする可能性のある丸め誤差や非結合的な挙動を導入します。例えば、本論文では、実数演算においては単調増加であるSoftSign活性化関数が、32ビット浮動小数点として実装されると、その性質を失うことを示しています。

ソフトウェアレベルでニューラルネットワークのコードを検証しようとする既存の試みは、混合した結果をもたらしています。ソフトウェア検証器は大規模なニューラルネットワークのインスタンスへのスケーリングに苦慮することが多く、その結果、実務者は非健全な無限精度モデルに戻るか、検証を断念してテストへと切り替えざるを得なくなります。さらに、既存のツールは特定の条件下で誤った結果を出力することが観察されており、それが浮動小数点実装に対する信頼できる安全性オラクルとしての信頼性に疑問を投げかけています。自動ソフトウェア検証器を、特にニューラルネットワークのコードに対して厳密かつ標準化された評価を行うための手法が不足しています。

手法

これらのギャップに対処するため、著者らは8つの最先端の自動ソフトウェア検証器をニューラルネットワークのコードに対して厳密に評価しました。その手法は、主に以下の3つのコンポーネントで構成されています。

1. ベンチマーク構築 (NeuroCodeBench 2.0): 著者らは、912個の検証例を含む包括的なベンチマークを構築しました。このベンチマークは以下を網羅しています：

   • 数学関数: 標準的なmath.h関数の特性（例：単調性、周期性、線形境界）をテストする58のインスタンス。
   • 活性化関数: 一般的な活性化関数（例：ReLU、TanH、SoftSign、GELU）の特性をテストする57のインスタンス。
   • ニューラルレイヤー: アフィン変換、正規化、プーリング、およびSoftMaxレイヤーをカバーする86のインスタンス。
   • フルニューラルネットワーク: Hopfieldネットワーク、SATエンコードされたReLUネットワーク、多項式近似ネットワーク、Lipschitz有界ネットワーク、およびVNN-COMP（確率密度および強化学習タスク）に由来するネットワークを含む711のインスタンス。
   • グラウンドトゥルース（正解）: すべてのインスタンスは、ブルートフォース・テスティング、全探索による構築、または反例生成などの手法を用いて、「安全（safe）」または「不安全（unsafe）」として事前にラベル付けされており、評価のための既知の正しい判定を保証しています。

2. 標準化と互換性: 公平な比較と再現性を確保するため、著者らはすべてのベンチマークインスタンスを、International Competition on Software Verification (SV-COMP) で使用されているフォーマットに変換しました。これには、モデルの実装、安全性プロパティ、および必要な依存関係を含む自己完結型のCファイルを作成することが含まれます。ワークフローには、リソース制限と実行を管理するためのBenchExecフレームワークを利用し、すべてのツールが2024年版SV-COMPで使用されたものと同じ構成で実行されるようにしました。

3. 実験的評価: 本研究では、8つのツール（2LS, CBMC, CPAChecker, DIVINE, ESBMC, PeSCo, Pinaka, UAutomizer）を以下の2つの条件下で評価しました：

   • ベースライン: 平文のベンチマークインスタンスに対して検証器を実行する。
   • オペレーショナルモデル: math.hライブラリの明示的なC実装（MUSLおよびCORE-MATHを使用）を提供し、関数定義を供給することで検証結果が改善されるかどうかを確認する。
   • 歴史的分析: 著者らは、分野の傾向を観察するために、2018年から2026年にわたる1つのツール（ESBMC）の歴史的なパフォーマンスも分析しました。

主な貢献

• NeuroCodeBench 2.0: 浮動小数点ニューラルネットワークのソフトウェアレベルの検証に特化した、大規模でグラウンドトゥルースを持つベンチマークの作成。これには、単純な関数から最大17万個のパラメータを持つフルネットワークまで、幅広いインスタンスが含まれています。
• SV-COMPへの統合: ベンチマークはSV-COMPのインフラストラクチャと互換性のある形式に整えられ、2026年版の公式ベンチマークセットの一部となっています。これにより、標準的なツール構成を用いた自動化された再現可能な評価が可能になります。
• 厳密な評価: ニューラルネットワークのコードに対する8つの最先端ソフトウェア検証器を比較した最初の体系的な研究であり、パフォーマンスと正確性の大きな差異を明らかにしました。
• オペレーショナルモデルの分析: 数学ライブラリ（MUSL、CORE-MATH）の明示的な実装を提供することが検証器のパフォーマンスを向上させるかどうかの調査を行い、その影響はツールに依存しており、多くの場合無視できるか、あるいは負の影響を与えることを明らかにしました。

結果

評価により、ニューラルネットワークのソフトウェア検証に関する現状についてのいくつかの重要な知見が得られました。

• 低い正確性とスケーラビリティ: 結果は「かなり期待外れ」であると記述されました。ツール間にはベンチマーク全体で大きな分散が見られ、最も優れた性能を示したツール（CBMC）でも912インスタンス中371個を正しく解決したのみであり、他のツールはそれよりも大幅に少ない解決数でした。カテゴリごとの平均解決率は様々であり、複雑なカテゴリ（例：強化学習）では解決率がわずか3%にまで落ち込むこともありました。ほとんどのツールは、一度に単一のニューラルレイヤーを検証することすらできませんでした。
• 誤った判定: いくつかのツールは高い割合で誤った結果を出力しました。例えば、CBMCは、ほぼ25%の誤った確定的な判定（主に偽陽性）を出しました。また、PinakaとUAutomizerも顕著なエラー率を示しました。大量のインスタンスを解決したツールの中で、誤った判定を出さなかったのはESBMCのみでした。
• オペレーショナルモデルの影響: 明示的なmath.hの実装（MUSLまたはCORE-MATH）を提供しても、全体的な目に見える改善は見られませんでした。一部のツール（CBMC, ESBMC, Pinaka）では、ライブラリコードの検証に伴う複雑さが増したことにより、パフォーマンスが実際に低下しました。他のツール（CPAChecker, PeSCo）では、解決されたインスタンス数は増加しましたが、これはしばしば誤った判定の急増を伴いました。
• スケーラビリティの限界: ツールはフルニューラルネットワークに対して著しく苦戦しました。強化学習や確率密度のような複雑なカテゴリでは、解決率は1桁台に低下しました。合成ネットワークであっても、ESBMCのようなツールは、タイムアウトする前に非常に小さな幅（例：幅4）のインスタンスしか解決できませんでした。
• 歴史的進展: 2018年から2026年までのESBMCの分析では、非単調ではあるものの、概ね一定の改善が見られました。2022年から2023年にかけての誤った判定の顕著な急増は、k-誘導アルゴリズムの実装エラーに起因しており、これはNeuroCodeBench 1.0のリリース後に修正されました。2024年のNeuroCodeBench 1.0の導入により、コミュニティ全体で誤った判定が劇的に減少しましたが、NeuroCodeBench 2.0（2025年後半）による影響はより緩やかなものでした。

重要性と主張

本論文は、ニューラルネットワークをソフトウェアレベルで検証することは概念的には可能であるものの、既存の最先端のソフトウェア検証器は、まだこのタスクを効果的に扱う準備ができていないと主張しています。研究は、現在のツールは単一のレイヤーを確実にチェックすることすらできず、頻繁に誤った結果を返し、標準的な数学ライブラリへの完全なサポートを欠いていることを強調しています。

著者らは、彼らの研究が検証コミュニティにとって必要な「現実認識（reality check）」として機能すると述べています。既知のグラウンドトゥルースを備えた厳密なベンチマークを提供することで、理想化された検証とソフトウェア実装の間のギャップが、現時点では既存のツールが埋めるにはあまりにも広いことを示しています。論文は、NeuroCodeBenchのリリースが、初期のリリース後の誤った判定の減少によって示されるように、すでに進展を刺激していると述べています。しかし、著者らは、ニューラルネットワークの完全な実装を最悪の数値的偏差に対して認証することは、数学ライブラリへのネイティブなサポートや、浮動小数点演算に適応したカスタム決定手続きを必要とする長期的な課題であると結論付けています。