Lean-verified lower bounds for the Shannon capacity of odd cycles

あなたは、騒々しく混沌とした街を横切って秘密のメッセージを送ろうとしていると想像してください。街にはあらゆる誘惑が溢れており、時にはあなたの信号が間違った通りの名前と混ざり合ってしまうこともあります。情報理論の世界において、これは現実的な問題です。つまり、エラーなしで完璧にデータを送るにはどうすればよいのか、という問題です。1950年代、数学者のクロード・シャノンは、「ノイズのある」通信路であっても、文字をどのようにグループ化するかさえ工夫すれば、完璧なメッセージを送ることができるということを解き明かしました。彼は「シャノンの容量（Shannon capacity）」と呼ばれる概念を導入しました。これは、特定の種類のノイズのあるネットワークを通じて、完璧なメッセージを送信できる最大速度を示すスコアのようなものです。

これを視覚化するために、街の地図上で行われるゲームを想像してみてください。その地図はグラフであり、交差点は点、通りは線で表されます。いくつかの通りは一緒に移動しても「安全」ですが、他の通りは危険であり、もしそれらを混ぜてしまうと衝突を引き起こします。目標は、危険な通りの間で決して衝突することのない、最大の交差点のグループ（「独立集合」）を選ぶことです。「シャノンの容量」とは、非常にトリッキーな問いを投げかけます。もしこのゲームを一度きりではなく、地図のコピーを何層にも積み重ねて、巨大で多次元的な街を作ってプレイしたとしたら、あなたの安全なグループはどれほど大きくなるでしょうか？ある形状については答えが分かっています。しかし、特に奇数形のループ（五角形や七角形のようなもの）については、その答えは何十年もの間、謎のままでした。それは、直線道路の制限速度は知っているのに、曲がりくねった七角形のトラックでどれくらいの速さで行けるのか全く分からないようなものです。

この論文は、これらの一部のトリッキーな七角形（およびそれ以上の大きさ）のトラックに関するその謎を解明することを目的としています。著者たちのチーム（数学者とコンピュータ科学者のグループ）は、これらの特定のループに対して、より少し高速に完璧なメッセージを送信する新しい方法を見つけ出しました。彼らは単に推測したわけではありません。彼らは、より大きく、より安全な交差点のグループを構築するための、巧妙でステップバイステップのレシピを使用しました。複雑な数学の中で一つも間違いを犯さないようにするために、彼らは「Lean」という非常に厳格なデジタル審判を用いて、すべてのステップをチェックしました。その結果、彼らはこれらの特定の奇数ループにおいて、完璧な通信の最大速度が以前に計算されていたよりも高いことを証明したのです。

安全な交差点のゲーム

著者たちが実際に何を行ったのかを詳しく説明しましょう。彼らは、単純なリング状のグラフ（奇数個の点を持つリング）を調べていました。例えば、7つの点を持つリング、11つの点、13つの点、といった具合です。長い間、数学者たちは5つの点を持つリングの「速度制限」（シャノン容量）については知っていました。しかし、7つ以上の点を持つリングについては、答えが霧の中に停滞していました。私たちはそれが「少なくとも」ある数値であることは知っていましたが、それがもっと高くなる可能性があるかどうかは分かっていませんでした。

著者たちは、安全なグループを成長させるための魔法のレシピのような手法を用いました。一つの地図上にある小さな安全な友人のクラブ（点の集合）を想像してください。論文では「積定理（product theorem）」について述べています。これは、二つの地図を叩き合わせ、新しい、より大きな地図を作り出す機械のようなものです。もし最初の地図に安全なクラブがあり、二番目の地図にも安全なクラブがあるなら、それらを組み合わせて新しい、より大きな地図上の安全なクラブを作ることができます。通常、この新しいクラブのサイズは、最初のクラブのサイズに二番目のサイズを掛けたものになります。しかし、著者たちは特別な「ガジェット」あるいはトリックを見つけました。特定の接続パターン（「有効なタプル」と呼ばれます）を使用することで、単純な掛け算が示唆するものよりも、新しいクラブを大きくすることができるのです。

このように考えてみてください。もし、喧嘩せずに協力できる2人のチームがあり、その二つのチームを組み合わせた場合、通常は4人のチームになると予想されます。しかし、この特別なトリックを使えば、著者たちはそれらを組み合わせることで、全員が完璧に仲良くできる5人のチームを作る方法を見つけたのです。このトリックを何度も繰り返し、地図を高く積み重ねていくことで、彼らはこれらの安全なチームを巨大なグループへと成長させることができました。

新記録

チームはこのレシピを、7、11、13、15、19、21、23個の点を持つ7つの異なる奇数リングに適用しました。それぞれのリングに対して、彼らは既知の安全なグループからスタートし、彼らの「積み重ね」マシンを何度も走らせました。その結果、シャノン容量の新たな下限値が得られました。

以下が、彼らが計算した正確な数値です。

• 7つの点を持つリングの場合、容量は少なくとも 3.258805369885 であることを証明しました。これは以前の最良の予測よりもわずかに高い数値です。
• 11つの点を持つリングの場合、新しい下限は 5.294502522149 です。
• 13つの点を持つリングの場合、限界を 6.302455083464 まで押し上げました。
• 15つの点を持つリングの場合、数値は 7.301600534487 です。
• 19つの点を持つリングの場合、9.357192705918 に到達しました。
• 21つの点を持つリングの場合、下限は 10.342455853338 です。
• そして、23つの点を持つリングについては、少なくとも 11.328224257774 の容量を見出しました。

これらの数字は、一見ランダムな数字の羅列に見えるかもしれませんが、情報理論の世界においては、具体的な改善を意味しています。これらは、これらの特定のネットワークにおいて、私たちがこれまで可能だと考えていたよりも、確実に少し速くメッセージを送信できることを意味しています。

デジタル審判

この論文を特別なものにしているのは、単にその数値ではありません。むしろ、どのようにしてその数値を得たかです。そこに含まれる数学は極めて複雑であり、膨大なデータセットと数千のステップを伴います。それは、人間が容易に小さなミスを見逃してしまうような種類の仕事です。これを解決するために、著者たちは証明全体を Lean と呼ばれるコンピュータ言語で記述しました。

Leanを、単に「正しいと思う」とか「良さそうだ」といった言葉を受け入れない、超厳格なデジタル審判だと考えてください。Leanは、すべてのステップに対して絶対的な論理的証明を要求します。もし著者たちが論理において間違いを犯していれば、Leanは止まって、「それは従っていない」と告げるのです。この論文が「Leanによって検証済み（Lean-verified）」であるということは、コンピュータが彼らの推論の全行をチェックし、彼らの新しい下限値が数学的に堅実であることを確認したことを意味します。彼らは単に結果をシミュレーションしたのではなく、それらを形式的に証明したのです。

また、著者たちは、これらの安全なグループの初期のパターンやレシピを見つけるために、大規模言語モデル（高度なAIチャットボットのようなもの）を使用したことにも言及しています。これは、独創的なアイデアを提案してくれるクリエイティブな助手がいて、その後、数学者がそのアイデアが実際に通用するかどうかを厳格なツールでテストするようなものです。このケースでは、AIが経路を提案し、人間、数学者、そしてAIのチームが、検証済みのゴールラインまでその道を歩み抜いたのです。

なぜ重要なのか

「それで、何になるのか？ 単に数値が少し高くなっただけではないか」と思うかもしれません。その答えは、問題の性質にあります。数十年にわたり、これらの奇数リングの容量は未解決の問題でした。私たちは答えが「少なくとも」ある下限と「せいぜい」ある上限（Lovász bound）の間のどこかにあることは知っていましたが、それを特定することができませんでした。下限をわずかでも押し上げるたびに、私たちはその隙間を狭めているのです。私たちは真の答えに近づいています。

この研究は、たとえ長い間停滞していた問題であっても、適切なツールを持ち、最も厳格な基準で自分の仕事をチェックする忍耐強さがあれば、依然として改善の余地があることを示しています。著者たちはすべての奇数リングに対するシャノン容量の謎をすべて解いたわけではありませんが、7、11、13、15、19、21、23のリングについては、以前よりも少し速く通信できることを証明することで、霧の深い角をいくつか晴らしたのです。