Formal Theorem Proving on miniF2F full n=244
40.6Total Solve RateVERITAS Two-Phase
Evaluation results
| Method | Links | |||||||
|---|---|---|---|---|---|---|---|---|
| VERITAS Two-PhaseLean/thm=27, API ($)=1502026.06 | 40.6 | 57.9 | 49.3 | 20 | 13.3 | 5.3 | 30 | |
| Best-of-5 SonnetLean/thm=5, API ($)=352026.06 | 36.9 | 53.4 | 44.8 | 17.8 | 13.3 | 10.5 | 10 | |
| Best-of-1 SonnetLean/thm=1, API ($)=72026.06 | 29.1 | — | — | — | — | — | — | |
| Portfolio (heuristic)Lean/thm=1, API ($)=<12026.06 | 26.2 | 30.7 | 46.3 | 11.1 | 6.7 | 0 | 0 |