Evaluating Autoformalization Robustness via Semantically Similar Paraphrasing
This work addresses the problem of unreliable autoformalization for users relying on LLMs, but it is incremental as it extends known robustness issues from text-to-SQL to a new domain.
The paper investigates the robustness of large language models (LLMs) in autoformalization by evaluating their performance on semantically similar paraphrased natural language inputs, finding that minor shifts in statements can significantly impact model outputs, with variability observed across benchmarks like MiniF2F and ProofNet.
Large Language Models (LLMs) have recently emerged as powerful tools for autoformalization. Despite their impressive performance, these models can still struggle to produce grounded and verifiable formalizations. Recent work in text-to-SQL, has revealed that LLMs can be sensitive to paraphrased natural language (NL) inputs, even when high degrees of semantic fidelity are preserved (Safarzadeh, Oroojlooyjadid, and Roth 2025). In this paper, we investigate this claim in the autoformalization domain. Specifically, we evaluate the robustness of LLMs generating formal proofs with semantically similar paraphrased NL statements by measuring semantic and compilation validity. Using the formal benchmarks MiniF2F (Zheng, Han, and Polu 2021) and Lean 4 version of ProofNet (Xin et al. 2024), and two modern LLMs, we generate paraphrased natural language statements and cross-evaluate these statements across both models. The results of this paper reveal performance variability across paraphrased inputs, demonstrating that minor shifts in NL statements can significantly impact model outputs.