SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization
Computation and LanguageArtificial Intelligence
Summary
The authors address the problem of converting informal math statements into formal code for proof tools like Lean, noting that current methods can wrongly accept or reject statements. They introduce SA-Pass, a new way to check if generated formal statements truly match the intended meaning using helper statements called shadows. They test this method on ShadowBench, a collection of 178 advanced math problems in Lean 4, showing some success but also room for improvement. Their method closely matches expert judgments when deciding if a statement is correct.
Authors
Hojae Han, Jongyoon Kim, Sanghyuk Park, Dongwook Cheon, Myungjae Jeon, Sunjong Choi, Soonho Kong, Wonseok Heo, Seung-won Hwang, Donghoon Hyeon
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.