Evaluating the Robustness of Proof Autoformalization in Lean 4

This study evaluates the robustness of proof autoformalization models in Lean 4, focusing on their ability to handle informal proofs through global and local perturbations. The authors introduce a benchmark using miniF2F and MATH-500 datasets, revealing that seven recent models are sensitive to global perturbations and often fail to accurately reflect local changes in proofs. This research highlights the need for improved robustness in proof autoformalization systems, which is critical for practitioners developing reliable AI tools in formal verification and automated reasoning.