Proof searching and prediction in HOL4 with evolutionary/heuristic and deep learning techniques
- PDF / 2,282,979 Bytes
- 22 Pages / 595.224 x 790.955 pts Page_size
- 51 Downloads / 148 Views
Proof searching and prediction in HOL4 with evolutionary/heuristic and deep learning techniques M. Saqib Nawaz1 · M. Zohaib Nawaz2,3 · Osman Hasan2 · Philippe Fournier-Viger1 · Meng Sun4
© Springer Science+Business Media, LLC, part of Springer Nature 2020
Abstract 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. Keywords HOL4 · Genetic algorithm · Simulated Annealing · LSTM · Proof searching · Proof learning · Fitness
1 Introduction Theorem proving is a popular formal verification method that is used for the analysis of both hardware and software systems. In theorem proving, the system that needs to be analyzed is first modeled and specified in an appropriate mathematical logic. Important/critical properties of the system are then verified using theorem provers [1] based on deductive reasoning. The initial objective of developing theorem provers was to enable mathematicians to prove theorems using computer programs within a sound environment. However, these mechanical tools have evolved in last two decades and now play a critical part in the modeling and reasoning about M. Saqib Nawaz and M. Zohaib Nawaz equally contributed to the paper. Philippe Fournier-Viger
[email protected]
Extended author information available on the last page of the article.
complex and large-scale systems, particularly safety-critical systems. Today, theorem provers are used in verification projects that range from compilers, operating syst
Data Loading...
