より高速な最短経路アルゴリズム

より高速な最短経路アルゴリズム

問題

最短経路問題は非常に単純な問題です。頂点と、それらを結ぶ（有向または無向の）辺からなるグラフがあります。各辺には実数値の重みが付けられています。ある頂点から出発して、グラフ内の他のすべての頂点について、パスの最小合計重みを見つけるか、到達不可能であることを報告します。

私が検討したバージョンでは、グラフは有向であり、厳密な解を必要とし、辺の重みは非負の実数でした。

実数値の重みは比較および加算が可能であると仮定します。最短経路アルゴリズムが内部で行う操作（訪問したノード数のカウントや中間頂点での距離の格納など）はすべて実行時間にカウントされます。

この設定では、古典的なDijkstraの最短経路アルゴリズムは、頂点の数（n≥2）と辺の数（m）で表される O(m+nlog⁡n) の時間で実行されます。これは、フィボナッチヒープのような適切な優先度付きキューデータ構造を使用することで達成されます。m≥n の場合、他の決定性アルゴリズムは、この2025年の画期的な論文で最初に紹介された O(m log^{2/3} n) や、この2026年のフォローアップの O(m log n + mn log n log log n) を達成します。

これらの界を考慮すると、m が n の関数として表されるパラメータ空間には、Dijkstra が優れている広い領域があります。そこで、私はエージェントたちに、重みが非負の実数である場合に何が可能かを調べ、Lean（形式検証ツール）を使用して正当性と効率性を証明するように依頼しました。

解法

約15時間とメッセージボードでの733件のメッセージの後、チームは有向グラフ設定における厳密な最短経路距離を見つけるための提案された新しいアルゴリズムを完成させました。このアルゴリズムは C-HD と呼ばれ、このLean証明で提示されています。

このアルゴリズムは、非生産的な辺に遭遇する局所探索をうまく処理します。依然として優先度比較を使用しますが、新しく遭遇した頂点は、未探索のリーフとして探索のサイズ制限にカウントできます。アルゴリズムは局所的な不変量（各更新後に真であり続ける規則）を維持し、慎重な辺の削除と有界な局所探索を行います。これにより、認定された範囲内でこの界を達成できます。

O ⁣(n+m+m log⁡ ⁣(2+mn+1)+m1/3(nlog⁡(n+2))2/3).

ここで、n≥2 は入力グラフの頂点数、m は辺の数です。認定された範囲は m≤n⌊⌊log⁡2n⌋3/4⌋ です。この分析のために、メモリ割り当て、辺のソート、入力グラフの読み込み、結果の出力のオーバーヘッドも追加します。

C-HD が Dijkstra やリストされた SOTA アルゴリズムよりも関連する領域で優れた界を持つ直感的な説明は、繰り返し行われる検索とデータ構造の作業を削減することです。そのアイデアは次のとおりです。

1. ソースと頂点の現在のフロンティアから開始します。
2. 外向きの辺に沿って有界な局所探索を実行します。
3. 新しく遭遇した頂点を、辺が距離推定値を改善しない場合に未探索のリーフを含めて、探索制限にカウントします。
4. 結果の探索ツリーとピボットを使用して、再帰的な作業を整理します。

この決定性手順は、繰り返しの作業を制限します。アルゴリズム C-HD は局所的な不変量を慎重に処理するため、同じ終点/頂点を数回再訪した場合でも、繰り返しの処理を制限できます。このように、C-HD は、頂点の訪問順序を事前に知らなくても、指定されたレジームでの総作業量で優れた界を達成します。依然として入力グラフ全体を読み込みます。

アルゴリズムはソートされた外向き辺リストに依存することに注意してください。これは、その独自の充電済み前処理の一部として構築されます。小さな入力や認定された密度範囲外の入力を処理するために、エージェントは別のアルゴリズムである Bellman–Ford を、実行開始時に選択される O((n+1)(m+1)) の実行時間界とともに追加しました。Bellman–Ford は Dijkstra のバリアントではありません。

以下に、証明された定理の抜粋と、達成された実際の実行時間目標を示します。

-- From namespace Frontier.CHD.Final:
theorem chd_CHDTarget : GateCTarget.CHDTarget GateCCalc.F :=
  ⟨chdProgram, chd_exact_within.1,
    bodyC KcC + 65536 * 9 + 100, chd_exact_within.2⟩

theorem chd_gateC : Frontier.GateC :=
  GateCTarget.chdTarget_F_imp_gateC chd_CHDTarget

C_HD_bound, within the certified range:
O(n + m + m * log(2 + m/(n+1)) + m^(1/3) * (n*log(n+2))^(2/3))

先行研究と比較するために、おおよそ m=n log^{3/4} n の辺を持つグラフを見てみましょう。Dijkstra の実行時間界は O(n log n) です。C-HD アルゴリズムは O(n log^{11/12} n) を達成します。これはわずかな改善に見えるかもしれませんが、これらのグラフが大きくなるにつれて、より優れた漸近的上限を達成したことを意味します。

例えば、n=2^{1000} の場合、主要な式 n log_2 n と n (log_2 n)^{11/12} の比率は、定数と低次の項を無視すると、1000^{1/12} ≈ 1.78 です。これは測定された速度向上ではありません。この改善は、入力サイズに対して対数的にスケールします。n を2乗すると、その比率は 2^{1/12} 倍になります。

実際のパフォーマンス

もちろん、これはまだ計算量の上限に過ぎず、数学的な約束です。アルゴリズムが理論的にはこのレジームで優れているとしても、実際に実行するとパフォーマンスが悪化する可能性があります。今回の実行では、小規模な正当性シミュレーションを実行しましたが、大規模な実グラフでの実装ベンチマークは行っていません。私の分析に基づくと、このアプローチは証明されたレジームにおいて、リストされた先行する界よりも優れた漸近的界を持っています。形式的な構成における定数は膨大であるため、これは実用的な速度向上を確立するものではありません。

形式検証

認定された範囲内でのアルゴリズムのパフォーマンスに対する界も正常に検証しました。

O(n + m + m * log(2 + m/(n+1)) + m^(1/3) * (n*log(n+2))^(2/3))

これは、m≈n log^{3/4} n のプロファイルに沿って O(n log^{11/12} n) に単純化されます。

Lean Comparator ツールを使用して証明を確認しました。Lean 証明は実行時間界と、n log n にわたる厳密な漸近的改善を確立します。このプロファイルを公開された界に代入すると、界が m log^{2/3} n および m log n + mn log n log log n と m√log n + √mn log n log log n よりも小さいことも示されます。

Comparator は、提出された証明が指定された定理を証明し、許可された公理のみを使用し、Lean カーネルによって受け入れられることを確認します。これにより、形式的なパフォーマンス保証が指定されたターゲットと一致することが保証されます。

C-HD はどれくらいの改善をもたらすか？

「しかし、実際にどれくらいの時間を節約できるのだろうか？」と考えているなら、証明が確立していることは次のとおりです。

m≈n log^{3/4} n のプロファイルに沿って、主要な界の式の比率は (log n)^{1/12} です。証明は、1兆頂点のグラフの測定された実行時間や正確な反復回数を示していません。m=10n の場合、グラフは異なる密度レジームにあり、この結果はそこでの最良の既知の界に対する改善を確立しません。

抽出

OpenAI の Hugging Face インシデントと Navier–Stokes の結果から学んだことがあるとすれば、それはエージェントが問題に対する進歩の時間を劇的に圧縮できるということです。そして、エージェントが協力するように促す簡単な方法の1つは、互いに話す方法、つまりメッセージボードを与えることです。

私がここでやったことは、10体の Claude Opus 5.5 エージェントを最大努力で起動し、シンプルなメッセージボードを与えたことです。彼らには初期の役割がありましたが、作業を再編成し、発見を共有し、互いのアイデアに異議を唱え、最も有望に見えるアプローチに労力をシフトすることができました。

私は彼らに、非負実数値を持つ有向グラフの厳密な最短経路に対する実質的な理論的改善と、完全なLean証明に裏打ちされたものを求めていることを正確に説明する、やや長いプロンプトを与えました。彼らはいくつかの方向を追求できました。対数因子を削除する、より良い指数を見つける、線形時間アルゴリズムを見つける、またはアルゴリズムが達成できることの基本的な下限を証明するなどです。

最後に、最近の論文と比較し、他のエージェントが繰り返さないように失敗したアプローチを記録し、互いの主張に異議を唱えるように依頼しました。成功を宣言する前に、再現可能なLeanビルドと2つの別々のピアレビューが必要でした。改善を証明できなかった場合は、部分的な進捗を維持し、未解決のまま残ったことを言うように指示しました。

エージェントのチームが何ができるかは魅力的です。データセンターにいる天才たちの国；その予測はそれほど的外れではありませんでした。

---

完全な証明パッケージ（Leanソース、非公式論文、検証記録）は github.com/spicylemonade/c-hd-proof で入手できます。