We study the effectiveness of neural sequence models for premise selection in automated theorem proving, one of the main bottlenecks in the formalization of mathematics. We propose a two stage approach for this task that yields good results for the premise selection task on the Mizar corpus while avoiding the hand-engineered features of existing state-of-the-art models. To our knowledge, this is the first time deep learning has been applied to theorem proving on a large scale.
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
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)
It seems kind of strange that he never thought of using computer proof systems for checking whether his proofs were right in class, and that he took a pattern-matching approach rather than using any of the existing AI proof-deriving systems like https://arxiv.org/abs/1606.04442 or https://intelligence.org/2013/12/21/josef-urban-on-machine-l...
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.
Artificial intelligence (AI) researchers have been developing and refining large language models (LLMs) that exhibit remarkable capabilities across a variety of domains and tasks, challenging our understanding of learning and cognition.
Recent work has demonstrated substantial gains on many NLP tasks and benchmarks by pre-training on a large corpus of text followed by fine-tuning on a specific task.