Repository logo
 

Bayesian Optimisation for Heuristic Configuration in Automated Theorem Proving

Simple item page
dc.contributor.authorSłowik, Agnieszka
dc.contributor.authorMangla, Chaitanya
dc.contributor.authorJamnik, Mateja
dc.contributor.authorHolden, Sean
dc.contributor.authorPaulson, Lawrence
dc.contributor.orcidSłowik, Agnieszka [0000-0001-7113-4098]
dc.contributor.orcidMangla, Chaitanya [0000-0001-7600-1681]
dc.contributor.orcidJamnik, Mateja [0000-0003-2772-2532]
dc.contributor.orcidHolden, Sean [0000-0001-7979-1148]
dc.contributor.orcidPaulson, Lawrence [0000-0003-0288-4279]
dc.date.accessioned2020-07-03T23:30:25Z
dc.date.available2020-07-03T23:30:25Z
dc.date.issued2019
dc.description.abstract<jats:p>Modern theorem provers such as Vampire utilise premise selection algorithms to control the proof search explosion. Premise selection heuristics often employ an array of continuous and discrete parameters. The quality of recommended premises varies depending on the parameter assignment. In this work, we introduce a principled probabilistic framework for optimisation of a premise selection algorithm. We present results using Sumo Inference Engine (SInE) and the Archive of Formal Proofs (AFP) as a case study. Our approach can be used to optimise heuristics on large theories in minimum number of steps.</jats:p>
dc.identifier.doi10.17863/CAM.54680
dc.identifier.issn2398-7340
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/307591
dc.language.isoeng
dc.publisherEasyChair
dc.publisher.urlhttp://dx.doi.org/10.29007/q91g
dc.rightsAll rights reserved
dc.subject46 Information and Computing Sciences
dc.subject49 Mathematical Sciences
dc.subject4602 Artificial Intelligence
dc.titleBayesian Optimisation for Heuristic Configuration in Automated Theorem Proving
dc.typeConference Object
dcterms.dateAccepted2019-06-27
prism.publicationNameEPiC Series in Computing
pubs.conference-nameVampire 2018 and Vampire 2019. The 5th and 6th Vampire Workshops
pubs.funder-project-idEngineering and Physical Sciences Research Council (1788755)
pubs.funder-project-idEPSRC (2119928)
rioxxterms.licenseref.urihttp://www.rioxx.net/licenses/all-rights-reserved
rioxxterms.typeConference Paper/Proceeding/Abstract
rioxxterms.versionVoR
rioxxterms.versionofrecord10.29007/q91g

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
Bayesian_Optimisation_for_Heuristic_Configuration_in_Automated_Theorem_Proving.pdf
Size:
259.62 KB
Format:
Adobe Portable Document Format
Description:
Published version
Licence
http://www.rioxx.net/licenses/all-rights-reserved
Download
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
DepositLicenceAgreementv2.1.pdf
Size:
150.9 KB
Format:
Adobe Portable Document Format
Download

Collections

Cambridge University Research Outputs