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.
Artificial Intelligence and Future 