コンピューターの艦隊が90年来の数学の問題を解決

2020年8月23日午前8時

研究者たちは、オット＝ハインリヒ・ケラーの予想をコンピューターに適した検索に翻訳することで、7次元空間についての予想を確認した。

数学者チームがついにケラー予想を解明した。しかし、彼らは自ら解いたわけではなく、コンピューター群に計算を学習させたのだ。

ケラー予想は、90年前にオット＝ハインリヒ・ケラーによって提唱されたもので、同一のタイルで空間を覆う問題です。これは、2次元空間を2次元の正方形タイルで覆う場合、少なくとも2つのタイルが辺を共有しなければならないというものです。この予想は、あらゆる次元の空間に対して同じ予測をします。例えば、12次元空間を12次元の「正方形」タイルで覆う場合、少なくとも2つのタイルが互いにぴったりと接することになります。

数学者たちは長年にわたりこの予想を少しずつ解明し、ある次元では正しいが、他の次元では誤りであることを証明してきました。昨年の秋現在、この問題は7次元空間においてのみ未解決のままです。

しかし、コンピューターによる新たな証明がついにこの問題を解決しました。昨年10月にオンラインに投稿されたこの証明は、人間の創意工夫とコンピューターの純粋なパワーを組み合わせることで、数学における最も難解な問題のいくつかを解くことができることを示す最新の例です。

新たな研究の著者であるスタンフォード大学のジョシュア・ブレーキンシーク氏、カーネギーメロン大学のマライン・ホイレ氏とジョン・マッキー氏、そしてロチェスター工科大学のデイビッド・ナルバエス氏は、40台のコンピューターを用いてこの問題を解いた。わずか30分後、コンピューターは一言で答えを出した。「はい、この予想は7次元において正しいのです。そして、私たちは彼らの結論を鵜呑みにする必要はないのです。」

答えには、それが正しい理由を説明する長い証明が添えられています。議論はあまりにも広範で人間には理解できませんが、別のコンピュータプログラムによって正しいことが検証できます。

言い換えれば、コンピュータがケラーの予想を解くために何を行ったかは分からなくても、コンピュータが正しく解いたことは確信できるのです。

神秘的な第七次元

ケラーの予想が二次元空間で成り立つことは容易に理解できます。一枚の紙を用意し、同じ大きさの正方形で、正方形の間に隙間がなく、重なり合わないように敷き詰めてみましょう。すぐに、少なくとも2つの正方形が辺を共有する必要があることに気づくでしょう。もし、周囲にブロックが転がっているなら、この予想が三次元空間でも成り立つことは同様に容易に理解できます。1930年、ケラーはこの関係があらゆる次元の対応する空間とタイルに当てはまると予想しました。

初期の結果はケラーの予測を裏付けました。1940年、オスカー・ペロンは1次元から6次元までの空間においてこの予想が成り立つことを証明しました。しかし50年以上経った後、新世代の数学者たちがこの予想に対する最初の反例を発見しました。ジェフリー・ラガリアスとピーター・ショアは1992年、10次元においてこの予想が偽であることを証明したのです。

単純な議論から、ケラー予想が1次元で偽であれば、必然的に高次元すべてで偽であることが示されます。したがって、ラガリアスとショアの発見以降、未解決の次元は7次元、8次元、9次元のみでした。2002年、マッキーはケラー予想が8次元（ひいては9次元でも）で偽であることを証明しました。

すると、7 次元だけが空いていました。つまり、推測が成り立つ最高次元か、推測が成り立たない最低次元かのどちらかでした。

「そこで何が起こっているのか、正確には誰も知らない」とヒューレ氏は語った。

点をつなぐ

数学者たちが数十年にわたってこの問題に取り組み続けるにつれ、その手法は変化していった。ペロンは最初の6次元を鉛筆と紙で解き明かしたが、1990年代までに研究者たちはケラーの予想を全く異なる形、つまりコンピューターを用いてこの問題を解く方法を確立した。

ケラー予想の元々の定式化は、滑らかで連続した空間に関するものでした。その空間には、無限の数のタイルを配置する方法が無限に存在します。しかし、コンピューターは無限の選択肢を含む問題を解くのが得意ではありません。その魔法を働かせるには、何らかの離散的で有限な対象について考える必要があるからです。

1990年、ケレスティーリ・コラディとシャーンドル・サボーはまさにそのような離散的対象を考案しました。彼らは、この対象についてケラー予想と等価な問いを立てることができることを証明しました。つまり、これらの対象について何かを証明すれば、必然的にケラー予想も証明できるということです。これにより、無限に関する問いは、少数の数の算術というより簡単な問題へと実質的に帰着しました。

仕組みは以下のとおりです:

ケラー予想を2次元で解きたいとしましょう。コラディとサボーは、ケラーグラフと呼ばれるものを構築することで、この問題を解決する手法を考案しました。

まず、テーブルの上に16個のサイコロがあり、それぞれ2つの点がある面が上を向いていると想像してください。（点が2つであるという事実は、2次元の予想を扱っているという事実を反映しています。なぜ16個のサイコロなのかは、後ほど説明します。）次に、それぞれの点を赤、緑、白、黒の4色のいずれかで塗りつぶしてください。

1つのサイコロ上の点の位置は互いに交換できません。片方の位置がx座標を表し、もう片方がy座標を表すと考えてください。サイコロに色を付けたら、2つの条件が満たされる場合、サイコロのペアの間に線、つまりエッジを描き始めます。サイコロの片方の位置には異なる色の点があり、もう片方の位置には異なる色の点があるだけでなく、赤と緑が1つのペア、黒と白がもう1つのペアになっている場合です。

例えば、片方のサイコロに赤い点が2つあり、もう片方に黒い点が2つある場合、それらはつながっていません。片方の目（異なる色）の基準は満たしていますが、もう片方の目（ペアの色）の基準は満たしていません。しかし、片方のサイコロが赤黒で、もう片方が緑緑の場合、片方の目（赤と緑）はペアの色で、もう片方の目（黒と緑）は異なる色なので、つながっています。

4色を使って2つの点を塗る方法は16通りあります（そのため、16個のサイコロを使います）。16通りの可能性をすべて目の前に並べてみましょう。ルールに当てはまるサイコロのペアをすべて繋げてみましょう。さて、肝心な質問です。4つのサイコロがすべて繋がっているものを見つけられますか？

このような完全に連結したサイコロの部分集合はクリークと呼ばれます。もしクリークを見つけることができれば、2次元においてケラー予想が偽であることが証明できます。しかし、クリークは存在しないため、クリークを見つけることはできません。4つのサイコロからなるクリークが存在しないという事実は、2次元においてケラー予想が真であることを意味します。

サイコロはケラー予想において問題となるタイルそのものではありません。しかし、それぞれのサイコロがタイルを表していると考えることができます。点に割り当てられた色は、サイコロを空間に配置する座標と考えてください。そして、エッジの存在は、2つのサイコロが互いにどのように位置しているかを示すものと考えてください。

2つのサイコロの目が全く同じ色の場合、それらは空間的に全く同じ位置にあるタイルを表します。共通する色がなく、ペアの色もない場合（片方のサイコロが黒と白で、もう片方が緑と赤）、それらは部分的に重なり合うタイルを表します。これはタイル配置において許されないことを覚えておいてください。2つのサイコロの目がペアの色と、同じ色のセット（片方が赤と黒で、もう片方が緑と黒）の両方である場合、それらは同じ面を持つタイルを表します。

最後に、そして最も重要なのは、サイコロの片方の色がペアになっており、もう片方の色が単に異なる場合、つまり辺で繋がっている場合、サイコロは互いに接しているもののわずかにずれているため、面が完全に揃っていないタイルを表しているということです。まさにこの状態を調べたいのです。辺で繋がっているサイコロは、面を共有せずに繋がっているタイルを表しており、まさにケラーの予想を反証するために必要なタイルの配置です。

「彼らは互いに触れ合う必要があるが、完全に触れることはできない」とヒューレ氏は語った。

スケールアップ

30年前、コラディとサボーは、数学者がこの手順を用いて、実験パラメータを調整することで、あらゆる次元におけるケラー予想を検証できることを証明しました。3次元でケラー予想を証明するには、面に3つの点があり、3組の色を持つサイコロを216個使うかもしれません（ただし、この点については柔軟性があります）。そして、先ほどと同じ2つの条件を用いて、それらの中から互いに完全に繋がっている8つのサイコロ（2の3乗）を探します。

一般的な規則として、n次元でケラー予想を証明するには、n個の目のサイコロを使い、大きさが2 ^{nのクリークを探します。このクリークは、}n次元空間全体を覆える一種の「スーパータイル」（2 ^{n 個}の小さなタイルで構成）を表すものと考えることができます。

したがって、このスーパータイル (それ自体には面を共有するタイルが含まれていません) を見つけることができれば、それを変換またはシフトしたコピーを使用して、面を共有しないタイルで空間全体を覆うことができ、ケラーの予想を反証することができます。

「成功すれば、平行移動によって空間全体をカバーできます。共通の面を持たないブロックは、タイル全体に広がるでしょう」と、現在ミシガン大学に所属するラガリアス氏は述べた。

マッキーは8次元において、256個のサイコロ（2 ⁸）からなるクリークを発見することでケラー予想を反証しました。したがって、7次元におけるケラー予想を解くには、128個のサイコロ（2 ⁷）からなるクリークを探す必要がありました。そのクリークを見つければ、7次元におけるケラー予想が偽であることが証明されます。一方、そのようなクリークが存在できないことを証明すれば、ケラー予想が真であることが証明されます。

残念ながら、128個のサイコロからなるクリークを見つけるのは特に厄介な問題です。これまでの研究では、8次元と10次元は、ある意味では扱いやすい低次元空間に「因数分解」できるという事実を利用できました。しかし、今回はそのような幸運に恵まれませんでした。

「7次元は素数なので、低次元に分割できないので問題です」とラガリアスは言う。「そのため、これらのグラフの完全な組み合わせ論を扱うしか選択肢がなかったのです。」

128 個のクリークを探し出すことは、人間の脳だけでは難しい作業かもしれませんが、それはまさにコンピューターが得意とする種類の質問です。特に、少し手助けすれば、その答えは格段に容易になります。

論理の言語

クリーク探索をコンピュータが解ける問題にするには、命題論理を用いた問題の表現が必要です。命題論理とは、一連の制約を組み込んだ論理的推論の一種です。

あなたと2人の友人がパーティーの計画を立てているとしましょう。3人でゲストリストを作成しようとしていますが、それぞれの利害が対立しています。エイヴリーを招待したいか、ケンバを招待したくないか、どちらか一方を選びます。共同企画者の1人はケンバかブラッド、あるいは両方を招待したいと思っています。もう1人の共同企画者は、自分の都合でエイヴリーかブラッド、あるいは両方を招待したくないと思っています。これらの制約を踏まえて、あなたはこう自問自答するかもしれません。「3人のパーティー企画者全員の希望を満たすゲストリストはあるだろうか？」

コンピュータサイエンス用語では、この種の問題は充足可能性問題と呼ばれます。この問題は、命題式と呼ばれるもので記述することで解決します。この場合、A、K、Bの文字はそれぞれ潜在的なゲストを表します。(A OR NOT K) AND (K OR B) AND (NOT A OR NOT B) です。

コンピュータは、各変数に 0 か 1 を代入してこの式を評価します。0 は変数が偽、つまりオフになっていることを意味し、1 は真、つまりオンになっていることを意味します。つまり、「A」に 0 を代入すると Avery は招待されていないことを意味し、1 を代入すると招待されていることを意味します。この単純な式に 1 と 0 を割り当てる方法、つまりゲストリストを作成する方法は多数あり、それらを実行した後でコンピュータが競合する要求をすべて満たすのは不可能だと結論付ける可能性があります。ただしこの場合は、すべての人に当てはまる 1 と 0 を割り当てる方法が 2 つあります。A = 1、K = 1、B = 0 (Avery と Kemba を招待する) と A = 0、K = 0、B = 1 (Brad だけを招待する) です。

このような命題論理文を解くコンピュータプログラムはSATソルバーと呼ばれます。「SAT」は「satisfiability（満足可能性）」の略です。SATソルバーは変数のあらゆる組み合わせを探索し、一言で答えを出します。「はい、式を満たす方法があります」か「いいえ、ありません」かのどちらかです。

「式全体が真となるように各変数が真か偽かを判断するだけで、それができれば式は満たされるが、できなければ式は満たされない」とピッツバーグ大学のトーマス・ヘイルズ氏は語った。

128個のサイコロからなるクリークを見つけることが可能かどうかという問題も、似たような問題です。命題論理式として記述し、SATソルバーに入力することも可能です。まず、7個の点と6色のサイコロを多数用意します。指定されたルールに従って、128個のサイコロが互いに繋がるように点を色分けできますか？言い換えれば、クリークが実現可能な色分け方法はあるでしょうか？

クリークに関するこの問いを捉える命題式は非常に長く、39,000個の異なる変数を含んでいます。それぞれの変数には、0または1の2つの値のいずれかが割り当てられます。その結果、変数の可能な順列、つまりサイコロの色の並び方は2の^39,000通りとなり、非常に大きな数となります。

7 次元のケラー予想に答えるには、コンピューターはそれらの組み合わせをすべてチェックする必要があります。つまり、すべてを除外する (つまり、サイズ 128 のクリークは存在せず、ケラー予想は 7 次元では正しい) か、機能する 1 つだけを見つける (つまり、ケラー予想は誤り) 必要があります。

「単純なコンピュータにすべての可能な構成を検証させたとしたら、その数は324桁になるだろう」とマッキー氏は述べた。世界最速のコンピュータでさえ、すべての可能性を網羅するには永遠にかかるだろう。

しかし、今回の研究の著者たちは、コンピューターがあらゆる可能性を実際に検証することなく、決定的な結論に到達する方法を解明しました。鍵となるのは効率性です。

隠れた効率性

マッキーは、彼にとってプロジェクトが本当にうまくいったと感じた日のことを思い出す。カーネギーメロン大学のオフィスで、黒板の前に立ち、共著者のホイールとブラーケンシークと問題について議論していたとき、ホイールが探索を適切な時間で完了できるような構造化方法を提案したのだ。

「あの日、私のオフィスには真の知的な天才が働いていました」とマッキーは言った。「まるでウェイン・グレツキーを見ているようでしたし、NBAファイナルでレブロン・ジェームズを見ているようでした。今でも思い出すだけで鳥肌が立ちます。」

特定のケラーグラフの探索をスムーズにする方法は数多くあります。例えば、テーブルの上にたくさんのサイコロがあり、それらを128個、ケラーグラフのルールを満たすように並べようとしていると想像してみてください。12個は正しく並べられたとしても、次のサイコロを追加する方法が見つからない、といった状況です。その場合、12個のタイルという初期配置が成立しない、128個のサイコロの配置をすべて除外することができます。

「最初に割り当てた5つの項目が合わないことが分かれば、他の変数を見る必要がなくなり、検索にかかる時間が大幅に短縮される」と、現在マサチューセッツ工科大学に所属するショア氏は言う。

効率性のもう一つの形は対称性です。物体が対称的である場合、私たちはそれらをある意味で同じものとみなします。この同一性により、物体の一部を見るだけで全体を理解することができます。例えば、人間の顔を半分見るだけで、顔全体を再現することができます。

ケラーグラフでも同様のショートカットが使えます。もう一度、テーブルの上にサイコロを並べているところを想像してみてください。テーブルの中央から始めて、左に構成を構築していくかもしれません。4つのサイコロを並べたところで、行き詰まりにぶつかります。これで、1つの初期構成と、それに基づくすべての構成が除外されました。しかし、その初期構成の鏡像、つまりサイコロを同じように置きながら、右に構築していくときのサイコロの配置も除外できます。

「対称性を賢く考慮した満足度問題の解決方法を見つけることができれば、問題はずっと簡単になります」とヘイルズ氏は語った。

4 人の共同研究者は、こうした種類の検索効率を新たな方法で活用しました。特に、対称性に関する考慮を自動化しました。対称性については、これまでの研究では数学者がほぼ手作業で対処していました。

彼らは最終的に、サイズ128のクリークの探索を効率化し、2の^{39,000通りの}構成を調べる代わりに、SATソルバーは約10億通り（2の^30乗）の探索で済むようにしました。これにより、これまでは数億年かかっていたかもしれない探索が、朝の雑用へと変わりました。そしてついに、わずか30分の計算で答えが導き出されました。

「コンピューターはノーと答えたので、ケラー予想は成り立つと分かりました」とホイレ氏は述べた。128個のサイコロをすべて繋げて色分けする方法は存在しないため、ケラー予想は7次元では成立する。つまり、空間を覆うタイルの配置には、必ず同じ面を持つタイルが少なくとも2つ含まれるということだ。

コンピュータは実際には一言の答え以上のものを返しました。200ギガバイトにも及ぶ長い証明でその結論を裏付けました。

この証明は、コンピュータが検証した変数の配置をすべて読み出す以上のものです。それは、目的のクリークが存在するはずがないことを立証する論理的議論です。4人の研究者は、ケラーの証明を正式な証明チェッカー（議論の論理をトレースするコンピュータプログラム）に入力し、それが機能することを確認しました。

「全てのケースを調べて何も見つからないというのではなく、全てのケースを調べて、このものが存在しないという証明を書くことができるのです」とマッキー氏は言った。「充足不可能性を証明することができるのです。」

オリジナルストーリーは、数学、物理科学、生命科学の研究の進展や動向を取り上げることで科学に対する一般の理解を深めることを使命とする、シモンズ財団の編集上独立した出版物であるQuanta Magazineから許可を得て転載されました。

WIREDのその他の素晴らしい記事

スプレッドシートを駆使したIT担当者による投票権回復への取り組み
裁判所への侵入で2人のホワイトハットハッカーが刑務所に送られた経緯
次のサイケデリックな旅では、アプリがガイド役を務めます
科学者が携帯電話とレーザーを使ってマスクをテスト
ハイブリッドスクールは最も危険な選択肢かもしれない
🎙️ 未来がどのように実現されるかをテーマにした新しいポッドキャスト「Get WIRED」をお聴きください。最新エピソードを視聴し、📩ニュースレターに登録してすべての番組をチェックしましょう。
💻 Gearチームのお気に入りのノートパソコン、キーボード、タイピングの代替品、ノイズキャンセリングヘッドホンで仕事の効率をアップさせましょう