Machine-Verifying Toom-Cook Multiplication with Integer Evaluation Points
This work addresses the challenge of ensuring reliability in fast multiplication algorithms for computational mathematics, though it is incremental as it builds on existing verification methods with AI assistance.
The paper tackles the problem of verifying the correctness of Toom-Cook multiplication algorithms with integer evaluation points by presenting a machine-verified proof in Lean 4, deriving a threshold function that guarantees algorithm termination for any selection of points when the base-case size is above this threshold.
We present a machine-verified proof of the correctness of Toom-Cook multiplication with generalized integer evaluation points. Toom-Cook is a class of fast multiplication algorithms parameterized by a triple $(k_x, k_y, \vec v)$ consisting of two positive integer split sizes $k_x, k_y$ and a vector $\vec v$ of distinct evaluation points. As part of our proof, we verify that for any selection of $k_x+k_y-1$ distinct integer evaluation points, we can compute a threshold function $θ(k_x, k_y, \vec v)$ such that, if the algorithm's base-case problem size is set above this threshold, then the algorithm's termination is guaranteed regardless of the values of the operands. The threshold formula, which we derive by obtaining upper bounds on the subproblem sizes produced by the Toom-Cook recurrence, does not depend on the operands; it depends only on $k_x$, $k_y$, $\vec v$, and the base $b$ in which we operate. We write the proof in Lean 4, making use of the Mathlib library. We formalize the algorithm, our base case threshold formula, and our key lemma statements in Lean. We then use the AI theorem prover Aristotle to assist in completing the machine verification of the algorithm's correctness. This proof, through its synthesis of human input and AI assistance, demonstrates the considerable power of AI to automate the machine verification process.