📄 Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs

Summary

Checking long mathematical proofs by hand is cognitively demanding. Autoformalization aims to help by converting natural-language proofs into code that an interactive theorem prover can check. The authors frame this as semantic parsing: LaTeX theorem–proof pairs are mapped to Coq. They cover elementary arithmetic and, separately, the correctness of simple imperative programs annotated with Hoare triples.

Training data is synthetic. A few hand-written seed examples guided the design of a rich grammar that produces LaTeX and Coq versions roughly in parallel. This includes features such as sublemmas, coreference, and different proof directions.

The model is a Universal Transformer with relative positional encodings and a copying mechanism, which handles unseen numbers and variable names. Results are measured by exact token match and by a semantic check, in which Coq verifies the generated proof.

The models generalize well to intermediate expression lengths and program sizes absent from training, but fail on lengths beyond the training range. They also handle hand-written inputs, though less accurately. The work suggests autoformalization is feasible in narrow domains, with possible uses in teaching proofs and software verification.

Key points

• Datasets: four classes of examples. EVEN-ODD, COMPOSITES and POWERS are arithmetic; POLY covers Hoare-logic code correctness. The grammars can in principle yield over 283 million arithmetic and over 491,000 code examples.
• Splits: 5,000 EVEN-ODD, 5,000 COMPOSITES and 2,000 POWERS examples were generated for each of training and testing. Training used n ∈ {2, 3, 5, 7, 9}; testing covered n from 2 to 12.
• Handwritten test set: an extra 45 human-written LaTeX pairs, 15 per arithmetic class, test robustness to grammatical structures outside the generator.
• Positional encodings: with absolute positional encodings, a Transformer scored 0% sequence-level accuracy on unseen lengths, so relative encodings were essential.
• POLY model: a deeper model (8 blocks, 8 recurrent passes, 8 heads) generalized to unseen program lengths of 4–10 lines, and depth clearly helped. Sequence-level and semantic-level accuracy coincided for POLY. Code and data are at github.com/gc974517/autoformalization.