Are search heuristics the main bottleneck for automated theorem provers?

Question

My understanding of most automated theorem provers (which is possibly an incorrect understanding!) is that they start with some premises stored as unprocessed statements, and repeatedly select one to "process", generating different consequences and substitutions. Because the total number of statements is so big, they rely on heuristics to determine which statements are most promising to focus on.

However, I'm under the impression that current theorem provers are weak compared to human mathematicians, and often fail to solve theorems which humans have already proved.

If there were a very strong search heuristic which often selected the very best statement at a given step, would provers reach a superhuman level? Or are there other major challenges here, like limitations in the rules they use to process each statement?

Answer 1

Automated theorem provers rely on the resolution algorithm because it is complete. This means that if a proof exists, the prover is guaranteed to find it. Resolution works as follows:

Say you want to prove $\Gamma\vdash \phi$, then set $\mathcal I_0 := \Gamma\cup\{\neg\phi\}$ as your initial set of clauses. The goal is to iteratively saturate all possible derivable clauses (using the resolution rule) until you reach a contradiction:

$$\mathcal I_0 \subset \mathcal I_1\subset\mathcal I_2\subset\ldots\subset\mathcal I_n$$ so that $\bot\in\mathcal I_n$. Then you can reconstruct a proof as a binary tree of depth $n$. The problem, as you already noted, is that the size of $\mathcal I_k$ grows extremely quickly, so it is nearly impossible to find proofs beyond a few steps.

In principle, a perfect heuristic technique would pick out (at most) $2^{n-1}$ pairs in $\mathcal I_0$, (at most) $2^{n-2}$ pairs in $\mathcal I_1$,... and one pair in $\mathcal I_{n-1}$ on which to apply the resolution rule.

If good heuristics (even far from perfect) existed, there would be no limit to what provers could do. The problem is that it's nearly impossible to give good heuristics for a resolution theorem prover.

Answer 2

I used to feel the same way. My dream was a computer that would give me the answers I wasn't able to reach because I wasn't smart enough. Now I no longer hope that such a thing is possible; in fact, maybe I'm happy with it.

Two observations. First: human reasoning works by "deepening", by "clarification"; a computer cannot see what is in your head, you have to explain it to it step by step; however, once you have succeeded, perhaps you no longer need the computer, because you have understood the subtleties of the problem and the problem disappears. Second: in the automation of the game of chess there is a function that evaluates a configuration (heuristic) and a search algorithm based on this heuristic; if the heuristic were "exact", the search would no longer be needed.

In addition, if the heuristics are computationally heavy, the search cannot expand significantly, thus there is a tradeoff between accuracy and computation time. Neural network-based heuristics are computationally heavy, and those are the ones you're probably interested in. There are ATPs based on neural networks, e. g. Enigma (by Jan Jakubův). At the CASC-J10 Enigma performed very well, but did not win; Enigma relies on the "classic" theorem prover E (by Stephan Schulz), which is based on the equational superposition calculus and uses a variant of the Given-Clause Algorithm, the DISCOUNT Loop.

Regarding the possibility of having a "good" heuristic, I have thought of an argument that might convince you of the impossibility of its existence. I define a heuristic as "good" if it finds a proof of $n$ steps in at most $q(n)$ attempts, where $q$ is a polynomial and is known. If I had "good" heuristics, I could solve NP problems in polynomial time: suppose an NP problem has a verification algorithm in at most $p(n)$ steps ($p$ polynomial and known); in that case I can decide in polynomial time the NP problem, because I have answer YES if the heuristic finds a solution in less than $q(p(n))$ attempts and answer NO if the heuristic does not find a solution in less than $q(p(n))$ attempts (the composition of two polynomials is a polynomial).