掛け算22回、1回たりとも減らせない

利益相反。 著者らによれば、AIエージェント(AnthropicのClaude)が、著者らの指示の下で、探索コードと、人間による監査を必要としないLeanの証明を書いた。一方、人間が監査しなければならない部分は著者らが設計した。この記事もClaudeが書いている。

数の正方形の格子、すなわち行列を2つ、学校で習うやり方で掛け合わせると、n行n列の格子ではn³回の掛け算が必要になる。ストラッセン(Strassen)は、2 × 2の行列2つを8回ではなく7回の掛け算で掛け合わせられることを示した。この技は再帰的に使える。大きな行列を4つのブロックに切り分け、それぞれのブロックを1つの数のように扱い、これを繰り返すのだ。するとコストはn³ではなくn^2.807のように増える。論文によれば、この2 × 2のレシピは1971年に最適であることが証明されている。

同じ考え方は、どんな固定サイズでも通用する。3 × 3の行列2つをr回の掛け算で掛け合わせ、要素がブロックでも成り立つレシピがあれば、コストはnのlog₃ r乗のように増える。簡単な計算で、何がかかっているかがわかる。そうしたレシピは、rが21以下のときにちょうどストラッセンに勝ち、22以上なら負ける。知られている最良の3 × 3のレシピはラダーマン(Laderman)によるもので、23回の掛け算を使い、1976年以来改良されていない。

半開きのままだった扉

ある問題について可能な最良の回数を、そのランクと呼ぶ。3 × 3の掛け算のランクの下界は、ゆっくりと上がってきた。2003年に19、そして2026年3月に20である。後者は王(Wang)が、0と1しかなく1 + 1 = 0となる小さな数の体系の上で計算したものだ。2026年9月には、王と、楊(Yang)率いるチームが、互いに10日以内の差でそれぞれ独立に21に到達した。しかし21では、ストラッセンより速い3 × 3のレシピの余地がまだ残っていた。

ポリテクニーク・モントリオールとカーネギーメロン大学のアイザック・ルディッチ(Isaac Rudich)と、ポリテクニーク・モントリオールのルイ=マルタン・ルソー(Louis-Martin Rousseau)は、今回その下界を22に押し上げた。

定理1。 2つの3 × 3行列を整数の定数を用いて掛け合わせ、任意のサイズのブロックに再帰的に適用できるアルゴリズムは、どれも少なくとも22回の掛け算を使う。

したがって、そうしたアルゴリズムはどれも約n^2.814より良くはならず、ストラッセンの2 × 2の方法に勝つものはない。

496の小さなパズル

証明は王が考案した表に基づいている。この表は、難しい問題を496のより易しい問題に分割する。それぞれの問題は、1つ目の行列に「条件」を加える。たとえば、ある要素どうしを足すとゼロになる、といった条件だ。条件が多いほど問題は易しくなり、最後は行列がすべてゼロという自明な場合に行き着く。

著者らはまず、それぞれのパズルの真の答えを、証明を試みる前に教えてくれる厳密な探索プログラムをつくった。その答えは地図の役割を果たし、どの下界を追いかける価値があるかを示した。最終的に、彼らの証明は496のパズルすべてに下界を与え、そのうち359を厳密に決定し(王の最新の結果では195)、252について下界を引き上げた。彼ら独自の「貼り合わせ」定理は、2つのより易しいパズルのレシピを組み合わせて3つ目のパズルのレシピをつくるもので、上界のうち145を提供した。

最終的な主張では2つの条件が重要になる。整数の定数:整数の定数をもつレシピを0と1の数の体系で読み替えても、掛け算の回数を増やさずに有効なレシピのままなので、下界がそのまま移る。ブロック:この要件がなければ近道が存在する。論文が引用するロソウスキ(Rosowski)の3 × 3アルゴリズムは掛け算21回しか必要としないが、数が交換可能であることに頼っており、再帰的には適用できない。

機械が検証した証明

証明はLeanで書かれている。Leanはプログラミング言語の一種で、すべてのステップが検証されたときにだけ定理がコンパイルされる。証明全体は3,521のモジュールにわたって約100万行に及び、1つのプロセッサコアで検証に11.1時間かかる。そのすべてを誰かが読む必要はない。監査役が読むのは約1,000行のライブラリで、どんな証明も存在する前に著者らが書いたものだ。そこでは掛け算のレシピとは何かが定義され、定理が述べられている。残りはLeanのカーネルが検証し、独立したチェッカーで結果を再現することもできる。

著者らはまた、AIエージェントが文献を探したことにも触れている。それぞれの参考文献が実在することは確認したが、「それぞれに私たちがその文献の功績とする考えがそのまま含まれていることまでは確認していない」。

最後の隔たり

1つの問いが残っている。掛け算22回の3 × 3のレシピは存在するのか、それともラダーマンの23回が真の最小値なのか。著者らはこの隔たりが「まもなく埋まる」と予想しており、それが実現したとき、あるいは論文の出版が受理されたときに、探索コードを公開するという。また、この下界は整数でない定数をもつレシピを対象外としている。