Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs (2022)

Abstract: The ever-growing complexity of mathematical proofs makes their manual verification by mathematicians very cognitively demanding. Autoformalization seeks to address this by translating proofs written in natural language into a formal representation that is computer-verifiable via interactive theorem provers. In this paper, we introduce a semantic parsing approach, based on the Universal Transformer architecture, that translates elementary mathematical proofs into an equivalent formalization in the language of the Coq interactive theorem prover. The same architecture is also trained to translate simple imperative code decorated with Hoare triples into formally verifiable proofs of correctness in Coq. Experiments on a limited domain of artificial and human-written proofs show that the models generalize well to intermediate lengths not seen during training and variations in natural language.

## introduction to the uninitiated, the notion of mathematical proof represents simply an argument written by people to convince others of mathematical truth. however, in a real sense, mathematical proof must have formal underpinnings that go beyond the written argument. arguments that lack such underpinnings might have fatal errors or even logical inconsistencies (see, for example, russell's paradox (irvine and deutsch, 2021)). nevertheless, mathematical arguments written in natural language are the norm and they have great value. in @xcite 's well-known paper that discusses a somewhat controversial (at the time) proof of the four color theorem @xcite , he explores "what is a mathematical proof?" he posits that all mathematical proofs must be (i) convincing, (ii) surveyable, and (iii) formalizable. the first two points are for the reader-proofs must be convincing to and comprehensible by mathematicians. for the third point, he notes that, "most mathematicians and philosophers believe that any acceptable proof can be formalized. we can always find an appropriate formal language and theory in which the informal proof can be embedded and 'filled out' into a rigorous formal proof." for most mathematicians, this third part is crucial for ensuring that subtle, but fatal, errors in logic do not exist in mathematical proof. great progress has been made since the 1970's in fully formalizing significant mathematical results. for instance, the feit-thompson theorem @xcite and the four color theorem @xcite have been formally verified using the proof assistant coq @xcite , and the kepler conjecture @xcite has been formally verified using the proof assistants isabelle and hol light @xcite . moreover, proof assistants have demonstrated immense utility for software verification, such as the full certification of a c compiler @xcite . proofs demonstrating the correct behavior of code share a similar structure to proofs in pure mathematics, where systems like hoare logic replace standard first-order logic. thus, tymoczko's criteria for mathematical proof can be extended to the verification of programs. for many experts, latex provides an excellent tool for satisfying the first two criteria. in addition, carefully written latex (higham, 2020) provides a rich structure for establishing the third criterion. the vast majority of modern mathematics is expressed using natural language (nl), with the overwhelming majority typeset in latex. fully formalizing mathematics using proof assistants is still a difficult and time consuming task. this paper takes some preliminary steps toward bridging this gap by exploring how modern machine learning techniques can be used to convert carefully written latex into equivalent, and formally verified mathematics in coq, a process referred to as autoformalization in the literature @xcite . @xcite explored the similar task of translating mathematical statements from latex into mizar, using lstm-based models with attention. to generate aligned latex-mizar pairs, they use a tool @xcite that translates top-level mizar statements into artificial latex sentences, a task that is facilitated by the fact that mizar is human readable and similar in length with the corresponding latex version. carman (2021) evaluated the competency of lstms toward formalizing a restricted set of artificially generated theorems about simple arithmetic expressions, reporting reasonable success over expression lengths seen during training. more recently, @xcite evaluated codex and palm on a significantly more limited, but human-written set of theorems in algebra and number theory. in contrast to prior work, we address the autoformalization of both theorems and their proofs, and extend the scope to proofs of code correctness. we use a number of manually written mathematical statements to abstract a complex grammar that is then used to generate a dataset of substantially longer and more diverse mathematical theorems and proofs. we develop an architecture based on the universal transformer @xcite and adapt a copying mechanism @xcite to handle arbitrary numbers and variable names at test time. the models are evaluated extensively on their ability to systematically generalize to statement lengths not seen during training, for which we report sequence-level accuracy as well as a semantic-level accuracy calculated by combining sequence-level accuracy for the theorem and running coq to determine if the generated proof is correct. code and data are made available at https://github.com/gc974517/autoformalization . ## dataset of theorems and proofs we create two independent datasets of mathematical statements that overall correspond to four classes of theorems and proofs: the first dataset contains three classes of arithmetic statements (even-odd, composites, and powers), described in detail in section 2.1, and the second dataset containing statements about code correctness via hoare logic (poly), described in detail in section 2.2. in each example, the input theorem-proof pair is given in latex, whereas the formalized output is represented in coq. this work focuses on the proof assistant coq @xcite because (a) there is a rich set of mathematical libraries that have been developed for it, (b) it has been used successfully to reason about significant computation artifacts, such as the compercert c compiler @xcite ), and (c) it benefits from a rich set of training material for the proof assistant related to software verification @xcite . each class of examples demonstrates features necessary for the successful autoformalization of mathematical theorems and proofs. for example, powers and composites examples may define useful terminology to make the theorems shorter, e.g. proving that 4 is a square, or conversely they may state theorems directly without any preliminary definitions, e.g. proving ∃n. n 2 = 4. as shown in figures 3 and 4 , this corresponds in coq to aliasing propositions using the definition keyword. additionally, the examples in the dataset provide a stress test of the copying mechanism described in section 3.1, testing its ability to learn the correct order and number of terms to include in mathematical expressions, as well as their placement in theorems and proofs, in a way that generalizes to arbitrary tokens in mathematical language. for each of the four classes of theorems and proofs, we manually created a few examples ourselves in order to guide the construction of a complex grammar that is then used to generate a dataset of substantially longer and more diverse mathematical theorems and proofs. each dataset is generated using its corresponding grammar in an identical way. first, a random seed is sampled that controls the overall structure of the theorem, proof, and definition, if any. then, the skeleton structure of the proof is completed with phrases that are sampled from a separate context-free grammar. the coarse control of the skeleton structure allows the construction of examples with interesting features like sublemmas, forward or backward proof direction, coreference, or additional conditions for the theorem, among others. many of the difficulties in formalizing mathematical statements from nl into coq stem from the wide variability in the level of detail of mathematical proofs, and the frequent mismatch between what is considered an acceptable inference step in nl proofs vs. an inference step in coq. furthermore, there may be multiple coq proofs for any given theorem, at different levels of granularity. we address this ambiguity by requiring the structure of the coq proof to match the overall structure of the theorem. 28m + 308 is even. proof. we know the summation between even numbers in n will be an even number. observe that 308 is known to be even. additionally, note that the pair m × 28 is trivially even. this is true because the coefficient 28 is even. ## semantic parsing architecture to formalize latex statements into coq, we developed an encoder-decoder architecture based on the universal transformer @xcite . similar to @xcite , we do so by adding recursive passes into the encoder and decoder of a base transformer @xcite , thus making the model analogous to a universal transformer without adaptive computation time (act). further, we introduce a copying mechanism and support for out-of-vocabulary mathematical terms. ## experimental evaluations to evaluate the performance of trained models, we ran two primary experiments: first on the collection of arithmetic examples, then on the collection of code correctness examples. all models are evaluated in terms of sequence-level accuracy, where an example is considered correctly processed only if the generated coq sequence for both the theorem and its proof perfectly matches token by token the ground truth sequence. we also report semantic-level accuracy, for which the generated coq theorem needs to attains a perfect sequencelevel accuracy and the coq engine verifies that the generated coq proof truly proves the generated coq theorm, regardless of whether it matches the ground truth version of the proof. this emphasizes that the model was able to capture the general meaning of the natural language proof by correctly translating the theorem and successfully proving it using the natural language version as a guide. all experiments were performed on one nvidia rtx-a6000 gpu with 48gb of memory. ## concluding remarks as we have seen, it is feasible to train machine learning models to perform autoformalization over very restricted domains of math and code correctness proofs. these models show capability to systematically generalize to new expression lengths and program sizes. moreover, these models were able to translate previously unseen hand written natural language examples, albeit with lower accuracy. we are hopeful that this approach can be applied to autoformalization of a larger segment of mathematics and code verification. as mentioned by @xcite , "autoformalization is not just a challenge: successful autoformalization would represent a breakthrough for general ai with significant implications in various domains." we see an especially significant impact in education, where integration of autoformalization into proof assistants for introductory mathematics and software verification courses would enable the detection of missing steps or misconceptions in students' proofs.