My question can be read on many levels and so I welcome answers to any reading. The general question is:

What is the computational complexity of verifying a proof?

One way of looking at a computational complexity class (for decision problems) is that is is a set of theories (a theory being a set of theorems) whose theorems can be proven with the resources allotted to the class (any computation of a yes/no by a TM can be viewed as a proof that the answer is yes/no).

Some complexity classes are defined using provability (at least NP), that is, given a proof (a witness or certificate), it can be checked (verified) by some other (strictly smaller) class's machine.

In most proofs of NP-completeness, showing that a problem is actually a member of NP usually is just showing that there is a witness fr any instance that can be verified by a P machine (or, better said, that the verification problem is a member of P).

My question comes from my observation that these verification problems (the one's I remember) seem almost always (I can't remember any others) to be very linear (yes, I'm confounding computational complexity with algorithmic running time).

Are there some verification algorithms that are (provably) polynomial of a higher degree than 1? Or even super-polynomial for EXP, EXP2, etc?

Or in general is the complexity of verification, applied to -any- complexity class, always linear (in P or some smaller class)?

(even though my question is about complexity classes, I am also curious about real life proofs where people may rely on lemmas that involve, for example, proving the existence of a particular intersection of hyperplanes (presumably (!) in some subclass of P)

  • $\begingroup$ I am a bit confused. How are proofs given to you? Are we talking about formal proofs? A formal proof would be a sequence of sentences, and to verify whether such a sequence is a proof or not is just as hard as verifying whether a sentence is an axiom of the theory in which the proof takes place (and it is decidable iff the theory is computably enumerable). Perhaps you mean something else? $\endgroup$ – Andrés E. Caicedo Jan 3 '11 at 0:18
  • $\begingroup$ @Andres: Thanks for clarifying in asking for clarification. I am mixing domain vocabularies. Even though I am talking about proofs and verifications, I am considering the mechanics not of sequence of applications of rules of inference, but rather sequences of TM rules. And I'm assuming that for a given TM only a finite set of rules. Also, the proof is not given in full, but as a certificate/witness that can be inputted to another TM (of presumably lower complexity) to verify/confirm the truth of the answer of the higher complexity problem. $\endgroup$ – Mitch Jan 3 '11 at 0:34

I will answer your questions in order:

1- The complexity of a proof is the length of the proof. Remember that a proof (witness or certificate) is simply a branch of a Turing machine on some given input. This corresponds to a solution to some problem. For example consider SAT, the input to the machine will be a SAT instance (i.e. a propositional formula), and the proof will be an assignment of 0-1 values to the variables. Some problems can have exponentially long proofs, like PSPACE-complete problems, or proofs of non-existence like in coNP.

2- The second question is not very clear for me. I think you are asking if there can be proofs with super-polynomial lenghts? Like I've said, PSPACE-complete and coNP languages have exponentially long proofs.

3- I don't understand what you mean with linear. You mean that the verifiers are always P machines? Not necessarily, for example, NEXP is also called Exponential-NP. This is because the proofs are verified by deterministic machines that run in exponential time.

In real life, you can consider that all the lines of text that a proof have, can be stated in formal logic, and this can be interpreted by a machine. A field in computational complexity that studies formal proofs is proof complexity. For example, you are given a statement written in some theory (e.g. Peano's arithmetic). Then, you calculated what are the necessary resources a machine needs to verify that the statement is true or not.

  • $\begingroup$ re 1- yes, under certain circumstances, a proof is certainly just the trace through a TM. But your example points to a diferent circumstance, SAT is an NP-complete problem, but as often presented, to show it's membership in NP, one gives a certificate of a valuation, which one then uses to verify that the SAT instance has a true valuation. That verification process, which one might also call a proof, is known to be in $NC^1$ (the Boolean Formula Value problem, calculating the boolean value of a formula with no variables, just boolean constants). $\endgroup$ – Mitch Jan 25 '11 at 1:17
  • $\begingroup$ continued...but to mix metaphors, that is a linear time algorithm. Anyway, the point is that the verification process produces a proof in the TM (as a sequence of moves), but the verification process, with the certificate as input has a certain nontrivial complexity to it. A certificate for an NEXP machine would be one that needs to be verified on an EXP machine, whose latter running time is, well, exponential (deterministic). So something I'd like to call a proof (simply the certificate) still needs to be supplied to a machine with possibly superlinear running time. $\endgroup$ – Mitch Jan 25 '11 at 1:23
  • $\begingroup$ A verification process is an algorithm, it cannot be in NC1. The language consisting of boolean formulas with no free-variables is in NC1. Of course, the circuit that decides this language has polynomial size with logarithmic depth. Also, a proof is not defined as an algorithm, is another string of bits that tells you if the input is in the language or not. Another example is, find a path with length <= l between nodes s and t in some graph. This problem is in P, and a proof will be a sequence of connected nodes with length l. $\endgroup$ – Marcos Villagra Jan 25 '11 at 1:34
  • $\begingroup$ the complexity of a proof is always defined as the length of an accepting path in the TM. This path is generated by the input. $\endgroup$ – Marcos Villagra Jan 25 '11 at 1:36
  • $\begingroup$ Am I getting your questions right? $\endgroup$ – Marcos Villagra Jan 25 '11 at 1:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.