Lower bound proves limits for 3x3 matrix multiplication speed
Lower Bound of 22 for 3x3 Matrix Multiplication over the Integers
Computational Complexity
Summary
Multiplying matrices is a common math problem in computing, and finding faster ways to do it helps many technologies. Previous work showed a clever method to multiply 2x2 matrices faster than usual, leading to faster multiplication for larger matrices. This paper proves that for 3x3 matrices, you need at least 22 multiplications, which means you cannot beat the speed achieved by the 2x2 method when scaling up. The authors use a detailed mathematical and computer-verified proof to establish this new lower limit.
What this means in practice
- •For algorithm designers: Avoid attempts to find 3x3 recursive multiplication algorithms with fewer than 22 multiplications, focusing effort on other problem sizes or methods.
- •For high performance computing engineers: Use the new lower bound to guide optimization strategies for matrix multiplication, understanding that 3x3 block recursions cannot outperform existing 2x2 based methods.
A theory result. No direct application yet.
Authors
Isaac Rudich, Louis-Martin Rousseau
Abstract
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.