Surface Sensitivity in Lean 4 Autoformalization

• URL: http://arxiv.org/abs/2604.23135v1
• Date: Sat, 25 Apr 2026 04:26:19 GMT
• Title: Surface Sensitivity in Lean 4 Autoformalization
• Abstract summary: We find that the observed paraphrase sensitivity reflects compilation-boundary failures rather than semantic divergence among successful formalizations.<n>Our results suggest that future training-time interventions should target the compile boundary rather than the semantic layer.
• Score: 1.7855077077275565
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Natural-language variation poses a key challenge in Lean autoformalization: semantically equivalent paraphrases of the same theorem statements can induce divergent formal outputs, yet it remains unclear whether this variation reflects semantic disagreements or shallower failures. We investigate this question in Lean 4 using 60 deterministic paraphrase rules applied to ProofNet\# and miniF2F. Across four GPT-family models and three open-weight 7B autoformalizers, we find that the observed paraphrase sensitivity reflects compilation-boundary failures rather than semantic divergence among successful formalizations. In particular, when both baseline and perturbed outputs compile, paired predictions are semantically equivalent under BEq+ and structurally near-identical under GTED. By contrast, paraphrasing substantially affects whether outputs compile, with failure modes varying across datasets and perturbation classes. Our results suggest that future training-time interventions should target the compile boundary rather than the semantic layer, and that benchmarks should separate compile-conditional equivalence from surface consistency.

Related papers

• Evaluating the Robustness of Proof Autoformalization in Lean 4 [8.029528831501514]
  We argue that a robust proof autoformalizer must remain faithful even for informal proofs that diverge from idealized ones.<n>We build a benchmark with both perturbations on miniF2F and MATH-500.<n>We evaluate seven recent models, all of which are sensitive to global perturbations and mostly fail to remain faithful under local perturbations.
  arXiv  Detail & Related papers  (2026-06-12T18:10:21Z)
• CausalFlip: A Benchmark for LLM Causal Judgment Beyond Semantic Matching [50.65932158912512]
  We propose a new causal reasoning benchmark, CausalFlip, to encourage the development of new large language models.<n>CaulFlip consists of causal judgment questions built over event triples that could form different confounder, chain, and collider relations.<n>We evaluate LLMs under multiple training paradigms, including answer-only training, explicit Chain-of-Thought supervision, and a proposed internalized causal reasoning approach.
  arXiv  Detail & Related papers  (2026-02-23T18:06:15Z)
• Beyond Memorization: Testing LLM Reasoning on Unseen Theory of Computation Tasks [8.210112631285666]
  Large language models (LLMs) have demonstrated strong performance on formal language tasks.<n>We introduce a benchmark for deterministic finite automata (DFA) construction from regular languages.<n>We show that models achieve perfect accuracy on factual questions and 84-90% on seen tasks, but accuracy drops sharply on unseen problems.
  arXiv  Detail & Related papers  (2026-01-19T21:00:31Z)
• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
  We propose a Reflective Autoformalization method that integrates semantic consistency evaluation into the autoformalization process.<n>This enables the model to iteratively generate formal statements, assess its semantic fidelity, and self-correct identified errors.<n>Experiments show that ReForm achieves an average improvement of 22.6 percentage points over the strongest baselines.
  arXiv  Detail & Related papers  (2025-10-28T16:22:54Z)
• Efficient semantic uncertainty quantification in language models via diversity-steered sampling [46.23327887393273]
  We introduce a diversity-steered sampler that discourages semantically redundant outputs during decoding.<n>Key idea is to inject a continuous semantic-similarity penalty into the model's proposal distribution.<n>Being modular and requiring no gradient access to the base LLM, the framework promises to serve as a drop-in enhancement for uncertainty estimation.
  arXiv  Detail & Related papers  (2025-10-24T10:06:21Z)
• From Disagreement to Understanding: The Case for Ambiguity Detection in NLI [3.5164356851161984]
  This position paper argues that annotation disagreement in Natural Language Inference (NLI) is not mere noise but often reflects meaningful variation.<n>We call for a shift toward ambiguity-aware NLI that first identifies ambiguous input pairs, classifies their types, and only then proceeds to inference.
  arXiv  Detail & Related papers  (2025-07-20T20:27:35Z)
• Same Question, Different Words: A Latent Adversarial Framework for Prompt Robustness [9.208007322096535]
  We present Latent Adversarial Paraphrasing (LAP), a dual-loop adversarial framework.<n>LAP trains a learnable perturbation to serve as a "latent continuous paraphrase"<n>We conduct experiments to demonstrate the effectiveness of LAP across multiple LLM architectures.
  arXiv  Detail & Related papers  (2025-03-03T09:36:50Z)
• The Remarkable Robustness of LLMs: Stages of Inference? [5.346230590800585]
  We investigate the robustness of Large Language Models (LLMs) to structural interventions by deleting and swapping adjacent layers during inference.<n>Surprisingly, models retain 72-95% of their original top-1 prediction accuracy without any fine-tuning.
  arXiv  Detail & Related papers  (2024-06-27T17:57:03Z)
• Cycles of Thought: Measuring LLM Confidence through Stable Explanations [53.15438489398938]
  Large language models (LLMs) can reach and even surpass human-level accuracy on a variety of benchmarks, but their overconfidence in incorrect responses is still a well-documented failure mode. We propose a framework for measuring an LLM's uncertainty with respect to the distribution of generated explanations for an answer.
  arXiv  Detail & Related papers  (2024-06-05T16:35:30Z)
• Decomposing Uncertainty for Large Language Models through Input Clarification Ensembling [69.83976050879318]
  In large language models (LLMs), identifying sources of uncertainty is an important step toward improving reliability, trustworthiness, and interpretability. In this paper, we introduce an uncertainty decomposition framework for LLMs, called input clarification ensembling. Our approach generates a set of clarifications for the input, feeds them into an LLM, and ensembles the corresponding predictions.
  arXiv  Detail & Related papers  (2023-11-15T05:58:35Z)
• Dive into Ambiguity: Latent Distribution Mining and Pairwise Uncertainty Estimation for Facial Expression Recognition [59.52434325897716]
  We propose a solution, named DMUE, to address the problem of annotation ambiguity from two perspectives. For the former, an auxiliary multi-branch learning framework is introduced to better mine and describe the latent distribution in the label space. For the latter, the pairwise relationship of semantic feature between instances are fully exploited to estimate the ambiguity extent in the instance space.
  arXiv  Detail & Related papers  (2021-04-01T03:21:57Z)
• Learning Causal Semantic Representation for Out-of-Distribution Prediction [125.38836464226092]
  We propose a Causal Semantic Generative model (CSG) based on a causal reasoning so that the two factors are modeled separately. We show that CSG can identify the semantic factor by fitting training data, and this semantic-identification guarantees the boundedness of OOD generalization error.
  arXiv  Detail & Related papers  (2020-11-03T13:16:05Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.