Skip to content
The methodOpen data
Back to the collection

Deep Network Guided Proof Search

Sarah Loos, Geoffrey Irving, Christian Szegedy, Cezary Kaliszyk

2017 · arXiv

MathematicsMachine learningPsychology
Read the paper
HN score
0
Mentions
3
Readers
3
Months
3
What’s in a score?

From the 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%.

Metadata: arXiv. Abstracts retain their original authors’ rights.

In the conversation

Original HN comments, with labels from simple text rules. A label describes the whole comment and may miss context or irony. Read the discussion to make up your own mind. About the labels

3 selected excerpts · 3 total mentions

skissane
Neutral mention · rule
> As soon as you need reliable outcomes, such as certainty whether an erroneous state can arise in a program, whether a proof for a mathematical conjecture exists, or whether a counterexample exists, exhaustive search is often necessary. Proof checking requires 100% reliability. But if you are searching the space of all possible proofs for a valid one, that process does not require 100% reliability. On the contrary, automated theorem provers rely on heuristics to guide their exploration of that space, none of which work 100% of the time. "Exhaustive search" is an infeasible strategy, because the search space is just too large. Finding proofs is the really hard part…
Read the full comment
(NP-hard), and the part which most stands to benefit from "AI" techniques – checking their validity is a lot easier (polynomial time). "New AI" deep-learning techniques can be used to augment automated theorem provers, by giving them guidance on which areas of the search space to target – see for example https://arxiv.org/abs/1701.06972 – that produced a seemingly modest improvement (3 percentage points) – but keep in mind how hard the problem is, a 3 percentage point improvement on a very hard problem can actually be a big deal – plus I don't know if any more recent research has improved on that.
Original comment Good Old Fashioned AI is dead, long live New-Fangled AI
popinman322
Neutral mention · rule
IIRC these nets don't actually build a knowledge base (though I may be wrong, it's been a while). They're still functioning in lossy continuous space. This is probably fine with a low number of symbols and relations, but once you get to the level of a neural theorem prover you need to properly handle symbol binding. If I'm working with integers and integer-valued variables, how do I represent the variables? How do I represent the operations? This gets more complex once you leave a closed domain, where all the operations and variables are defined up front, and you enter an open domain like theorem proving. There are definitely good applications for small-scale symbolic…
Read the full comment
work; you could possibly improve efficiency of warehouse robots, for example. Highly (pro/ef)ficient neural theorem provers would be amazingly useful, though. Not to mention reasoning over medical knowledge given only the source documents (journal articles). In either of the two domains above you need to extract symbols and relations directly from text. I think symbol-identification and relation-identification, for unstructured documents, can likely be done with some of the state-of-the-art models (particularly thinking of Diffbot[0] here). So use something like Diffbot to identify symbols+relations, then... how do you represent them? Once you have the symbols you can use traditional reasoning tech on them, but it's going to be extremely slow for any reasonable unit of work. Which is exactly why you'd want to piggyback off of neural work. --- Some work has been done on neural theorem proving (NTP). See [1][2]. There are justifications for replacing the existing graph search vs. providing better search heuristics, but I'm fuzzy on the details. Either approach should be eligible for reinforcement learning. [0]: https://www.diffbot.com/products/natural-language/ [1]: https://arxiv.org/abs/1705.11040 [2]: https://arxiv.org/abs/1606.04442 (This is just for premise selection; it doesn't replace the prover machinery) [3]: https://arxiv.org/abs/1701.06972 (More guided search)
Original comment Neurosymbolic AI – Combining neural nets and symbolic AI

Keep following the thread.

More in Mathematics

More from the same topics.

1994arXiv

On proof and progress in mathematics

William P. Thurston

In response to Jaffe and Quinn [math.HO/9307227], the author discusses forms of progress in mathematics that are not captured by formal proofs of theorems, especially in his own work in the theory of foliations and geometrization of 3-manifolds and dynamical systems.

Mathematics
29 mentions21 months
9HN score