技術的概要：VNN-LIB 2.0：ニューラルネットワーク検証のための厳密な基盤

問題提起

ニューラルネットワーク検証コミュニティは、ソルバーと高レベルツール間の相互運用性を促進するために、VNN-LIB 標準（バージョン 1.0）にますます依存するようになっています。しかし、バージョン 1.0 には、厳密な形式的基盤として機能することを妨げる 4 つの決定的な欠陥が存在します：

1. 形式的構文の欠如：バージョン 1.0 は問い合わせ言語の構文を形式的に定義していないため、異なるソルバーによって互換性のない実装がもたらされています。
2. 表現力の限界：この標準は、単一の入力と出力を持つ単一のネットワークを前提としています。複数のネットワーク、複数の入力/出力、または隠れ層へのアクセスをネイティブにサポートできず、ユーザーはモデルを人為的に結合することを余儀なくされます。これにより、検証されたアーティファクトとデプロイされたモデルとの間の関係が不明瞭になります。
3. 型システムの欠如：数値型（例えば、浮動小数点数対実数値）を指定するメカニズムが存在しません。これにより、ソルバーが有限精度算術を実数値として扱う際に曖昧さや潜在的な非健全性が生じます。
4. 意味論の欠如：この標準には形式的意味論が存在しないため、ソルバー、問い合わせ生成器、または変換の正しさを形式的に証明することが不可能であり、証明証の発展を阻害しています。

SMT-LIB などの標準とは異なり、VNN-LIB 特有の課題は、問い合わせが自己完結型ではなく、外部のニューラルネットワークモデル（通常は ONNX 形式）の性質を指定する点にあります。ONNX 自体は形式的意味論を持たず、進化を続けているため、厳密な VNN-LIB 標準を定義するには、特定の ONNX バージョンから問い合わせ言語を切り離しつつ、互換性を維持する必要があります。

手法

著者らは、これらの課題に対処するために、VNN-LIB 2.0 の理論的基盤を開発しました。核心的な方法的革新は、ネットワーク理論（$\Psi$）の導入です。

1. ネットワーク理論の抽象化

著者らは、「ネットワーク理論」を、VNN-LIB を定義するためにニューラルネットワークモデル形式から必要とされる最小限の構文、型判定、および意味論を捉える抽象仕様として定義しています。

• 切り離し：$\Psi$ はインターフェースとして機能します。$\Psi$ の具体的な実装（例えば、ONNX v1.20.0 用）は、要素型、テンソル表現、モデル構造、およびノード出力参照に対する具体的な定義を提供します。
• モジュール性：VNN-LIB 2.0 は抽象的な $\Psi$ に対して定義されます。これにより、ONNX が進化しても標準は安定して維持されます。新しい ONNX バージョンに対して必要なのは、VNN-LIB 標準そのものではなく、$\Psi$ のインスタンス化の更新のみです。
• 形式化：構文、型付け、意味論を含む標準全体は、内部の一貫性を確保し曖昧さを排除するために、対話型定理証明器Agdaで機械化されています。

2. 形式的構文と表現力

ネットワーク理論に基づき、著者らは VNN-LIB 2.0 の形式的文法を定義し、表現力を大幅に拡張しました：

• 複数のネットワーク：問い合わせは複数のネットワークを宣言でき、ティーチャー - スチューデント検証やエンコーダ - デコーダアーキテクチャなどのシナリオをサポートします。
• ネットワークの等価性：この標準は、equal-to（正確に同じモデルファイルを参照）と isomorphic-to（同じグラフ構造を持つが、重みが異なる可能性のあるモデルを参照）の宣言を導入します。これにより、ソルバーはネットワークのコピー間で推論（例えば、変数の境界）を共有できます。
• 隠れノード：declare-hidden 構文は、中間層の出力に対する制約を可能にし、エンコーディングやアテンション機構に関する推論に不可欠です。
• 多次元入出力：任意の数の入力と出力をサポートし、マルチモーダルネットワークに対応します。

3. 型システムと意味論

• 型付け：形式的型システムは数値的健全性を強制します。これにより、算術演算や比較が互換性のある型で行われることを保証します（例えば、明示的な強制変換規則なしに float32 と int32 を混合することを防止）。型システムは、基盤となるネットワーク理論 $\Psi$ が提供する判定に依存します。
• 意味論：問い合わせの意味論は、数学的充足可能性問題として定義されます。モデルの集合 $M$（$\Psi$ からインスタンス化されたもの）と入力割り当て $X$ が与えられたとき、すべてのアサーションが真となる割り当てが存在するかどうかを意味論が決定します。
• 実数値問い合わせ：モデルを実数（$\mathbb{R}$）上の関数として扱う既存のソルバーに対応するため、この標準は「実数値問い合わせ」のメカニズムを導入します。区別された real 型を使用することで、問い合わせ作成者は、浮動小数点の精度不足による潜在的な非健全性を認識しつつ、ソルバーがモデルを $\mathbb{R}$ 上で解釈することを明示的に承認します。これは、基本理論から導出された特定のネットワーク理論 $\Psi_{\mathbb{R}}$ を構築することによって達成されます。

主要な貢献

1. ネットワーク理論（$\Psi$）：モデル形式から必要とされる最小限の意味論的インターフェースを定義する新たな抽象化の導入。これにより、VNN-LIB は特定の ONNX バージョンに依存せずに定義可能になります。
2. 形式的構文と文法：複数のネットワーク、隠れ層、複雑な入出力構造をサポートする、正確な文脈自由文法。
3. 形式的型システム：ネットワーク理論に対する数値的型の健全性を強制する型付けシステム。数値表現における曖昧さを解消します。
4. 形式的意味論：ネットワーク理論によってパラメータ化された問い合わせ意味論の厳密な数学的定義。これにより、VNN-LIB を消費または生成するツールの正しさを形式的に証明可能になります。
5. 機械化：完全な標準が Agda で形式化され、規範的な参照実装と機械検証済み証明の基盤を提供しています。
6. 実数値拡張：導出されたネットワーク理論を介した実数値解析のサポートのためのモジュール型アプローチ。健全性の必要性と現在のソルバー能力の現実とのバランスを取ります。

結果と検証

• 内部的一貫性：Agda による形式化は、構文、型付け、意味論の内部的一貫性を検証し、バージョン 1.0 に存在した曖昧さから標準が自由であることを保証します。
• 表現力の実証：本論文は、ネットワーク理論 $\Psi$ の単純な変換が実数値問い合わせの完全なインスタンスを生み出すことを実証し、抽象化の柔軟性を示しています。
• コミュニティへの採用：この標準は検証コミュニティから肯定的な評価を得ています。主要なソルバーチームは VNN-LIB 2.0 のサポートを約束しており、新しい標準は VNN-COMP 2026 コンペティションでの使用が予定されています。
• ツールサポート：著者らは、新しい標準に準拠したパーサーと型チェッカーを実装した高性能 C++ ライブラリ（Python および Julia バインディング付き）を、Agda 形式化と共にリリースしました。

重要性

本論文は、VNN-LIB 2.0 が信頼できるニューラルネットワーク検証のための堅牢かつ厳密な基盤を提供すると主張しています。その重要性は、以下の 2 つの相補的な領域にあります：

1. 実用的な相互運用性：表現力の拡張（複数のネットワーク、隠れノード）と構文の標準化により、コミュニティは統一的な方法でより豊かな性質を指定・検証できるようになり、ベンチマークやツールの比較が促進されます。
2. 理論的厳密性：形式的意味論と型システムを提供することで、ツールとソルバー間の「厳密な契約」を確立します。これにより、ツール自体（ソルバー、オプティマイザー、証明チェッカー）の形式的検証が可能となり、数値的健全性に関する微妙な問題（例えば、実数値意味論と浮動小数点意味論の区別）が解決されます。

著者らは、この仕事が理論的である一方で具体的な帰結を持つことを強調しています。すなわち、問い合わせの解釈を曖昧さなく保証し、技術的課題を解決する言語を提供し、将来的に形式的に検証された証明証の基礎を築くことです。