ShadowBench: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization
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.
Results at a glance
What SA-PASS checks
A metric that only checks whether a formalization compiles can be fooled by a statement that type-checks but proves something else, and a metric that requires an exact restatement penalizes a correct formalization written a different (but equivalent) way. SA-PASS instead compares a generated statement against a small set of shadow statements -- alternate, independently written characterizations of the same theorem -- and requires the generated statement to compile, to imply every shadow (forward check), and to be implied by their conjunction (backward check). Passing all three is treated as evidence the statement captures the same mathematical content as the source theorem, not just its surface shape.
Citation
@misc{han2026shadowbenchreliableautomaticevaluation,
title={SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization},
author={Hojae Han and Jongyoon Kim and Sanghyeok Park and Dongwook Cheon and Yeachan Park and Myeong Jae Jeon and Sunjong Choe and Soonho Kong and Wonseok Hur and Seung-won Hwang and Donghoon Hyeon},
year={2026},
eprint={2608.29270},
archivePrefix={arXiv},
primaryClass={cs.CL},
url={https://arxiv.org/abs/2608.29270},
}