SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization

arXiv:2608.29270v1 Announce Type: cross Abstract: Autoformalization translates informal mathematical theorems into code for proof assistants such as Lean. A central challenge is that current evaluation metrics can accept type-correct but misaligned statements or reject correct statements written in a different formulation. Inspired by Pass@k, we propose SA-Pass (Semantic Alignment Pass), which tests formal statements using auxiliary statements called shadows that characterize the intended statement. A generated statement receives full credit only when it compiles, implies each shadow (forward check), and is implied by their conjunction (backward check). We instantiate SA-Pass in ShadowBench, a Lean 4 full autoformalization benchmark of 178 postgraduate- to research-level problems spanning eight mathematical areas. Claude Code (Opus 4.8) with Numina-Lean-Agent reaches 61.8% compile rate and 11.2% SA-Pass. Across outputs generated by six agentic configurations, SA-Pass achieves 98.8% binary agreement with expert judgments. An early version of ShadowBench served as the benchmark for Track 4 of the ICML 2026 AI4Math Challenge.

Related

• FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation
• XSearch: Explainable Code Search via Concept-to-Code Alignment
• LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving

Source: arXiv cs.AI | 2026-09-01