Deep network guided proof search
From MaRDI portal
Abstract: Deep learning techniques lie at the heart of several significant AI advances in recent years including object recognition and detection, image captioning, machine translation, speech recognition and synthesis, and playing the game of Go. Automated first-order theorem provers can aid in the formalization and verification of mathematical theorems and play a crucial role in program analysis, theory reasoning, security, interpolation, and system verification. Here we suggest deep learning based guidance in the proof search of the theorem prover E. We train and compare several deep neural network models on the traces of existing ATP proofs of Mizar statements and use them to select processed clauses during proof search. We give experimental evidence that with a hybrid, two-phase approach, deep learning based guidance can significantly reduce the average number of proof search steps while increasing the number of theorems proved. Using a few proof guidance strategies that leverage deep neural networks, we have found first-order proofs of 7.36% of the first-order logic translations of the Mizar Mathematical Library theorems that did not previously have ATP generated proofs. This increases the ratio of statements in the corpus with ATP generated proofs from 56% to 59%.
Recommendations
Cites work
Cited in
(33)- The role of the Mizar mathematical library for interactive proof development in Mizar
- Machine learning guidance for connection tableaux
- Towards the automatic mathematician
- Improving ENIGMA-style clause selection while learning from history
- Guiding an automated theorem prover with neural rewriting
- Improving stateful premise selection with transformers
- Towards finding longer proofs
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
- The role of entropy in guiding a connection prover
- A neurally-guided, parallel theorem prover
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- Deepalgebra -- an outline of a program
- On the proof complexity of deep inference
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
- Deep Proof Search in MELL
- Theorem proving in large formal mathematics as an emerging AI field
- Property invariant embedding for automated reasoning
- Prolog Technology Reinforcement Learning Prover
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- A formal proof of the expressiveness of deep learning
- A formal proof of the expressiveness of deep learning
- Automated proof synthesis for the minimal propositional logic with deep neural networks
- Proof Guidance in PVS with Sequential Pattern Mining
- Lemmas: generation, selection, application
- Synergies between machine learning and reasoning -- an introduction by the Kay R. Amel group
- Invariant neural architecture for learning term synthesis in instantiation proving
- Efficient neural clause-selection reinforcement
- Deep reinforcement learning for synthesizing functions in higher-order logic
- Learning guided automated reasoning: a brief survey
- ATWGNNS: graph simplified representation and learning of logical formula for premise selection
- Fast and slow enigmas and parental guidance
- Vampire with a brain is a good ITP hammer
- Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
Describes a project that uses
Uses Software
This page was built for publication: Deep network guided proof search
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4645728)
