papers AI Learner
The Github is limit! Click to go to the new site.

Towards Evolutionary Theorem Proving for Isabelle/HOL

2019-04-17
Yutaka Nagashima

Abstract

Mechanized theorem proving is becoming the basis of reliable systems programming and rigorous mathematics. Despite decades of progress in proof automation, writing mechanized proofs still requires engineers’ expertise and remains labor intensive. Recently, researchers have extracted heuristics of interactive proof development from existing large proof corpora using supervised learning. However, such existing proof corpora present only one way of proving conjectures, while there are often multiple equivalently effective ways to prove one conjecture. In this abstract, we identify challenges in discovering heuristics for automatic proof search and propose our novel approach to improve heuristics of automatic proof search in Isabelle/HOL using evolutionary computation.

Abstract (translated by Google)
URL

http://arxiv.org/abs/1904.08468

PDF

http://arxiv.org/pdf/1904.08468


Similar Posts

Comments