New benchmark shows 7 autoformalization LLMs fail robustness tests

Proof autoformalization aims to convert natural-language mathematical proofs into formal code for systems like Lean 4. However, existing benchmarks only test on curated, perfectly formed proofs. A new paper from Zhengtao Gui, Sheng Yang, and Zhouxing Shi introduces the first robustness evaluation for autoformalization models, using two types of perturbations. The first, global perturbation, paraphrases the informal proof in a different style — the formalization should remain correct even if the wording changes. The second, local perturbation, alters a specific value, symbol, or step (often counterfactually) — a robust model should faithfully reflect that change instead of reverting to the original or inferring something else.

The researchers built a benchmark based on miniF2F and MATH-500, then tested seven state-of-the-art models. Results were sobering: every model was sensitive to global perturbations, meaning small rewrites could flip correctness. More critically, all models largely failed under local perturbations — they ignored counterfactual changes or silently corrected them back, indicating a tendency to hallucinate rather than follow the actual input. The work highlights that today’s autoformalizers lack the robustness needed for reliable translation of real-world mathematical reasoning, and provides code and data for further research.