Robustness of Autoformalization as a New Evaluation Axis
Highlights of This Issue
The main theme of this issue is that "evaluation of autoformalization is moving from correctness to robustness and faithfulness." The 56% misformalization rate revealed by the ProofNet-Verified audit in the previous issue is now symmetrically evidenced on the model side: Evaluating the Robustness of Proof Autoformalization in Lean 4 is the first systematic measurement of proof autoformalization performance under perturbations, finding that models commonly exhibit "silent regression"—quietly reverting counterfactual edits to the original rather than faithfully reflecting them, with an average faithfulness rate of only 6.3% across seven models on numeric/symbolic edits. The faithfulness gap between benchmarks and models is becoming a sharper bottleneck than solving rates.
Dataset construction continues to scale up, with Lean-GAP providing formalized statements for graduate-level algebra problems with mathematician sign-off via two-stage human review. On the saturation ATP side, Teaching Vampire New Tricks is the first to evaluate neural clause selection at combinatorial scale. On the tooling front, Lean 4.35.0-rc1 brings a batch of updates aimed at proof automation.
Community and Developments
- Tool Updates: Lean 4.35.0-rc1 introduces
[grind hom]/[grind hom_pred]homomorphism simplification attributes,bv_decide_pushincremental preprocessing, and deprecatesmvcgenin favor ofvcgen—these automation tactics can serve as stronger baselines for neural-guided proof search. - Benchmark Audit: Ground False: Dissecting Errors in Formal Mathematics Benchmarks (ICML 2026 AI4Math workshop) formally publishes the ProofNet-Verified audit from the previous issue and applies the same pipeline to six benchmarks, showing unfaithfulness rates ranging from 4.8% to 60%, primarily depending on curation processes.
- Trust Discussion: Don't trust Lean4 alone argues that when AI produces proofs in bulk, the Lean kernel itself becomes a security/trust bottleneck, calling for peer review of AI-solved results.
Open Questions
- The "separable evaluation of benchmark defects and system defects" proposed in the previous issue gains new evidence: Ground False applies the same audit pipeline to six benchmarks, showing unfaithfulness rates spanning an order of magnitude (4.8%–60%) and primarily depending on curation processes. Can "curation quality" itself be standardized as a mandatory reported metric at benchmark release, allowing downstream evaluation to be calibrated?
- RobustPABench shows models have an average faithfulness rate of only 6.3% on local counterfactual edits, with even Gemini-3.1-Pro regressing 95.9% on numeric edits—is "silent regression" homologous to the "sycophancy" phenomenon revealed by FaithformBench in Issue 4? Can a unified perturbation-faithfulness framework characterize both failure modes?
- Robustness evaluation is currently a post-hoc metric—can it be used as a training objective (e.g., RL reward) rather than just an evaluation axis, combined with the Process-Verified RL approach from Issue 4 that uses Lean feedback as dense rewards, so that models learn to faithfully reflect edits rather than regress during training?
Papers in this issue
All existing proof autoformalizers in Lean 4 are unstable under paraphrasing and silently revert over 90% of counterfactual proof-level edits, undermining their reliability for verifying natural-language mathematics.
Editor's noteThe first systematic evaluation of proof autoformalization robustness, categorizing perturbations into global (style rewriting) and local (counterfactual edits), measuring correctness stability and faithfulness respectively. Compared to FaithformBench in Issue 4 (which perturbs reasoning steps to evaluate CoT autoformalization faithfulness), its increment lies in focusing on proof-level counterfactual edits and quantifying the 'silent regression' failure mode—models quietly revert local edits to the original rather than faithfully reflecting them, with an average faithfulness rate of only 6.3% across seven models on numeric/symbolic edits. Benchmarks and code are public, adding a robustness dimension beyond correctness to autoformalization evaluation.
LEAN-GAP provides 430 graduate algebra problems, showing LLMs achieve high syntactic elaboration but low semantic fidelity, making human verification the bottleneck in autoformalization.
Editor's noteA formalized dataset of 430 graduate-level algebra problems from Dummit & Foote's 'Abstract Algebra', with two-stage human review ensuring every statement has mathematician sign-off. Compared to StochBench (stochastic processes) and AxQM (quantum mechanics) in Issue 5, its increment lies in focusing on the algebra domain and systematically analyzing autoformalization difficulties such as 'answer-embedded formalization', also documenting cases where AI as a second reader found errors in the textbook's original problems. Currently about 20% complete, semantic evaluation relies on LLM judges, so model comparisons should be treated as relative signals.
Neural clause selection consistently boosts VAMPIRE within domains but fails to transfer across datasets, though multi-dataset training recovers most performance.
Editor's noteThe first systematic evaluation of neural clause selection in saturation ATP (Vampire) across multiple ITP-derived benchmarks (Mizar40, Isabelle, CoqHammer), examining cross-domain transfer and combinatorial strategy effects. Key findings: cross-benchmark transfer fails (even below the unguided default strategy) but joint training recovers performance, and neural guidance shows diminishing marginal returns at combinatorial scale—this is the first work evaluating neural guidance at the combinatorial level. Directly valuable for designing generalizable neural guidance systems, but the focus is on ATP rather than the Lean 4 ecosystem.
Trivet combines LLMs with the Lean theorem prover to validate all 74 valid LLVM transformations and refute 73 of 74 invalid ones, overcoming Alive2's scalability, symbolic bitwidth, and loop limitations.
Editor's noteThe first automatic translation verification framework combining LLMs with Lean for LLVM transformations. The core increment is using deterministically generated proof scaffolds to decompose verification into case analysis of UB trigger conditions, leaving only transformation-specific proof obligations to the LLM, and using counterexample branches to convert candidate counterexamples into machine-verified non-refinement proofs. Compared to Alive2's SMT bounded verification supporting symbolic bit-widths and unbounded loop induction, it reduces proof time by 75.9% compared to manual proof engineering. The focus leans toward compiler verification rather than mathematics, but its scaffolding mechanism is a reference for designing agentic proof search.
Stellar Colosseum, a five-stage adversarial many-agent inference harness, achieves 71% on TCS-Bench and proves five open problems by structuring long-horizon research into critique-preserving, tree-aggregated stages.
Editor's noteA model-agnostic multi-agent framework for long-horizon mathematics and TCS research, explicitly dividing the research process into strategy exploration, readiness gating, decomposition, parallel proof construction, and global verification, preserving criticism in aggregation rather than simple voting. Compared to Goedel-Architect in Issue 2 (blueprint generation and refinement), its increment lies in treating strategy exploration and readiness gating as independent stages. However, evaluation is based on natural language proofs and TCS-Bench, not involving Lean 4 formalization, and some results rely on undisclosed models, limiting reproducibility.
