# Evaluating Autoformalization Robustness via Semantically Similar Paraphrasing

arXiv: https://arxiv.org/abs/2511.12784 · HTML: https://mlsanity.com/paper/2511.12784/

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 1 of its 8 references that are in the map.
- First posted on arXiv 16 Nov 2025.

## Builds on (most cited first, 1 of 1)

- [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022)

## Built on by (most cited first, 6 of 6)

- [Theory-Scale Auto-Formalization of Logics for Computer Science](https://mlsanity.com/paper/2606.26525/) (2026)
- [Characterizing Paraphrase-Induced Failures in Lean 4 Autoformalization](https://mlsanity.com/paper/2604.23135/) (2026)
- [From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier](https://mlsanity.com/paper/2607.07779/) (2026)
- [CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean](https://mlsanity.com/paper/2605.17255/) (2026)
- [A Pilot Benchmark for NL-to-FOL Translation in Planetary Exploration](https://mlsanity.com/paper/2605.17911/) (2026)
- [Analyzing the Narration Gap in LLM-Solver Loops](https://mlsanity.com/paper/2606.19588/) (2026)

## Abstract (arXiv)

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. 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 and Lean 4 version of ProofNet, 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.