arXiv:1909.09137
Bayesian Optimisation with Gaussian Processes for Premise Selection
원문 초록
Heuristics in theorem provers are often parameterised. Modern theorem provers such as Vampire 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 probablistic framework for heuristics optimisation in theorem provers. We present results using a heuristic for premise selection and The Archive of Formal Proofs (AFP) as a case study.
함께 살펴볼 논문
공통 태그를 근거로 연결했습니다. 실제 인용 관계나 논문의 우수성을 뜻하지 않습니다.
Nonmyopic Global Optimisation via Approximate Dynamic Programming
Residual Deep Gaussian Processes on Manifolds
Spectral Representations for Accurate Causal Uncertainty Quantification with Gaussian Processes
Multi-view Bayesian optimisation in reduced dimension for engineering design
Dimensionality Reduction Techniques for Global Bayesian Optimisation
Statistical Machine Learning for Astronomy -- A Textbook
토론
이 논문과 연결된 포럼 글이 아직 없습니다.