Formal Theorem Proving on miniF2F (val)
42.2Pass@1POETRY
Evaluation results
| Method | Links | |||
|---|---|---|---|---|
| POETRYenvironment=Isabelle2024.05 | 42.2 | — | — | |
| Thor + expert iterationenvironment=Isabelle2024.05 | 37.3 | — | — | |
| Thor + Magnushammerenvironment=Isabelle2024.05 | 36.9 | — | — | |
| θ_full (expert iterated on full curriculum)search width (d)=512, expansion factor (e)=8, parameters=774M2022.02 | 33.6 | 41.2 | 47.3 | |
| FMSCLenvironment=Lean2024.05 | 33.6 | — | — | |
| θ_mathlib (expert iterated on mathlib-train)search width (d)=512, expansion factor (e)=8, parameters=774M2022.02 | 31.3 | 38.3 | 44.1 | |
| θ₁ (value-function based search)search width (d)=512, expansion factor (e)=8, parameters=774M2022.02 | 28.5 | 35.5 | 41.2 | |
| θ1d (expansions)=512, e (samples per expansion)=8, objective=proofsize, search=best-first search2022.02 | 28.5 | 35.5 | — | |
| θ0d (expansions)=512, e (samples per expansion)=8, search=cumulative logprob priority best-first search2022.02 | 28.4 | 33.6 | — | |
| θ1 (outcome objective)d (expansions)=512, e (samples per expansion)=8, objective=outcome, search=best-first search2022.02 | 28.3 | 34.7 | — | |
| Thorenvironment=Isabelle2024.05 | 28.3 | — | — | |
| θ0 (MiniF2F setup)d (expansions)=128, e (samples per expansion)=16, search=cumulative logprob priority best-first search2022.02 | 27.6 | 31.8 | — | |
| PACTsearch width (d)=512, expansion factor (e)=82022.02 | 23.9 | 29.3 | — | |
| MiniF2Fd (expansions)=128, e (samples per expansion)=162022.02 | 23.9 | 29.3 | — | |
| PACTenvironment=Lean2024.05 | 23.9 | — | — |