Compiling is not the same as being right
Compile rate counts a formalization as correct when its Lean code type-checks. ShadowBench's checkers test whether the statement actually says what the problem says. Here the two are compared on every output: 41 systems × 178 problems.
Where every system lands
If compile rate were a good proxy, every point would sit on the diagonal. Click a point for details.
Every output, system by system
Each bar is the system's 178 problems. Systems with no compiled and no aligned output are left out.
Compiles and aligned (SA-PASS)
Compiles, misaligned (false positive)
Aligned, does not compile (false negative)
Aligned, compile timed out
Neither
How this is counted
- Compiles
- The standalone Lean compile passes (a
sorryis rejected), as in the leaderboard's Compile rate. - Aligned
- Every forward and backward checker passes, whether or not the standalone compile did. Against the paper's expert review of compile-passed outputs, the checkers reach precision 1.000 and recall 0.930: they never accept a misaligned statement, and miss 3 of the 43 aligned ones (auxiliary declarations named differently from the reference).
- False positive
- Compiles but fails at least one checker: compile rate counts it, SA-PASS does not.
- False negative
- Passes every checker but does not compile, usually a proof left as
sorryor a broken proof under a correct statement. Outputs that only hit the evaluator's compile time limit are shown separately. - Source
- Per-problem evaluator records for all 41 leaderboard rows (
data/compile_confusion.json); the counts reproduce every row's published Compile rate and SA-PASS.