TensorRocq: Rocq における図式的推論の実現に関する技術的概要

本論文は、対称モノイダル圏（SMC）の推論において、紙上の証明と形式検証の間のギャップを埋めるためのツール「TensorRocq」を提案しています。これは、Rocq（Coq の次世代プロトコル）上で動作するライブラリであり、ストリングダイアグラムの図式的推論を、結合律（associativity）の扱いを自動化しつつ、テンソル意味論に基づいて検証可能な形で可能にします。

以下に、問題定義、手法、主要な貢献、結果、および意義について詳細にまとめます。

1. 問題定義

対称モノイダル圏（SMC）は、回路論理や量子計算（ZX-calculus）など、多くの計算モデルを記述するための共通枠組みです。紙上の証明では、ストリングダイアグラムを用いて「接続性のみが重要（only connectivity matters）」という直感的な操作（図の歪曲や部分図の置換）によって推論が行われます。

しかし、従来の証明支援系（Rocq/Coq）において SMC を形式化する際、以下の課題が存在しました：

• 結合律の冗長性: 証明支援系では、結合律や自然性条件を明示的に適用して項を構造的に等しくする必要があるため、証明は「接続性」の本質的な情報ではなく、結合順序の調整（構造的な書き換え）に支配されがちです。
• 可読性と堅牢性の欠如: 証明は長くなり、定義やステートメントのわずかな変更（結合順序など）に対して脆弱になります。
• 既存ツールの限界: 既存のツール（Chyp など）は外部ツールとして機能し、検証済みではないか、あるいは具体的な意味論（テンソルなど）に基づく理論への適用が困難でした。

2. 手法と理論的基盤

TensorRocq は、ハイパーグラフ、PROPs、テンソルの 3 つの概念を統合し、それらを共通の「テンソル意味論」で結びつけることで、図式的推論を自動化・検証可能にします。

2.1 理論的基盤

• テンソル: 計算の直列合成（縮約）と並列合成（積）を代数的に表現します。テンソルは「接続性」を単純な代数恒等式として表現するため、SMC の複雑な構造を単純化します。
• ラベル付きハイパーグラフ: 項を構造的に表現します。エッジは演算子、頂点は接続点を表し、インターフェース（入力・出力）を備えています。
• APROPs (Autonomous PROPs): 対称モノイダル圏の構文インターフェースとして機能します。キャップ（cap）とカップ（cup）演算子を備えており、任意の SMC 項をハイパーグラフに変換する際の中間表現となります。

2.2 実装アプローチ

• 反射（Reflection）による検証: 証明支援系内で計算可能なアルゴリズム（反射）を用いて、項をハイパーグラフに変換し、同型性をチェックします。
• 意味論的検証: ハイパーグラフ同型性は、対応するテンソル意味論における等価性を保証します。これにより、構造的な書き換え（図の歪曲）が意味的に正しいことが保証されます。
• 二重プッシュアウト（Double Pushout）書き換え: ハイパーグラフレベルで部分図を検出し、等価な図に置換するアルゴリズムを実装しています。
• 型クラスによる拡張性: 既存のプロジェクト（例：VyZX）に対して、テンソル意味論と APROP 間の「引用（quoting）」と「意味付け（denoting）」を型クラスで実装することで、既存の定義を変更せずに TensorRocq の tactic を適用できるようにしています。

3. 主要な貢献

1. 検証済み図式書き換えエンジン: SMC 項における結合律を自動的に無視し、接続性に基づいた図式的書き換えを可能にする、Rocq 統合型の tactic を提供します。
2. ハイパーグラフとテンソルの統合フレームワーク: 構文（ハイパーグラフ/PROPs）と意味論（テンソル）を結びつける検証済み変換を提供し、書き換えの正当性をテンソル意味論に基づいて保証します。
3. 既存プロジェクトへの統合: VyZX（ZX-calculus の形式実装）への適用を通じて、既存の SMC 理論に対して、定義を変更することなく図式的推論を可能にする型クラスベースのインフラを実証しました。
4. 抽象的理論の定義: Chyp と同様に、生成子と関係式から新しい SMC 理論（例：Frobenius 代数）を定義し、その上で書き換えを行うための「Signature」構造を提供します。

4. 結果と評価

• 証明の短縮と可読性向上: VyZX における CNOT ゲートと SWAP 演算の等価性証明において、従来の手動結合律調整を必要とした 45 行の証明を、TensorRocq を用いることで 17 行に短縮しました。証明は図式的な変換に焦点を当て、構造的なノイズを排除しています。
• 堅牢性: 項の結合順序などの構造的な変化に対して、図式的な等価性のみを考慮するため、証明がより堅牢になりました。
• 性能: 同型性チェックは計算コストがかかる可能性がありますが、実証実験（数十エッジ程度のグラフ）では 1 秒未満で完了し、実用的なスケーラビリティを示しました。
• Frobenius 代数の導出: 生成子と関係式のみから定義した Frobenius 代数において、Frobenius 条件の異なる形式を自動的に導出・検証できることを示しました。

5. 意義と将来展望

TensorRocq は、対称モノイダル圏における「紙上の証明」と「形式検証」の間の長年のギャップを解消しました。

• 意味論的保証: 図式的な直感を、テンソル意味論に基づいた厳密な検証と結びつけることで、安全な自動化を実現しています。
• 応用範囲の拡大: 量子計算（ZX-calculus）だけでなく、線形代数ライブラリや他の量子計算フレームワーク（Qbricks, SQIR など）への適用が期待されます。
• 将来の課題: 現在の制約として、キャップ/カップを含む書き換えや、パラメータ付き生成子（ZX スパイダーの位相など）の完全なマッチング、および視覚化ツールの統合が挙げられています。これらは今後の拡張対象として位置づけられています。

総じて、TensorRocq は、複雑な代数的構造を持つ計算モデルの形式検証において、直感的かつ効率的な推論を可能にする重要なツールとして確立されました。