Can neural networks be used to prove conjectures?

Question

Imagine I have a list (in a computer-readable form) of all problems (or statements) and proofs that math relies on.

Could I train a neural network in such a way that, for example, I enter a problem and it generates a proof for it?

Of course, those proofs then needed to be checked manually, but maybe the network then creates proofs from combinations of older proofs for problems yet unsolved.

Is that possible?

Would it be possible, for example, to solve the Collatz-conjecture or the Riemann-conjecture with this type of network? Or, if not solve, but maybe rearrange patterns in a way that mathematicians are able to use a new "proof method" to make a real proof?

Answer 1

Not in such straight forward way as described, but neural networks are successfully applied to guide the search of proof. There are automated theorem provers. What they do look roughly like this:

1. Get the mathematical statement

2. Apply one of the known mathematical equivalence transformations (theorems, axioms, etc)

3. Check, if the resulting statement is trivially true. Then our sequence of transformations is the proof (since they all were equivalence transformations). Else, goto 2.

The tricky part here is to choose which transformation to apply at step 2. A neural network can be trained to predict function like

Statement, Transformation --> usefulness of that transformation to that statement

Then, during the search, we can apply such transformation, that neural network considers the most useful. Also, proving a theorem can be considered game, where axioms are the rules, and when you've reached the proof you win. In this form, Reinforcement Learning agents can be applied to prove theorems (this is also successfully done).

Here are papers that do similar things:

• Generating Correctness Proofs with Neural Networks (Proverbot9001)

• A Learning Environment for Theorem Proving (GamePad)

• Learning to Prove with Tactics (TacticToe)

• Learning to Prove Theorems via Interacting with Proof Assistants (CoqGym)

• HOList: An Environment for Machine Learning of Higher-Order Theorem Proving

• Reinforcement Learning of Theorem Proving (rlCoP)

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

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.

Answer 4

I've published an article with the corresponding new method based on the generative grammars of first-order theories:

Thoughts on generative grammars and their use in automated theorem proving based on neural networks

This approach allows not to use previous data but to generate it as much as it's needed in machine learning. In the article, you may find necessary theory on logic, grammars, and neural networks. You'll also find examples of the python-functions generating proofs literally. I've added a grammar for the propositional logic that can be naturally enlarged to the "real" cases of first-order theories (say, group or number theory).