ShadowBench

A benchmark for semantic alignment in Lean 4 autoformalization. SA-PASS checks whether generated code compiles and expresses the intended theorem.

Leaderboard

Loading paper results...

Submit code

Level

Include 0.0

Show

Area

Loading...

Metric definitions

Compile rate: Share of tasks whose generated Lean code compiles standalone.
SA-PASS (Soft): Mean forward and backward checker pass rate, averaged over all tasks. Non-compiling tasks score zero.
SA-PASS: Share of tasks that compile and pass every forward and backward checker.