Can deep networks be trained to prove theorems?

Question

Assume we have a large number of proofs in first order predicate calculus. Assume we also have the axioms, corollaries, and theorems in that area of mathematics in that form too.

Consider the each proposition that was proved and the body of existing theory surrounding that specific proposition as an example in a training set and a known good proof for the proposition as the associated labels. Now, consider a deep artificial network designed specifically to train on this example set, and the hyper-parameters set correctly to do so.

Is it possible to train a deep artificial network in such a way that the presentation of a new proposition and the existing theory surrounding it presented in first order predicate calculus at the input would produce a proof at the output?

(Of course, such proofs should then be be checked manually.)

If the proportion of good proofs resulting was sufficiently high, might it be possible to create a genetic algorithm that proposes propositions to the trained deep network thereby creating proofs?

Is that possible?

Would it be possible to use this kind of deep network design to solve the Collatz conjecture or the Riemann conjecture or at least rearrange patterns in a way that mathematicians are more able to arrive at a legitimate proof?

Answer 1

Existing production systems, developed over the last few decades, have the rules of inference coded into them. They are based on the vision of Leibniz that all classical logic can be encoded into symbolic language and processed mechanically. First order predicate logic was developed and a nomeclature was formalized.

Although the vision of automatic theorem proving was considerably challenged by the Gödel's two incompleteness theorems, Turing's completeness work and the development of an architecture to practically realize it by von Neumann revived the work toward automating the mechanical process of inference.

MIT's AI lab, during the time of Minsky, was alive with such efforts, but what they called the combinatory explosion showed that there was insufficient computing resource availability to search the space required to automatically prove arbitrary theorems of non-trivial complexity. Large parallel computers called connection machines and various schemes, using meta rules and heuristic approaches, were employed to overcome the combinatory explosion problem.

Artificial networks were introduced and the idea that they could rival production machines was trounced by the LISP community when first proposed. However, in the context of considerable success in increasing computing resources and the recent achievements in machine learning, many have begun to ask questions that had been shelved in the twentieth century.

We already know that artificial networks can learn arbitrary logical and algebraic functions, many of which are PAC Learnable.¹ Given the proper learning environment, learning logical inference is clearly something the cerebral cortex can do at its current point in evolution. Whether neural networks will reach that level of cognition is an open question many ask.

That mainstream AI and machine learning research is not focusing on artificial network acquisition of logical inference rules, largely because programming them into a system like DRools and other commonly used production systems seems the more rational approach does not mean it will always be. The question is whether there is a sufficient return on investment to do what may be interesting but certainly expensive, when other solutions already exist.

This question is similar to another Artificial Intelligence Stack Exchange question on how good AI is in math. One of the answers given there is applicable here.

It is important not to dismiss any approach in this period of time, since the recent interest in AI has not only reignited government spending but also commercial spending. This spending increases personnel, computing power, and incentive to overcome obstacles that might have been thought to be insurmountable previously.

---

Footnotes

[1] PAC Learning is a framework for determining the practical computability of learning algorithms given the features of the class of hypotheses that can be learned using the given model and the expected accuracy and confidence of the learning process.

Answer 2

Your idea may be feasible in general, but a neural network is probably the wrong high level tool to use to explore this problem.

A neural network's strength is in finding internal representations that allow for a highly nonlinear solution when mapping inputs to outputs. When we train a neural network, those mappings are learned statistically through repetition of examples. This tends to produce models that interpolate well when given data similar to training set, but that extrapolate badly.

Neural network models also lack context, such that if you used a generative model (e.g. an RNN trained on sequences that create valid or interesting proof) then it can easily produce statistically pleasing but meaningless rubbish.

What you will need is some organising principle that allows you to explore and confirm proofs in a combinatorial fashion. In fact something like your idea has already been done more than once, but I am not able to find a reference currently.

None of this stops you using a neural network within an AI that searches for proofs. There may be places within a maths AI where you need a good heuristic to guide searches for instance - e.g. in context X is sub-proof Y likely to be interesting or relevant. Assessing a likelihood score is something that a neural network can do as part of a broader AI scheme. That's similar to how neural networks are combined with reinforcement learning.

It may be possible to build your idea entirety out of neural networks in principle. After all, there are good reasons to suspect human reasoning works similarly using biological neurons (not proven that artificial ones can match this either way). However, the architecture of such a system is beyond any modern NN design or training setup. It definitely will not be a matter of just adding enough layers then feeding in data.

Answer 3

What We Know

According to a World Bank page, "Today, there are around 200 million higher education students in the world, up from 89 million in 1998." At least 1 in 100 have, as a mathematics requirement, had to develop a proof for a theorem, and live at least 40 years afterward.

Although there are at least 20 million neural nets that can prove a theorem, they fall short of examples that would answer this question in the affirmative. These neural networks are biological, not artificial, and they have mostly proven previously proven theorems, not the Collatz conjecture or the Riemann conjecture.

What Some Believe

Those who believe that deep Q-learning and attention based devices will be joined by other learning system designs until the faculties of the human brain are simulated and perhaps surpassed, would likely include theorem proving as one of those human capabilities. These would likely declare predicate logic and inference as just another complex cognitive function that will be achieved in artificial systems.

Those who believe that some capabilities are imbued into humans and are reserved capabilities, may declare predicate logic and inference as reserved to humans alone.

Current State of Progress

There are no academic articles indicating the ability to prove even the simplest proofs using predicate logic and inference. It is possible that a government or private enterprise has achieved some level of success in doing so, but such has not been disclosed.

The idea that artificial networks, if developed appreciably, could surpass production systems, AI systems that are based on productions or rules, in their areas of greatest effectiveness was proposed early in the development of AI. It was disputed then and disputed now, however the arguments are not mathematical, so there is no strong indication that it is impossible.

Certainly other cognitive aspects of human thought are important objectives of AI research. Dialog, automated education, planning, strategic analysis, and vehicle piloting are all aspects of higher thought that demand more than DQN and attention based network approaches can now deliver, but the research effort in these areas are appreciable and well funded.

Potential Approach

Research toward logical cognitive abilities should begin proofs already know, far simpler than the conjectures mentioned in the question. For example, it has been proven that the sum of two non-negative integers must be another non-negative integer. In predicate calculus, that can be represented as a character string.

$\forall a∈C, b∈C: s=a+b \implies s∈C$

It says that a and b being members of the set of counting numbers, that the s, defined as the sum of the two, must also be a member of the set of counting numbers. Its proof can also be represented as a sequence of character strings of first-order predicate calculus.

No Small Research Project

Such an example may seem simple to someone who has taken years of math courses and has constructed proofs. It is not simple for a child, and it is very difficult to get an artificial network to converge to a function that applies all the rules of logical inference and incorporates meta-rules for arriving at a proof for a formal system such as integer arithmetic.

Turing complete networks, such as RNNs, will certainly have advantages over MLPs (multilayer perceptrons). Attention-based networks may be a reasonable research option. There are others indicated in the references below.

A parallel computing platform would be needed for the research, since the input vector may be hundreds of Kbytes. The sizes of examples and how many would be needed is difficult to estimate without getting a year or two into the research process.

The definition of counting numbers, the plus sign, and the equals sign must first be defined, and those definitions and a number of axioms, postulates, lemmas, and corollaries must be part of the input example in the formal form like the proposal to be proved above, along with that proposal.

And that's the work to prepare only one example. You'd need thousands to train intuitive knowledge about the rules of inference into a deep network. (I chose the word INTUITIVE very deliberately for theoretical reasons that would take at least a hundred pages to explain well.)

This is no small project since the example data set must have at least a few thousand cases, and each case, though it may share some theory, must be set up so that the proposal is perfectly formed and the necessary body of theory is also presented in perfect form at the input for each training iteration.

My guess is that it would take a team of bright researchers with the appropriate understanding of deep networks, convergence, and predicate calculus about ten years to train a network to give viable proofs in response to simple mathematical proposals.

But It Would Be No Small Achievement

That may seem an absurd endeavor for some, but it would be the first time someone taught a computer how to be logical. It took nature just under the age of earth to teach logical inference to an organism, Socrates.

People assume that because a computer is made up of digital circuits that perform logic by design that computers are logical. Anyone who has been around software development for decades with the inclination to think deeper than hacking for fun or money knows differently. Even after careful programming, computers do not simulate logical inference and cannot correct their own programmed behavior for any arbitrary bug. In fact, most of software development today is bug fixing.

Simulating logical thought would be a major step toward simulating cognition and the wider array of human capabilities.

---

References

Learning to Compose Neural Networks for Question Answering Jacob Andreas, Marcus Rohrbach, Trevor Darrell, and Dan Klein UC, Berkeley 2016 https://arxiv.org/pdf/1601.01705.pdf

Learning multiple layers of representation Geoffrey E. Hinton Department of Computer Science, University of Toronto 2007 http://www.csri.utoronto.ca/~hinton/absps/ticsdraft.pdf

Neural Turing Machine (slideshow) Author: Alex Graves, Greg Wayne, Ivo Danihelka Presented By: Tinghui Wang (Steve) https://eecs.wsu.edu/~cook/aiseminar/papers/steve.pdf

Neural Turing Machines (paper) Alex Graves, Greg Wayne, Ivo Danihelka https://pdfs.semanticscholar.org/c112/6fbffd6b8547a44c58b192b36b08b18299de.pdf 2014

Reinforcement Learning, Neural Turing Machines Wojciech Zaremba, Ilya Sutskever ICLR conference paper https://arxiv.org/pdf/1505.00521.pdf?utm_content=buffer2aaa3&utm_medium=social&utm_source=twitter.com&utm_campaign=buffer 2016

Dynamic Neural Turing Machine with Continuous and Discrete Addressing Schemes Caglar Gulcehre1, Sarath Chandar1, Kyunghyun Cho2, Yoshua Bengio1 https://arxiv.org/pdf/1607.00036.pdf 2017

An On-Line Self-Constructing Neural Fuzzy, Inference Network and Its Applications Chia-Feng Juang and Chin-Teng Lin IEEE Transactions on Fuzzy Systems, v6, n1 1998 https://ir.nctu.edu.tw/bitstream/11536/32809/1/000072774800002.pdf

Gated Graph Sequence Neural Networks Yujia Li and Richard Zemel ICLR conference paper 2016 https://arxiv.org/pdf/1511.05493.pdf

Building Machines That Learn and Think Like People Brenden M. Lake, Tomer D. Ullman, Joshua B. Tenenbaum, and Samuel J. Gershman Behavioral and Brain Sciences 2016 https://arxiv.org/pdf/1604.00289.pdf

Context-Dependent Pre-Trained Deep Neural Networks for Large-Vocabulary Speech Recognition George E. Dahl, Dong Yu, Li Deng, and Alex Acero IEEE Transactions on Audio, Speach, and Language Processing 2012 https://s3.amazonaws.com/academia.edu.documents/34691735/dbn4lvcsr-transaslp.pdf?AWSAccessKeyId=AKIAIWOWYYGZ2Y53UL3A&Expires=1534211789&Signature=33QcFP0JGFeA%2FTsqjQZpXYrIGm8%3D&response-content-disposition=inline%3B%20filename%3DContext-Dependent_Pre-Trained_Deep_Neura.pdf

Embedding Entities and Relations for Learning and Inference in Knowledge Bases Bishan Yang1, Wen-tau Yih2, Xiaodong He2, Jianfeng Gao2, and Li Deng2 ICLR conference paper 2015 https://arxiv.org/pdf/1412.6575.pdf

A Fast Learning Algorithm for Deep Belief Nets Geoffrey E. Hinton, Simon Osindero, Yee-Whye Teh (communicated by Yann Le Cun) Neural Computation 18 2006 http://axon.cs.byu.edu/Dan/778/papers/Deep%20Networks/hinton1*.pdf

FINN: A Framework for Fast, Scalable Binarized Neural Network Inference Yaman Umuroglu, et al 2016 https://arxiv.org/pdf/1612.07119.pdf

From Machine Learning to Machine Reasoning Léon Bottou 2/8/2011 https://arxiv.org/pdf/1102.1808.pdf

Deep learning Yann LeCun1,2, Yoshua Bengio3 & Geoffrey Hinton4,5 Nature vol 521 2015 https://www.evl.uic.edu/creativecoding/courses/cs523/slides/week3/DeepLearning_LeCun.pdf

Answer 4

It's possible, but probably not a good idea.

Logical proof is one of the oldest areas of AI, and there are purpose-built techniques that don't need to be trained, and that are more reliable than a neural-network approach would be, since they don't rely on statistical reasoning, and instead use the mathematician's friend: deductive reasoning.

The main field is called "Automated Theorem Proving", and it's old enough that it's calcified a bit as a research area. There are not a lot of innovations, but some people still work on it.

The basic idea is that theorem proving is just classical or heuristic guided search: you start from a state consisting of a set of accepted premises. Then you apply any valid logical rule of inference to generate new premises that must also be true, expanding the set of knowledge that you have. Eventually, you can prove a desired premise, either through enumerative searches like breadth first search or iterative deepening, or through something like A* with a domain-specific heuristic. A lot of solvers also use just one logical rule (unification) because it's complete, and reduces the branching factor of the search.