用‘影子命题’评估形式化是否语义对齐，提升数学定理自动形式化评测可靠性。
SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization
- 引入影子命题作为标准参照，通过正反向逻辑检验语义一致性。
- 在178道高阶数学题上，最优模型达11.2%语义对齐通过率。
- 与专家判断98.8%一致，适合评估大模型数学形式化能力。
自动形式化将非正式数学定理转化为证明助手（如Lean）可处理的代码。当前评测指标常误判类型正确但语义错误的陈述，或拒绝对应正确的不同表述。受Pass@$k$启发，本文提出SA-Pass（语义对齐通过率），通过辅助命题（即“影子”）来检验生成的形式化陈述：只有当陈述可编译、能推出所有影子（前向验证）、且其合取能被该陈述蕴含（后向验证）时才得分。我们构建了ShadowBench，一个基于Lean 4的完整自动形式化基准，包含178道从研究生到研究级的数学问题，覆盖八个领域。采用Claude Code（Opus 4.8）与Numina-Lean-Agent，最高达到61.8%编译率和11.2% SA-Pass通过率。六种代理配置下，SA-Pass与专家判断的二分类一致性达98.8%。该基准曾作为ICML 2026 AI4Math挑战赛第4赛道的评测基础。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。