16
$\begingroup$

In this question, suppose $S$ is some popular real-world automated proof system that is stronger than or equivalent to Peano Arithmetic. I would be happy with a positive answer to the following for any such $S$, so please feel free to cherry-pick $S$ to make that easier:

Can the validity of an $S$-proof be verified in time polynomial in the string-length of the proof?

I've been able to find some work assessing progress in formal proof verification, such as

http://www.ams.org/journals/notices/200811/tx081101408p.pdf

but not much on the algorithmic complexity of verifying the outputs of various approaches, so I figure I must be looking in the wrong places / using the wrong search terms. Please, help point me in the right direction!

Improve this question
$\endgroup$
8
  • 6
    $\begingroup$ I'm shocked that the answer seems to be turning out to be no. I cannot help but think, however, that the systems for which proof-checking is not polynomial-time that what they are calling the proof object is not really what we want to think of as the real proof object, but rather a kind of convenient short-cut, like directions of how to build an honest proof. $\endgroup$ Commented Dec 26, 2015 at 12:23
  • 2
    $\begingroup$ @JoelDavidHamkins, I agree, since what we normally think of as an "honest proof" is a series of steps each of which follows from the previous by application of one of a finite number of axioms or rules of deduction, and such an "honest" proof is thus checkable in linear time by checking each step. $\endgroup$ Commented Dec 26, 2015 at 17:11
  • 1
    $\begingroup$ As Jason illustrates in his answer, speed of proof verification in systems based on type theory depends on the performance of the normalization algorithm. Some type theories might have fast normalization but this is not the case for the calculus of inductive constructions used by Coq. In any case, the key word 'strong normalization' is perhaps what you're looking for in the last sentence. $\endgroup$ Commented Dec 26, 2015 at 19:34
  • 2
    $\begingroup$ I yet have to see useful polynomial-time checkable proofs. $\endgroup$ Commented Dec 26, 2015 at 21:58
  • 3
    $\begingroup$ I think I can summarize the discussion as follows: (1) In theory, proofs should be polynomial time checkable objects, but these are not feasible to work with. (2) In practice, proof assistants rely on automation, that is a computer program constructing a theorem, but checking the program is undecidable. (3) Proof assistants often work by passing the generated proof through a kernel (a small piece of code which actually does the checking), and so one only needs to check the proof term passed to the kernel. This depends on the speed of the normalization procedure needed to check the proof term. $\endgroup$ Commented Dec 27, 2015 at 1:13

3 Answers 3

Reset to default
7
$\begingroup$

No, for languages based on Martin-Löf Type Theory

In proof systems based on Martin-Löf Type Theory, including Coq and Agda, proof-checking can involve evaluating arbitrarily complicated (proven-terminating) programs.

As a simple example, we can define a function is_positive : ℕ → Prop that evaluates to True if its argument is positive, and evaluates to False otherwise. The size of a proof of is_positive is constant (it's just a proof of True when is_positive is given an argument that evaluates to a numeral). However, it's relatively easy to define an exponentiation function that makes checking a proof of is_positive$2^n$ take time exponential in $n$. Here is the Coq code:

(** Define a version of [+] which is recursive on the right argument. *) Fixpoint plusr (n m : nat) {struct m} : nat := match m with | 0 => n | S m' => S (plusr n m') end. (** Define a version of [*] which is recursive on the right argument. *) Fixpoint multr (n m : nat) {struct m} : nat := match m with | 0 => 0 | S m' => plusr n (multr n m') end. Fixpoint pow (base exponent : nat) {struct exponent} : nat := match exponent with | 0 => 1 | S e' => multr base (pow base e') end. (** Test [pow] *) Compute pow 1 2. (* 1 *) Compute pow 2 3. (* 8 *) (** Return [True] if a number is [S _], [False] if it is [0] *) Definition is_positive (n : nat) : Prop := match n with | 0 => False | S _ => True end. Time Check I : is_positive (pow 2 9). (* 0.09375 *) Time Check I : is_positive (pow 2 10). (* 0.40625 *) Time Check I : is_positive (pow 2 11). (* 1.875 *)

Since numbers are stored in unary, by default, in Coq, the proof term I : is_positive (pow 2 n) has $\mathcal O(n)$ nodes.

You could, hypothetically, output evidence of well-typedness. In the degenerate case, where your well-typedness evidence is just a trace of the execution of the typechecker, you get linear time checking in the length of trace (assuming your trace-encoding isn't eliding expensive details).

I'm uncertain about languages like HOL, which are not based on dependent type theory. It's plausible that there are some systems where proof-checking is extremely simple, and can't involve any computation. I would look at Metamath as a likely candidate, even though it's closer to machine-checked proof than automated theorem proving (and I don't know of anyone using it for things outside of pure math).

Improve this answer
$\endgroup$
3
  • $\begingroup$ If I recall correctly, Coq's I is the canonical element of True? So Check I : is_positive (pow 2 11) asks Coq to verify that is_positive (pow 2 11) is definitionally equal to True. This can only be done by reducing pow 2 9 until it matches S _, which sadly happens only when pow 2 9 is reduced to a numeral. If this is what is going on here, it's worth pointing out that this are other terms of type pow 2 9 that type check much faster. $\endgroup$ Commented Dec 26, 2015 at 16:26
  • $\begingroup$ You mentioned HOL is not based on type theory. If by HOL you mean the HOL proof assistant (and its offspring, like HOL Light), then they are based on type theorem, just not dependent type theorem. Maybe you had Mizar in mind? $\endgroup$ Commented Dec 27, 2015 at 0:37
  • $\begingroup$ Jason: Updated to say "dependent type theory". My knowledge is narrow as far as concrete examples go. Thanks! François: That's correct. This proof is also instantaneous if you recurse on the left rather than the right for add and mult. The point is that you can't avoid things like this in general in dependent type theory. $\endgroup$ Commented Dec 31, 2015 at 3:49
4
$\begingroup$

It of course depends on the proof system, but it's polynomial (actually basically linear) in any reasonable one. The catch is that (by incompleteness) there's no effective bound on how long the proof might have to be based on the statement of the theorem.

Suppose you've got a proof system where verifying the proof takes triple-exponential time (or whatever) using some Turing machine T. Then imagine running T on the proof, recording all the execution steps. The sequence of recorded steps is in a sense a new proof, that can be verified in essentially linear time, though the new proof itself is much longer than the old proof.

Improve this answer
$\endgroup$
1
  • 3
    $\begingroup$ As Jason Rute points out, the claim that checking a proof is polynomial is not necessarily true for automated proof systems, whose proofs may include arbitrary computations which happen to terminate. It's true that one could replace the proof certificates with longer ones which explain the computation (or just pad the length...), but the existing systems don't do that. $\endgroup$ Commented Dec 26, 2015 at 2:04
3
$\begingroup$

Given that I can cherry-pick the system, consider HOL Light. In HOL light (and probably in other systems like Isabelle and Coq), the proofs are written in a functional programming language (for HOL Light, it is OCaml). The formal proof is a program which merely constructs a theorem object. Part of the proof program are tactics, that is subroutines which apply powerful reasoning to calculate a proof. These tactics can take a while. More specifically, since the language the proof is written in is Turing complete there is no upper bound on the algorithmic complexity except that it is computable. Even some of the built-in tactics check first order validity which is unsolvable, and therefore has no nice upper bound on complexity.

Obviously, in practice, the proofs in proof systems are checkable in a feasible amount of time.

Also, one can modify the proof system to output a lambda term as a proof witness. This can be checked faster, but I don't know the exact upper bound on running time (it might still be theoretically bad). An expert could give a better answer to this second point.

Improve this answer
$\endgroup$
4
  • 1
    $\begingroup$ Are you saying that the question of whether something is a proof is not even decidable in this system? After all, if all we have is essentially a program for constructing the theorem object, then in a Turing-complete programming context, we cannot decide whether or not that program will halt. $\endgroup$ Commented Dec 26, 2015 at 12:41
  • $\begingroup$ Yes, that is what I am saying. (I guess, when I said "computable," I meant computable if it constructs a proof, but you are right, it is undecidable.) $\endgroup$ Commented Dec 26, 2015 at 16:22
  • 1
    $\begingroup$ I think it's best to separate the tactic language from proof verification since tactics are really part of proof automation. Proof assistants do a bit of automation on top of a trusted proof verification kernel. I think it's better to separate the two. For example, Coq has a tactic that will automatically generate a proof of any true goal in Presburger arithmetic. The same could be done for any decidable theory, no matter how complex the decision algorithm. The Coq kernel only verifies the correctness of the term generated and doesn't care whether it came from a tactic or was written by hand. $\endgroup$ Commented Dec 26, 2015 at 20:05
  • $\begingroup$ @FrançoisG.Dorais, while I agree with you, I might point out that HOL Light---with which I am most familiar--does not generate proof terms, though it could be modified to do so. (I haven't used HOL Light in 7 years; things may have changed.) Instead, it relies on type-safety to only construct true theorems. The only "proofs" in HOL Light are the ML programs. (I don't know about Coq. Is, for example, the proof term for Gonthier's Coq proof of the Four Color Theorem stored somewhere?) My answer to the OP's question was also an attempt to clarify how systems like Coq and HOL Light actually work. $\endgroup$ Commented Dec 27, 2015 at 0:28

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.