整数係数の3×3行列積には少なくとも22回の乗算が必要
Lower Bound of 22 for 3x3 Matrix Multiplication over the Integers
この論文をやさしく読む
ひとことで言うと
整数定数を使う3×3の行列乗算を再帰的に繰り返す方式では、Strassenの2×2方式より速い指数は得られないと証明しています。
何に役立つ？
行列乗算アルゴリズムを探索するとき、この条件の3×3方式にどこまで改善の余地があるかを絞り込む基礎結果です。
この研究の面白いところ
乗算回数の下界を21から22へ一つ引き上げるだけで、Strassenの指数を上回れるかという判断が変わります。Leanでアルゴリズムの限界そのものを形式化した点も特徴です。
どこまで分かった？
下界の対象は整数定数を使う3×3の再帰的アルゴリズムです。あらゆる行列乗算法の限界を示すものではなく、最良既知の23回と今回の下界22回の間には差が残ります。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
Strassenは、二つの2×2行列の積を、8回ではなく7回の乗算で計算できることを示した。このアルゴリズムを再帰的に適用すると、二つのn×n行列をO(n^2.807)回の乗算で掛け合わせることができ、素朴な方法のO(n^3)を上回る。既知の最良の3×3再帰的行列乗算アルゴリズムは23回の乗算を使い、計算量はO(n^2.854)である。公表済みの最良の下界は、整数定数を使うアルゴリズムについて21回であり、O(n^2.771)回の乗算で計算するアルゴリズムの余地を残している。そのため、この下界ではStrassenの方法を上回るアルゴリズムの可能性を排除できない。 本研究では、整数定数を使うあらゆる3×3再帰的アルゴリズムについて、乗算回数の下界が22回であることを証明する。これにより、そのようなアルゴリズムはO(n^2.814)回の乗算より良い計算量を達成できず、Strassenの2×2方式を上回る3×3アルゴリズムの可能性が排除される。 証明は、問題を496個の部分問題へ分解して取り組んだWangの最近の分解手法に基づく。そのうち359個について厳密な解を与える。証明はLeanで記述されており、検証に必要な監査対象は少数の短いファイルのみである。このLeanによる形式化は、単に問題のランクを述べるのではなく、行列乗算の再帰的アルゴリズムの限界についての主張を直接符号化している。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-10-01（UTC）
- 最新改訂
- 2026-10-01 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-10-01 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
Strassen showed that two 2x2 matrices can be multiplied with 7 multiplications instead of 8. Applied recursively, his algorithm multiplies two nxn matrices with O(n^2.807) multiplications, beating the naive O(n^3). The best known 3x3 recursive matrix multiplication algorithm uses 23 multiplications O(n^2.854). The best published lower bound of 21 (on algorithms with integer constants) leaves room for an algorithm with O(n^2.771) multiplications, and thus does not rule out the possibility of an algorithm that would beat Strassen's. We prove a lower bound of 22 multiplications for any 3x3 recursive algorithm with integer constants, proving that no such algorithm can do better than O(n^2.814) multiplications, and eliminating the possibility of a 3x3 algorithm that beats Strassen's 2x2 method. The proof builds on a recent decomposition method from Wang, who approached the problem by turning it into 496 subproblems. We provide exact solutions for 359 of them. The proof is in Lean; verification requires auditing only a few short files. The Lean formalization directly encodes statements about the limitations of recursive algorithms for matrix multiplication, as opposed to just a statement about the rank of the problem.
arXiv ID: 2610.01639 ／ 要約の誤りについて