22年の疑いを経て、メッセージは「混ぜる」ほうが「運ぶ」より強いとわかった
何人もの送信者が、それぞれ自分の受信者にメッセージを届けたいと考えているケーブルのネットワークを思い浮かべてほしい。古典的なやり方はルーティングだ。各メッセージは小包のように一つ以上の経路に沿って運ばれ、通信量を任意の割合で多くの経路に分けることもできる。ネットワーク符号化(ネットワークコーディング)は、さらにもう一つ自由を加える。途中のノードは、受け取ったメッセージをただ転送するのではなく、たとえば足し算によって組み合わせてよいのだ。
問題は、その自由によって、より多くのデータを通せることがあるのかどうかだ。論文が扱うのは無向ネットワークである。ケーブルはどちらの方向にもデータを運べるが、両方向で一つの容量を共有する。
次々と確かめられた予想
2004年、リー(Li)とリー(Li)は、この設定では符号化は分数ルーティング(通信を経路に分割するルーティング)に対して何の優位ももたらさないと予想した。ハーヴィー(Harvey)、クラインバーグ(Kleinberg)、ラサラ・レーマン(Rasala Lehman)も独立に同じ予想を立てた。その後20年にわたり、この予想はネットワークの種類ごとに次々と確かめられた。セッションが二つの場合、ある種の平面ネットワーク、符号化ノードが6個以下のネットワーク、などだ。だが一般的には決着しなかった。計算量理論の他の結果、たとえば外部メモリでの整数ソートや乗算回路の下界は、この予想を仮定したうえで証明されていたほどだ。
既知の理論はすでに、かかっているものの大きさを限定していた。符号化がルーティングに勝てるとしても、その差はせいぜい対数倍にとどまる。そして2017年のブレイバーマン(Braverman)、ガーグ(Garg)、シュヴァルツマン(Schvartzman)の結果は、符号化が厳密に優位になるネットワークが一つでもあれば、それをはるかに大きな差に増幅できることを示していた。すべては、有限の例を一つ見つけることにかかっていた。
足し算で十分
付録には基本的な仕掛けが示されており、混ぜることがなぜ役に立つのかがわかる。いくつかの送信元をハブvのまわりに、それらの受信者を別のハブwのまわりに置き、vとwを1本のケーブルで結ぶ。各送信元には、他の受信者へ通じる小さなわき道もある。3ラウンドのうちに、真ん中のケーブルはすべてのメッセージの和を運ぶ。各受信者はその和と、わき道から届く他のメッセージを受け取り、引き算によって自分のメッセージを取り出す。真ん中のケーブルがなければ、各送信元から受信者までは5ホップかかる。
ハウプラー(Haeupler)、ワイツ(Wajc)、ズジッチ(Zuzic)の以前の研究によるこの仕掛けは、符号化を速くする。だがそれだけでは、より多く運べるようにはならない。長い経路でも、高いレートのパイプラインを走らせることはできるからだ。
ネットワークに変えられた回路
トロント大学のシンダン・ジャン(Xindan Zhang)とバオチュン・リー(Baochun Li)、清華大学のゾンペン・リー(Zongpeng Li)が、欠けていた一歩を見つけた。彼らは短い符号を可逆な計算に変える。逆にたどれる整数の足し算からなる回路で、計算し、結果をコピーし、そのあと途中の作業を元に戻す。次に、物理的なケーブルがその回路の配線そのものであるような新しいネットワークを構築し、計算のすべてのレジスタ(作業用のレジスタも含む)に、それぞれ専用の送信者・受信者の要求を割り当てる。
あとは、配線に沿った「時間」を注意深く勘定すれば片がつく。すべての配線について合計すると、長さは各要求がカバーしなければならない最短距離とちょうど一致する。ところが、指定された要求は、余分に2単位かかるある種のゲートを避けられない。そのためルーティングは完全なレートに厳密に届かない。一方、符号はどのケーブルもちょうど1回ずつ使い、多数のブロックにわたってパイプライン化すれば、レート1に近づく。
証明されたこと
- 有限の連結ネットワークで、すべてのノードが他の最大3個のノードとつながり、どのケーブルも容量1であるもの。その上で、単純な2元線形符号が、可能な最良の分数ルーティングに勝つ。2004年の予想は誤りである。
- 同じ整数による構成が、すべての有限体とすべての非自明な有限アーベル群で一度に成り立つ。
- コピーを繰り返し組み合わせることで、著者らは、符号化が完全なレートに近づく一方でルーティングが1/log nのべき乗のように落ちていく、無限個のネットワークの族を構築した。つまりポリ対数の優位だ。
論文は反例のノード数を示していない。その構成要素だけでも、13,122ラウンド続く符号である。
機械によるチェック
有限の反例と、族についての定理はどちらも、証明支援系Leanで形式化されている。著者らによれば、2,472個の宣言と1,755個の定理を監査した結果、証明はLeanの三つの標準公理しか使っておらず、未完成の証明もなかった。新しい環境での独立な再チェックも成功したが、使ったLeanのカーネルは同じだった。
未解決のこと
著者らは三つの問いを挙げている。有限の例における優位の本当の大きさ、既知の対数の上限が実際に達成されるかどうか、そして小さな反例が存在するかどうかだ。論文の最後の一文が現状をまとめている。「結局のところ、無向ネットワークでも符号化は役に立つ。どれほど役に立ちうるかは、これから明らかになる。」
AIの使用の申告。 脚注によれば、OpenAIのGPT-6 Astraが証明とLeanのコードの開発を支援した。