@inproceedings{han-etal-2026-shadowbench,
title = "{SHADOWBENCH}: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization",
author = "Han, Hojae and
Kim, Jongyoon and
Park, Sanghyeok and
Cheon, Dongwook and
Park, Yeachan and
Jeon, Myeong Jae and
Choe, SunJong and
Kong, Soonho and
Hur, Wonseok and
Hwang, Seung-Won and
Hyeon, Donghoon",
editor = "Lee, Hung-Yi and
Dev, Sunipa and
Li, Jessy and
Elliott, Desmond",
booktitle = "Proceedings of the 2026 Conference on Empirical Methods in Natural Language Processing",
month = oct,
year = "2026",
address = "Budapest, Hungary",
publisher = "Association for Computational Linguistics",
url = "https://aclanthology.org/2026.emnlp-main.2335/",
pages = "53031--53067",
ISBN = "979-8-89176-459-0",
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."
}<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="han-etal-2026-shadowbench">
<titleInfo>
<title>SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization</title>
</titleInfo>
<name type="personal">
<namePart type="given">Hojae</namePart>
<namePart type="family">Han</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Jongyoon</namePart>
<namePart type="family">Kim</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Sanghyeok</namePart>
<namePart type="family">Park</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Dongwook</namePart>
<namePart type="family">Cheon</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Yeachan</namePart>
<namePart type="family">Park</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Myeong</namePart>
<namePart type="given">Jae</namePart>
<namePart type="family">Jeon</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">SunJong</namePart>
<namePart type="family">Choe</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Soonho</namePart>
<namePart type="family">Kong</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Wonseok</namePart>
<namePart type="family">Hur</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Seung-Won</namePart>
<namePart type="family">Hwang</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Donghoon</namePart>
<namePart type="family">Hyeon</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<originInfo>
<dateIssued>2026-10</dateIssued>
</originInfo>
<typeOfResource>text</typeOfResource>
<relatedItem type="host">
<titleInfo>
<title>Proceedings of the 2026 Conference on Empirical Methods in Natural Language Processing</title>
</titleInfo>
<name type="personal">
<namePart type="given">Hung-Yi</namePart>
<namePart type="family">Lee</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Sunipa</namePart>
<namePart type="family">Dev</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Jessy</namePart>
<namePart type="family">Li</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Desmond</namePart>
<namePart type="family">Elliott</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<originInfo>
<publisher>Association for Computational Linguistics</publisher>
<place>
<placeTerm type="text">Budapest, Hungary</placeTerm>
</place>
</originInfo>
<genre authority="marcgt">conference publication</genre>
<identifier type="isbn">979-8-89176-459-0</identifier>
</relatedItem>
<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>
<identifier type="citekey">han-etal-2026-shadowbench</identifier>
<location>
<url>https://aclanthology.org/2026.emnlp-main.2335/</url>
</location>
<part>
<date>2026-10</date>
<extent unit="page">
<start>53031</start>
<end>53067</end>
</extent>
</part>
</mods>
</modsCollection>
%0 Conference Proceedings
%T SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization
%A Han, Hojae
%A Kim, Jongyoon
%A Park, Sanghyeok
%A Cheon, Dongwook
%A Park, Yeachan
%A Jeon, Myeong Jae
%A Choe, SunJong
%A Kong, Soonho
%A Hur, Wonseok
%A Hwang, Seung-Won
%A Hyeon, Donghoon
%Y Lee, Hung-Yi
%Y Dev, Sunipa
%Y Li, Jessy
%Y Elliott, Desmond
%S Proceedings of the 2026 Conference on Empirical Methods in Natural Language Processing
%D 2026
%8 October
%I Association for Computational Linguistics
%C Budapest, Hungary
%@ 979-8-89176-459-0
%F han-etal-2026-shadowbench
%X 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.
%U https://aclanthology.org/2026.emnlp-main.2335/
%P 53031-53067
Markdown (Informal)
[SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization](https://aclanthology.org/2026.emnlp-main.2335/) (Han et al., EMNLP 2026)
ACL
- Hojae Han, Jongyoon Kim, Sanghyeok Park, Dongwook Cheon, Yeachan Park, Myeong Jae Jeon, SunJong Choe, Soonho Kong, Wonseok Hur, Seung-Won Hwang, and Donghoon Hyeon. 2026. SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization. In Proceedings of the 2026 Conference on Empirical Methods in Natural Language Processing, pages 53031–53067, Budapest, Hungary. Association for Computational Linguistics.