Deep Network-based Automated Theorem Prover

This is a review of the paper — “Deep network guided proof search”. arXiv preprint arXiv:1701.06972, as given in reference [1].

— Automated first-order theorem provers (ATP) can be used to prove mathematical theorems and these can also be used in applications such as program analysis, theory exploration, and reasoning.

— Higher-order logic, Naive Bayes, techniques are used in prior works to improve search.

— This article provides deep learning-based guidance in proofs of theorems provers inside an ATP.

— Modern ATP does not perform well in general when many facts are present.

— AI can help select lemmas to be tested on ATP for better results and time complexity.

— Mentioned in paper that ATP can find proofs upto 20 human steps [in Mizar Mathematical Library proof sets wherein proofs upto 100 steps are provided]

— Does not rely on Tableau Methods for ATP.

— Experiments on Mizar Mathematical Library converted to First Order Logic (FOL).

— Learns syntax tree of proof clause.

— First-order logic theorem prover E preprocesses the FOL into CNF to do proof search.

— CNF form if the formula is the conjunction of clauses and each clause is a disjunction of literals. A literal is a predicate term.

— Clause Selection Heuristic is the main thing driving this work.

— Unprocessed clauses: those clauses that are not processed.

— Once a clause is viewed its consequences are generated, each of these is added to the unprocessed clause list.

— The viewed clause is shifted to the processed clause list.

— The algorithm used to view clauses determines how long would it take to find the proof.

— ATP uses a heuristic to select a clause search heuristic and sets other parameters and decides the next step.

— As specified in the paper the best-performing heuristics were selected by targeting various criteria in a round-robin manner.

— Other heuristics can be FIFO on shortest unprocessed clause.

— Hybrid approach combining the above two heuristics produced better results.

— Here, a machine learning-based optimal clause selection heuristic given time and computing powers, is proposed in this paper.

— Mizar Mathematical Library (MML) is a collection of formularized proofs

— MML has been translated to FOL (the number goes up to 57,882 Mizar theorems), and this makes it best choice for experiments in CS and ML.

— The FOL proofs used by authors are based out of work by Kaliszyk & Urban (2015).

— Around 91000 proofs were used to train and learn the ATP.

— Network architecture was taken by premise selection work by Alemi et al. (2016).

— Model takes — (a) negated conjecture in CNF form, and, (b) unprocessed clause in CNF form.

— Convert the above two in fixed-sized vectors using an embedding network and combine the two using a combining network and generate a score to select a clause. The same architecture but different weights are used for this. This was tried using (a) a CNN (b) WaveNet, and (c) a RNN.

— Loss is computed towards 1 if the clause selected is used in proof, else it is set to be near 0.

— Combiner use one 1024-unit hidden layer.

— The input layer converts each symbol to an embedding vector of dimension 1024.

— Ranks are produced for the clauses in addition to the given clause selection methods mentioned above.

— Rankings are produced for clauses to be used in ATP.

— Harder and deeper theorems were proved with improvements in strategy with this approach.

— Due to the time taken by neural networks, a hybrid approach is better, for example, one where a combinatorial search follows a deep neural-based layer with a hand-crafted clause selection phase.

— However, the computational time of the method proposed here is high as compared to prior works.

— Experimental proofs are provided by authors that the two-phase process reduces the time to prove a theorem by reducing the steps and hence increasing the number of theorems proved in the given time.

— Results increase the number of theorems with ATP proofs.

References

Loos, S., Irving, G., Szegedy, C., & Kaliszyk, C. (2017). Deep network guided proof search. arXiv preprint arXiv:1701.06972.

Alexander A Alemi, Francois Chollet, Geoffrey Irving, Niklas Een, Christian Szegedy, and Josef Urban. Deepmath-deep sequence models for premise selection. In Advances in Neural Information Processing Systems, pp. 2235–2243, 2016.

Cezary Kaliszyk and Josef Urban. MizAR 40 for Mizar 40. J. Autom. Reasoning, 55(3): 245–256, 2015a. doi: 10.1007/s10817–015–9330–8. URL http://dx.doi.org/10.1007/ s10817–015–9330–8.