Theorem Proving on PISA 2021-10-22 (test)
57Success RateThor
Evaluation Results
| Method | Links | |
|---|---|---|
| Thor2022.05 | 57 | |
| Language model ∪ Sledgehammer2022.05 | 48.8 | |
| Language modelparameters=700M, sampling temperature=1.2, search strategy=best-first search2022.05 | 39 | |
| LISA2022.05 | 33.2 | |
| Sledgehammertimeout limit=30s, ATPs=E, SPASS, Vampire, Z3, CVC42022.05 | 25.7 |