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

問題 最短経路は非常に単純な問題です。頂点とそれらを接続する（おそらく有向の）辺からなるグラフがあります。各辺には実数値の重みがあります。ある頂点から開始して、グラフ内の他のすべての頂点について、パスの最小合計重量を見つけるか、到達不可能であることを報告したいとします。私が考慮したバージョンでは、グラフは有向であり、正確な答えが必要で、辺には非負の実数値の重みが与えられました。実数値の重みは比較および加算できると仮定します。最短経路アルゴリズムが内部で行う操作（訪問したノードの数を数える、中間頂点の距離を保存するなど）はすべて実行時間に含まれます。この設定では、古典的なDijkstraの最短経路アルゴリズムは、O(m+nlog⁡n)時間で実行されます。ここで、n≥2は入力グラフの頂点の数、mは辺の数です。これは、適切な優先度付きキューデータ構造（フィボナッチヒープなど）を使用して達成されます。m≥nの場合、他の決定論的アルゴリズムは、O(mlog²⁄³n)（2025年の画期的な論文で最初に紹介された）およびO(m√logn+√mnlog n log log n)（2026年のフォローアップ）を達成します。これらの境界を考慮すると、Dijkstraがより優れているパラメータ空間の広い領域があります。そこで、重みが非負の実数値であった場合に何が可能かをエージェントに調査させ、Lean（形式検証ツール）を使用して正当性と効率を証明するように依頼しました。 ソリューション メッセージボード上で約15時間と733件のメッセージの後、チームは有向グラフ設定で正確な最短経路距離を見つけるための新しいアルゴリズムの提案を完了しました。このアルゴリズムはC-HDと呼ばれ、このLean証明で提示されています。このアルゴリズムは、非生産的な辺に遭遇する局所探索をうまく処理します。依然として優先度比較を使用しますが、新しく遭遇した頂点は、未探索のリーフとして検索のサイズ制限にカウントできます。アルゴリズムは局所的な不変量（各更新後に真となるルール）を維持し、注意深い辺の削除と有界な局所探索を行います。これにより、認定された範囲内でこの境界を達成できます：O(n+m+mlog(2+m/(n+1))+m¹/³(nlog(n+2))²/³)。ここで、n≥2は入力グラフの頂点の数、mは辺の数です。認定範囲はm≤n⌊⌊log₂n⌋³/⁴⌋です。この分析のために、メモリの割り当て、辺のソート、入力グラフの読み取り、結果の出力のオーバーヘッドも追加します。C-HDがDijkstraやリストされたSOTAアルゴリズムよりも関連する領域で優れた境界を達成する直感的な説明は、繰り返し検索とデータ構造の作業を削減することです。アイデアは次のとおりです。ソースと頂点の現在のフロンティアから開始します。外向きの辺に沿って有界な局所探索を実行します。新しく遭遇した頂点を検索制限にカウントします。これには、辺が距離推定値を改善しない場合に未探索のリーフが含まれます。結果の検索ツリーとピボットを使用して、再帰的な作業を整理します。この決定論的な手順は、繰り返し作業を制限します。アルゴリズムC-HDは局所的な不変量を慎重に処理するため、同じ終点/頂点を数回再訪しても、繰り返し処理を制限できます。このように、C-HDは、頂点の訪問順序を事前に知らなくても、述べられた領域での総作業量でより優れた境界を達成します。依然として入力グラフ全体を読み取ります。アルゴリズムはソートされた外向き辺リストに依存することに注意してください。これは、それ自体の課金済み前処理の一部として構築されます。小さな入力や認定された密度範囲外の入力を処理するために、エージェントは別のアルゴリズムであるBellman-Fordを追加しました。実行時間境界はO((n+1)(m+1))で、実行の開始時に選択されます。Bellman-FordはDijkstraのバリアントではありません。以下に、証明された定理の抜粋と、実際に達成された実行時間ターゲットを示します。 -- 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, 認定された範囲内：O(n + m + m * log(2 + m/(n+1)) + m^(1/3) * (n*log(n+2))^(2/3)) 以前の研究と比較するために、おおよそm=nlog³⁄⁴nの辺を持つグラフを見てみましょう。Dijkstraの実行時間境界はO(nlog⁡n)であり、C-HDアルゴリズムはO(nlog¹¹/¹²n)を達成します。これはわずかな改善に見えますが、これらのグラフが大きくなるにつれて、より優れた漸近的上限を達成したことを意味します。たとえば、n=2¹⁰⁰⁰の場合、主要な式n(log₂n)とn(log₂n)¹¹/¹²の比率は、定数と低次の項を無視すると、1000¹/¹²≈1.78です。これは測定された速度向上ではありません。この改善は、入力サイズに対して対数多項式的にスケールします。nを2乗すると、その比率は2¹/¹²倍になります。 実際のパフォーマンス もちろん、これはまだ複雑さの上限であり、数学的な約束にすぎません。理論的にはアルゴリズムがこの領域で優れていても、実際に実行するとパフォーマンスが悪化する可能性があります。今回の実行では、小さな正当性シミュレーションを実行しましたが、大規模な実グラフでの実装のベンチマークは行いませんでした。私の分析に基づくと、このアプローチは証明された領域でリストされた以前の境界よりも優れた漸近的境界を持っています。形式的な構成の定数は膨大であるため、これは実用的な速度向上を確立するものではありません。 形式検証 また、認定された範囲内でのアルゴリズムのパフォーマンスの境界を正常に検証しました：O(n + m + m * log(2 + m/(n+1)) + m^(1/3) * (n*log(n+2))^(2/3))。これは、プロファイルm≈nlog³⁄⁴nに沿ってO(nlog¹¹/¹²n)に単純化されます。Lean Comparatorツールを使用して証明を確認しました。Lean証明は実行時間境界と、nlog⁡nに対する厳密な漸近的改善を、述べられた密度プロファイルに沿って確立します。そのプロファイルを公開された境界に代入すると、境界がmlog²⁄³nおよびm√logn+√mnlog n log log nよりも小さいことも示されます。Comparatorは、提出された証明が指定された定理を証明し、許可された公理のみを使用し、Leanのカーネルによって受け入れられることを確認します。これにより、形式的なパフォーマンス保証が述べられたターゲットと一致することが保証されます。 C-HDはどのくらいの改善を提供しますか？ 「しかし、実際にどれくらいの時間が節約されるのだろうか？」と考えているなら、証明が確立しているのは次のとおりです。プロファイルm≈nlog³⁄⁴nに沿って、主要な境界式の比率は(log⁡n)¹/¹²です。証明は、1兆個の頂点を持つグラフの測定された実行時間や正確な反復回数を提供しません。m=10nの場合、グラフは異なる密度領域にあり、この結果はそこでの最良既知の境界に対する改善を確立しません。 引き出し OpenAIのHugging FaceインシデントとそのNavier–Stokesの結果から私が学んだことがあれば、それはエージェントが問題の進歩を劇的に圧縮できるということです。そして、エージェントが協力するように促す簡単な方法は、互いに話す方法、つまりメッセージボードを与えることです。ここで私がしたことは、最大努力で10個のClaude Opus 5.5エージェントを起動し、簡単なメッセージボードを与えることでした。彼らは初期の役割を持っていましたが、仕事の再編成、発見の共有、互いのアイデアへの挑戦、そして最も有望に見えるアプローチへの労力のシフトを行うことができました。私は彼らに、正確に何をしてほしいかを説明する、やや長いプロンプトを与えました。