A Machine-Checked Cost Analysis of the BMSSP Recurrence in Isabelle/HOL With a Non-Vacuous Size-Parametric Runtime Witness

技術要約：BMSSP 再帰に関する機械検証されたコスト解析

問題提起
本論文は、有向単一始点最短経路（SSSP）における長年の課題であった $O(m + n \log n)$ の「ソート・バリア」を打破する、Duan, Mao, Mao, Shu, および Yin による 2025 年の決定論的アルゴリズムの中核エンジンである、**有界マルチソース最短経路（BMSSP）**再帰の形式的検証を取り扱う。元のアルゴリズムは $O(m \log^{2/3} n)$ の実行時間を達成しているが、その正当性と、特にその償却コスト解析を証明助手（proof assistant）で形式化することには、大きな困難が伴う。これらには、ソースの集合と有界な距離範囲を伴う再帰的な正当性の議論の複雑さ、カスタム分割データ構造にわたる償却会計の繊細さ、そして「空虚な（vacuous）」漸近定理（入力ファミリーが限定されているか、あるいは必要な実行が存在しないために、技術的には真であるが意味をなさない定理）のリスクが含まれる。

手法
著者らは、モジュール性を確保し、関心の分離を厳密に行うために、6 つの明確に階層化された理論として構成された、Isabelle/HOL（Isabelle2025-2）による完全な形式化を提示する。この開発は HOL と HOL-Library のみをインポートしており、外部のアキシオム、sorry、または oops 文は一切含まれていない。

1. 意味論的基礎: 著者らは、有限の重み付き有向グラフ、単純なウォーク、および距離計数を定義する。すべての後続の議論の基礎となる、一意の最短ウォークと厳密なタイブレークに関する構造的補題を確立する。
2. 再帰的正当性: BMSSP 再帰の抽象モデルを、FindPivots ルーチン、ベースケース、および分割ループを含めて形式化する。機械検証された証明により、抽象アルゴリズムが任意の適切に構成されたグラフに対して最短距離を正しく計算することを確立する。
3. 実行可能アーティファクト: 抽象モデルは、自然数の頂点と重みを用いた実行可能な関数（bmssp_distances）へと洗練される。著者らは bmssp_correct_strong を証明し、実行可能な出力が最短距離の意味論的定義と一致することを、特定の 5 頂点の例を用いた評価を通じて確認する。
4. コストモデル: 抽象的な分割インターフェース（Insert, BatchPrepend, Pull）がコスト述語と共に定義される。著者らは、この抽象再帰に対して $O(m \log^{2/3} n)$ の償却コスト包絡線（envelope）を証明する。極めて重要なことに、彼らは論文の対数スケジュールの忠実な実現体となるバケット化された分割データ構造を実装し、高速化に必要な決定的な $O(\log(N/M))$ 挿入スケールを証明する。
5. 運用的洗練: 2 つの運用的レイヤーが定義される：
   • Exact-Concrete (正確・具体的): 再帰的な子の出力を、増分範囲スライスに厳密に結合させる。
   • Charged (チャージ型): 出力をデカップル（分離）し、増分スライスのみを課金する。
     著者らは、exact-concrete 関係が意図された入力（具体的にはパス・ファミリー）に対して**非全域的（non-total）**であることを機械検証し、完全な実行が存在できないという障害を強制的に導き出す。
6. サイズ・パラメトリック・レイヤー: 著者らは、単位重みの有向パスの非限定的なファミリー（$P_n$）を構築する。彼らは、charged 関係が全域的であり、完全な実行が存在することを証明する。計算量を変えることなく全域性を確保するために、彼らは「膨張させた」スケジュール・インデックス（$N = n \cdot n$）を採用し、これによりバケット容量がパスをカバーしつつ、$O(\log^{2/3} n)$ の因子を維持することを保証する。

主要な貢献

• 初の機械化された形式化: これは、BMSSP 再帰とその実行時間解析の初の機械検証された形式化である。
• 非空虚なサイズ・パラメトリックな証跡: 本論文は、単位重みの有向パスにおいて、charged 実行時間が $O(|V| \cdot (\ln |V|)^{2/3})$ であることを示す、完全に無条件な定理を提供している。この結果は、著者らが「非空虚性レジャー（non-vacuity ledger）」を通じて、ファミリーが境界なく成長し、完全な実行が存在し、かつ動作領域が実現されていることを明示的に証明しているため、非空虚である。
• 結合による障害の形式的診断: 著者らは、素朴で密結合したコスト関係（exact-concrete モデル）における欠陥を特定し、形式的に証明する。彼らは、この関係がパス・ファミリーに対して最大 1 ステップしか取らせないことを示し、それに基づくサイズ・パラメトリックな境界がいかに空虚になるかを実証する。この障害は機械検証された補題として記録されており、メインの結果は、この障害を回避するためにデカップルされた charged 関係を用いて導出される。
• 実行可能検証: 開発には、ビルドプロセス内のコード評価によって検証された、実行可能な最短距離関数と、その正当性証明が含まれている。

結果
メインの定理 path_nonvac_runtime_bigo_card_V_unconditional は以下を示す：
$$(\lambda n. \text{real}(\text{path\_nonvac\_time } n)) \in O(\lambda n. \text{real}(\text{card}(\text{path\_k\_V } n)) \cdot (\ln(\text{real}(\text{card}(\text{path\_k\_V } n)) + 2))^{2/3})$$
この境界は以下の特性を持つ：

• 無条件（Unconditional）: 実行の存在やグラフの特性に関する仮定を、パス・ファミリーの定義以外に持たない。
• サイズ・パラメトリック（Size-Parametric）: 漸近変数は固定されたパラメータではなく、真のグラフサイズ（$|V|$）である。
• 非空虚（Non-Vacuous）: 存在が証明されている「最小コスト」の実行のコストを制限している。

また、本論文は、具体的なバケット構造によって実現される抽象コストモデルに対する $O(m \log^{2/3} n)$ の境界を確立し、$O(\log(N/M))$ の挿入スケールを確認している。

意義と範囲
著者らは、本研究の意義を、Duan–Mao–Mao–Shu–Yin の SSSP 実装の完全なエンドツーエンドの検証ではなく、BMSSP 再帰の正当性とチャージ型実行時間解析の厳密な形式化として明示的に位置づけている。

• 主張されていること: 本論文は、再帰ロジックの正当性と、チャージ型操作コスト解析（特定の非限定的ファミリーに対する非空虚な漸近境界を含む）の妥当性を検証したと主張している。
• 主張されていないこと: 著者らは、エクスポートされた SML コードの機械ステップ複雑性を検証したとは主張しておらず、また、すべてのグラフまたはすべての実行に対する普遍的な境界を主張してもいない。彼らは、サイズ・パラメトリックなメインの境界が、特定のファミリーに対する「最小コスト」の実行を制限するものであることを明示している（普遍的な境界はこのファミリーに対しては偽となるため）。
• 方法論的貢献: 本論文は、機械化された複雑性における「非空虚性」が、第一級の証明義務として重要であることを強調している。漸近定理は、入力ファミリーが限定されているか、あるいは実行が存在しない場合、論理的には妥当であっても空虚になり得ることを示している。「非空虚性レジャー」（成長、実行の存在、および領域の実現の証明）は、将来の再帰的複雑性の議論の形式化のための再利用可能なテンプレートとして提示されている。

要約すると、本研究は、BMSSP 再帰の高信頼な機械検証された基礎を提供し、機能的正当性とコスト解析を厳密に分離し、結果としての漸近境界が意味のあるものとなるよう、形式化における落とし穴を注意深く診断し、回避している。