Srihari Nanniyur

Srihari Nanniyur, Siddhartha Jayanti

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.

Jianing Zhou, Hongyu Gong, Srihari Nanniyur et al.

We study a new application for text generation -- idiomatic sentence generation -- which aims to transfer literal phrases in sentences into their idiomatic counterparts. Inspired by psycholinguistic theories of idiom use in one's native language, we propose a novel approach for this task, which retrieves the appropriate idiom for a given literal sentence, extracts the span of the sentence to be replaced by the idiom, and generates the idiomatic sentence by using a neural model to combine the retrieved idiom and the remainder of the sentence. Experiments on a novel dataset created for this task show that our model is able to effectively transfer literal sentences into idiomatic ones. Furthermore, automatic and human evaluations show that for this task, the proposed model outperforms a series of competitive baseline models for text generation.