SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization
SA-Pass (*Semantic Alignment Pass*), which tests formal statements using auxiliary statements called shadows that characterize the intended statement, is proposed, which achieves binary agreement with expert judgments.