Proof searching and prediction in HOL4 with evolutionary/heuristic and deep learning techniques

摘要

Interactive theorem provers (ITPs), also known as proof assistants, allow human users to write and verify formal proofs. The proof development process in ITPs can be a cumbersome and time-consuming activity due to manual user interactions. This makes proof guidance and proof automation the two most desired features for ITPs. In this paper, we first provide two evolutionary and heuristic-based proof searching approaches for the HOL4 proof assistant, where a genetic algorithm (GA) and simulated annealing (SA) is used to search and optimize the proofs in different HOL theories. In both approaches, random proof sequences are first generated from a population of frequently occurring HOL4 proof steps that are discovered with sequential pattern mining. Generated proof sequences are then evolved using GA operators (crossover and mutation) and by applying the annealing process of SA till their fitness match the fitness of the target proof sequences. Experiments were done to compare the performance of SA with that of GA. Results have shown that the two proof searching approaches can be used to efficiently evolve the random sequences to obtain the target sequences. However, these approaches lack the ability to learn the proof process, that is important for the prediction of new proof sequences. For this purpose, we propose to use a deep learning technique known as long short-term memory (LSTM). LSTM is trained on various HOL4 theories for proof learning and prediction. Experimental results suggest that combining evolutionary/heuristic and deep learning techniques with proof assistants can greatly facilitate proof finding/optimization and proof prediction.