# SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization

Preprint · Hojae Han, Jongyoon Kim, Sanghyeok Park, Dongwook Cheon, Yeachan Park, Myeong Jae Jeon, Sunjong Choe, Soonho Kong, Wonseok Hur, Seung-won Hwang, Donghoon Hyeon

- Archive id: arxiv:2608.29270
- Published: 2026-08-29
- Venue: The 2026 Conference on Empirical Methods in Natural Language Processing
- arXiv: https://arxiv.org/abs/2608.29270
- Citations: 0
- Source URL: https://arxiv.org/abs/2608.29270
- PDF: https://arxiv.org/pdf/2608.29270
- Provenance: arxiv

## 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.

_Abstract reproduced under CC0-1.0 (arXiv descriptive metadata)._

Topics: [AI for Mathematics & Formal Proof](https://space-kitty.com/topics/ai-mathematics)

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.