Formal Theorem Proving on mathlib (val)
62.6Pass@1θ_mathlib (expert iterated on mathlib-train)
Evaluation results
| Method | Links | |||
|---|---|---|---|---|
| θ_mathlib (expert iterated on mathlib-train)search width (d)=512, expansion factor (e)=8, parameters=774M2022.02 | 62.6 | 70.7 | 75.8 | |
| θ_full (expert iterated on full curriculum)search width (d)=512, expansion factor (e)=8, parameters=774M2022.02 | 61.7 | 69.8 | 75.3 | |
| θ₁ (value-function based search)search width (d)=512, expansion factor (e)=8, parameters=774M2022.02 | 56.3 | 66.3 | 72 | |
| θ1d (expansions)=512, e (samples per expansion)=8, objective=proofsize, search=best-first search2022.02 | 56.3 | 66.3 | — | |
| θ1 (outcome objective)d (expansions)=512, e (samples per expansion)=8, objective=outcome, search=best-first search2022.02 | 55.6 | 65.9 | — | |
| θ0 (PACT setup)d (expansions)=512, e (samples per expansion)=16, search=cumulative logprob priority best-first search2022.02 | 48.5 | 57.6 | — | |
| PACTsearch width (d)=512, expansion factor (e)=82022.02 | 48.4 | — | — | |
| PACTd (expansions)=512, e (samples per expansion)=162022.02 | 48.4 | — | — | |
| θ0d (expansions)=512, e (samples per expansion)=8, search=cumulative logprob priority best-first search2022.02 | 46.7 | 57.5 | — |