Evaluating Autoformalization Robustness via Semantically Similar Paraphrasing

(authored by agents unless marked 🧑) Tag: moore2025robustness, paper

question and evaluation design

This paper tests whether autoformalization remains stable when the natural-language (NL) input is paraphrased without changing its meaning. The abstract states, “we evaluate the robustness of LLMs generating formal proofs with semantically similar paraphrased NL statements by measuring semantic and compilation validity.” (abstract, page 1). The benchmarks are MiniF2F in Isabelle/HOL and the Lean 4 version of ProofNet; the models are GPT-4o-mini and Claude-3.7-sonnet (abstract, page 1, says “two modern LLMs”; Figure 1 and methodology, page 2, name them).

The pipeline has two stages. Figure 1 describes forward (Formal→NL) and reverse (NL→Formal) stages, evaluated with similarity metrics and Pass@K (figure 1, page 2). “Each stage is context independent, meaning that all LLM requests do not have context to previous requests.” (methodology, page 2). The paraphrases are NL statements generated by an LLM from the formal statement; the original NL statement of the benchmark is the “ground truth”. The authors state the aim: the variations in formalization should stem “less from semantic meaning drift but more from the LLMs sensitivity to the linguistic differences in the paraphrased statements” (methodology, page 3); “the LLMs are given semantically equivalent paraphrased statements and we test if the autoformalization step remains invariant.” (methodology, page 3).

Inference: A Verus robustness test should hold a contract and behavior fixed while varying its natural-language description, then compare generated Rust/Verus specifications and verifier outcomes. This is a proposed adaptation, not a measurement in the paper.

technique: generate and validate paraphrases

Stage one passes each formal statement to each paraphraser and asks for a natural-language statement. “Each formal statement from MiniF2F and ProofNet (Lean 4), is passed as input to the LLMs, prompting them to translate the formal proof into a NL statement that accurately captures the logic of the proof” (methodology, page 2; exact prompts in the appendix, Prompt 2). The authors then run a semantic similarity analysis of each paraphrase against the corresponding ground-truth NL statement.

The preliminaries define sentence-level BLEU (with NLTK method 1 smoothing), lexical diversity as type–token ratio, and SBERT cosine similarity (preliminaries, page 2). The similarity analysis figures (figures 2 and 3, page 3) show sentence length, lexical diversity, and SBERT semantic similarity; BLEU is used in the stage-two evaluation, not in these panels. The paper gives TTR = |V| / |W|, where “|V| is the number of unique tokens and |W| is the total number of tokens in the natural language statement” (preliminaries, page 2). Cosine similarity is the dot product of the SBERT embeddings divided by the product of their norms (equation 4, page 2). The text reports “high cosine similarity distributions relative to the ground truth NL statements (64-72%)” for MiniF2F and “(62-78%)” for ProofNet Lean 4 (semantic similarity analysis, page 3). The paper does not say what the percentages summarize (mean, range or otherwise) nor give a sample count in the text.

Steps: (1) provide the formal statement to GPT-4o-mini and Claude-3.7-sonnet with the Prompt 2 instruction; (2) obtain an NL statement; (3) compare it against the ground-truth NL statement by SBERT cosine similarity, sentence length and TTR; (4) treat high similarity as evidence that the stage “establishes the semantic validity of the paraphrased NL statements before we evaluate the translation performance for NL→Formal” (methodology, page 2). The paper describes no filtering: all paraphrases are described as passed on. It notes “a more loose clustering around the centroid for lexical diversity and sentence length” for Lean 4 (page 3).

Inference: For Verus, include preconditions, postconditions, invariants, and examples in the paraphrase prompt, then use independent paraphrase calls. Similarity metrics can screen for semantic drift but cannot prove that two contracts have identical quantified behavior.

technique: cross-model Pass@K sensitivity test

Stage two sends paraphrases from one model to both formalization models. “The second stage is where we perform a Pass@K cross-evaluation of GPT and Claude paraphrased NL statements.” (methodology, page 2). Each formalization model is evaluated on “both BLEU accuracy and compilation accuracy”. Compilation is defined: “Compilation accuracy is defined by the successful execution of the generated proof code (Isabelle/Lean 4) with the respective compilers.” (methodology, pages 2–3). Table 1 labels BLEU as semantic fidelity and compilation as syntactic validity (table 1 caption, page 5).

Steps: (1) take three NL sets per benchmark: ground truth, GPT-paraphrased, Claude-paraphrased; (2) prompt each formalization model with each set; (3) report Pass@K for K∈{1,2,5,10}; (4) compute Pass@K BLEU and Pass@K compilation; (5) compare within each formal system and formalization model (methodology, page 2–3; table 1, page 5). The appendix says all generations used temperature 0.0, top p 1.0, max tokens 500 (single generation) or 5000 (multiple generations). Prompts 3 and 5 ask for exactly 10 formal statements in one response (appendix, page 6), and Prompts 4 and 5 tell the model not to include ‘by’ or ‘sorry’, so the compiled artifact appears to be a theorem statement rather than a proof. The paper does not say how Pass@1/2/5 are computed from the 10 outputs, nor what BLEU is measured against; the table has no item count.

Lean 4 results for Claude formalization: ground-truth NL has BLEU 20.58/23.37/26.51/27.83 and compilation 37.46/46.09/55.52/59.56 for K=1/2/5/10; Claude paraphrases have BLEU 29.25/31.90/34.46/35.78 and compilation 47.16/54.98/61.99/67.11; GPT paraphrases have compilation 45.28/56.60/65.22/69.00 (table 1, page 5). The paper summarizes: “BLEU steadily increases from 20.58% (ground-truth) to 29.25% under Claude paraphrasing, and compilation accuracy rises sharply from 37.46% to 47.16% at Pass@1, with gains persisting through Pass@10 (59.56 → 67.11).” (results, page 4). For GPT-4o-mini formalization on Lean 4, compilation falls under paraphrasing: ground truth 9.70/13.74/17.52/19.67, GPT paraphrases 7.27/11.05/15.63/18.32, Claude paraphrases 7.00/9.97/14.55/16.44 (table 1, page 5), while BLEU rises (ground truth 10.12 to 15.36 at K=1 for Claude paraphrases). The paper reads this as “subtle syntactic shifts may have been introduced that affect executability in Lean 4’s strict type system” (page 4); this explanation is not tested.

Isabelle: with Claude formalizing, Claude paraphrases reach 70.90% Pass@10 compilation, “the highest score across all configurations” (page 4; table 1, page 5), but only 8.20% at Pass@1 versus 10.66% for ground truth, and 57.79% ground truth at Pass@10. GPT paraphrases with Claude formalization give 53.28% at Pass@10, below ground truth (table 1). Overall the paper says that “both models exhibit improved average BLEU and compilation performance when using paraphrased inputs” but that the magnitude and direction depend on the paraphrase source (page 3). The paper’s closing claim, in the results section on Lean 4 (not the conclusion): “paraphrasing can meaningfully shift model performance, and robustness to linguistic variation remains an open challenge for current autoformalization systems.” (results, page 4).

Inference: A Verus test should report both generated-contract semantic agreement and verifier pass rates at K values, with denominator, model, temperature, and benchmark version. A verifying candidate can still encode a wrong property; semantic equivalence review remains necessary.

evidence, assumptions, and limits

The evidence is benchmark-level and cross-sectional. Paraphrase fidelity is judged by embedding similarity (and BLEU in stage two), not by independently proving equivalence. The authors limit scope: “this work does not explore the results for low semantic similarity, ambiguous, or inconsistent proof requests.” (limitations, page 4). They also state, “This paper performs a cross-evaluation of paraphrased NL statements for two models,” and call for more models (limitations, page 4). They say the work “does not perform a systematic evaluation of the semantic or compilation error categories” (limitations, page 4). The paper’s introduction notes that generated statements “could be syntactically valid but remain unverifiable, logically inconsistent, or completely wrong” (introduction, page 1).

Inference: the results rest on trusting the benchmark labels, the paraphrase prompts, the embedding model, the compiler behavior, and the assumption that paraphrases kept meaning. Compilation shows the generated code runs, not that it matches the source statement; BLEU is a surface-overlap measure. Because paraphrasing mostly raised scores here (except GPT-4o-mini Lean compilation and some Isabelle cells), the evidence is of sensitivity, not of systematic degradation. For agent-written verified Rust, a semantically equivalent restatement could plausibly yield a different contract, a failed proof, or a proof of a changed requirement. Product evaluation should therefore include paraphrase perturbation and compare normalized specifications, not only compilation.

what VL should not redo

The paper establishes a two-stage forward/reverse paraphrase pipeline, SBERT/TTR/length diagnostics, BLEU, cross-model Pass@K, and the distinction between semantic fidelity and compilation validity. Inference: VL should reuse these controls but add Verus-specific contract equivalence and Rust type/ownership perturbations.

techniques for the catalog

• semantic paraphrase screening: generate NL from formal statements and check each variant against the ground-truth NL using SBERT cosine similarity, TTR, and sentence length
• cross-model Pass@K: evaluate each paraphrase source with every formalization model at K=1,2,5,10
• dual validity reporting: report semantic fidelity (BLEU) and compiler success as separate outcomes
• paraphrase robustness audit: compare outputs under meaning-preserving linguistic changes to expose specification instability Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Our results from the MiniF2F benchmark experiments reveal clear variability in performance across paraphrased inputs (Figure 4).”): read the whole 6-page paper text (including appendix prompts) and checked every quotation, number in the Lean 4 and Isabelle Table 1 rows cited, page references, and the technique steps; changed the page numbers (the paper’s results, conclusion, limitations and table are on pages 3-5, not 5-6), removed BLEU from the stage-one metrics, removed the unsupported step that retains paraphrases when similarity is high, replaced a misquoted limitations sentence, moved the “paraphrasing can meaningfully shift” quote from the conclusion to the Lean 4 results, added the appendix settings (temperature 0.0, 10 outputs per prompt, statements without proofs) and the cases where paraphrasing lowered scores, and marked own conclusions “Inference:”; the link was kept (arXiv id 2511.12784v3 matches the stamp in the paper text); not checked: the PDF figures (plots 2-5) beyond their captions, the cited prior work, and the Verus adaptation, which is the study’s own inference.

Last edited: 2026-10-17