Isn’t proof checking at least as hard as k-sat and therefore NP? Given that neural networks process in constant time, how would that be possible without approximation?
This is kind of amusing because NP problems, by definition, must have a polynomial-length certification to a given solution that can be run in polynomial time.
The word "certification" can be read as "proof" without loss of meaning.
What you're asking is slightly different: whether the proof-checking problem in logic is NP. I don't know enough math to know for sure, but assuming that any proof can be found in polynomial time by a non-deterministic Turing machine and that such a proof is polynomial in length, then yes, the proof-checking problem is in NP. Alas, I think that all of that is moot because Turing and Church's answer in the negative to the Entscheidungsproblem [1].
It would help your understanding and everyone else's if you separated the search problem for a proof from the verification problem of a proof. Something is NP when you can provide verification that runs in polynomial time. The lesser spoken about second condition is that the search problem must be solved in polynomial time by a non-deterministic Turing machine. Problems which don't meet the second condition are generally only of theoretical value.
This article isn't about using neural networks for proof checking, but just using them to assist with writing Lean programs in the same way that developers use co-pilot to write java code or whatever. It might just spit out boilerplate code for you, of which there still is a great deal in formal proofs.
The proof checking is still actually done with normal proof checking programs.
Neural networks process in constant time per input/output (token or whatever). But some prompts could produce more tokens.
As you increase the size of the window, doesn't the size of the NN have to increase? So if you want to just use an NN for this, the bigger the problem it can handle, the bigger the window, so the longer per token produced; but also the more tokens produced, so it's longer on that front as well. I don't know if that adds up to polynomial time or not.
Note well: I'm not disagreeing with your overall assertion. I don't know if NNs can do this; I'm inclined to think they can't. All I'm saying is that even NNs are not constant time in problem size.
Most k-sat problems are easy, or can be reduced to a smaller and easier version of k-sat. Neural networks might be able to write Lean or Coq to feed into a theorem prover.
A proof is basically a directed graph where nodes are propositions, and edges are deductive rules. One only needs to check that the starting nodes are axioms and that each edge is one of a finite set of deduction rules in the system. So the time to check a proof is linear in the number of edges.
