Name
Title | ||
|---|---|---|
Bayesian Optimisation For Premise Selection In Automated Theorem Proving (Student Abstract) |
Abstract | ||
|---|---|---|
Modern theorem provers utilise a wide array of heuristics to control the search space explosion, thereby requiring optimisation of a large set of parameters. An exhaustive search in this multi-dimensional parameter space is intractable in most cases, yet the performance of the provers is highly dependent on the parameter assignment. In this work, we introduce a principled probabilistic framework for heuristic optimisation in theorem provers. We present results using a heuristic for premise selection and the Archive of Formal Proofs (AFP) as a case study. |
Year | DOI | Venue |
|---|---|---|
2020 | 10.1609/AAAI.V34I10.7232 | AAAI |
DocType | Volume | Issue |
Conference | 34 | 10 |
ISSN | Citations | PageRank |
2159-5399 | 0 | 0.34 |
References | Authors | |
0 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Agnieszka Slowik | 1 | 0 | 0.68 |
| Chaitanya Mangla | 2 | 0 | 0.68 |
| Mateja Jamnik | 3 | 158 | 30.79 |
| Sean B. Holden | 4 | 195 | 30.15 |
| Lawrence C. Paulson | 5 | 0 | 1.35 |