Checking proofs with very low complexity

The very notion of mathematical proof is founded upon the idea that a proof is ‘routine’ to check. While it may be difficult to actually prove a mathematical theorem, a proof should allow us to verify its truth without question or significant effort. But exactly how much effort is required to check a proof, in terms of computational complexity?

Abstract proof systems and the Cook-Reckhow criterion

In proof complexity there is a well-known formalisation of this idea: the Cook-Reckhow criterion. This criterion says that, to qualify as a ‘proof system’, proofs must be polynomial-time checkable. It is this that gives rise to the famous Cook-Reckhow theorem [BIBCITE%%3%]:

Theorem (Cook-Reckhow ’74). There is a proof system for classical propositional logic with polynomial size proofs of each tautology if and only if $\mathbf{coNP} = \mathbf{NP}$ .

But this polynomial time criterion for checkability seems overkill in practice. We can usually verify proofs in commonly used systems in some ‘local manner’ leading to log-space algorithms or simpler.

So what is the general complexity of checking proofs? Well, naturally, the answer to that question depends on the proof system at hand. However, perhaps a lower bound can be derived from the following intuition: to know that a proof is correct, we have to at least check that the conclusion is a syntactically correct formula. This is known to not be possible in $\mathbf{AC}^0$ but is possible in $\mathbf{TC}^0$ (an apparently folklore result).

The log-time hierarchy (aka $\mathbf{AC}^0$ )

such as $\mathbf{AC}^0$ are defined using the model of random-access Turing machines. These machines are able to ‘jump’ to on the input tape by simply writing down the address of that cell in binary. In this way it makes sense to speak of ‘logarithmic-time computation’.

The class $\mathbf{AC}^0$ , in this setting, is now just the languages accepted on a logarithmic-time random access Turing machine which allows alternation, i.e. the machine may have both non-deterministic and co-nondeterministic states. From a descriptive complexity point of view, this means that we can compute predicates that use quantifiers over indices of the input (or other logarithmic-size objects) . Indeed there is a famous characterisation to this effect by Immerman [BIBCITE%%4%], that may be informally stated as follows:

Theorem (Immerman ’87). $\mathbf{AC}^0$ is just the class of languages recognised by first-order logic on finite structures.

More formally, the first-order signature here consists of basic manipulation of indices, e.g. $+$ , $\leq$ and $\max$ , and predicates for accessing the symbol at each index.

Example. Let us consider the modus ponens rule of Hilbert-Frege systems:

$\dfrac{A \quad (A \to B)}{B}$

We can verify that a triple of strings $(\sigma,\tau,\pi )$ forms an instance of this rule with the following $\mathbf{AC}^0$ predicate: there is an index $i<|\tau|$ such that,

$\tau(0)=``(" \ \wedge \ \tau(i)= ``\to" \ \wedge \ \tau(|\tau|-1)= ``)"$ ; and,
$\forall j<i . \ \sigma(j)=\tau(j+1)$ ; and,
$\forall j<|\pi|. \ \pi(j)=\tau(i+j)$ .

Here I am writing, say, $\sigma(i)$ to denote the symbol at position $i$ of the string $\sigma$ . As convention, indices start from the left at $0$ and finish on the right at $|\sigma|-1$ .

Log-time hierarchy with counting (aka $\mathbf{TC}^0$ )

Now the class $\mathbf{TC}^0$ is obtained from $\mathbf{AC}^0$ by adding an oracle for counting. More precisely, we may query at any point the number of symbols satisfying an already defined property. It might not seem like much of a change, but it is enough to stump complexity theorists: we have no nontrivial lower bounds for $\mathbf{TC}^0$ . In fact, as far as we know, $\mathbf{TC}^0$ could equal $\mathbf{NP}$ !

Example (Buss ’87). Buss gave a $\mathbf{TC}^0$ algorithm for formula verification in his seminal paper on the complexity of the Boolean Formula Value problem [BIBCITE%%5%], which we sketch a variation of here. Let us consider formulas generated by the following grammar:

$A \quad ::= \quad p \quad | \quad \neg A \quad | \quad (A \vee A) \quad | \quad (A \wedge A)$

We can check that a string $\sigma$ is formula as follows: for every index $i<|\sigma|$ we have that:

$\sigma(i)\sigma(i+1)$ is not a forbidden adjacent pair of symbols for formulas, e.g. $pp,p\neg ,(),\vee(,\wedge\vee$ ; and,
if $\sigma(i)=``\vee"$ or $\sigma(i)=``\wedge"$ then $\exists j,k$ with $j<i<k$ such that $\sigma(j)=``("$ and $\sigma(k)=``)"$ and the number of “(” and “)” in $\sigma(i,j)$ is identical.

The point is that if $\sigma$ is not a formula, then there must be some minimal substring $\sigma'$ that occurs in a correct context (i.e. $\sigma$ becomes a formula if we replace $\sigma'$ with a propositional variable) but is not a formula.

Note that there is a subtlety here about how propositional variables are coded, since there are infinitely many of them. A common and natural implementation, that suffices for our purposes, is that propositional variables are simply coded as strings with symbols distinct from the rest of the signature.

Further details on low-level complexity classes.

Hide details on low-level complexity classes.

Proofs as parsing certificates

However, one could imagine that a proof, as well as verifying the truth of a formula, also acts as a parsing certificate, at the same time verifying the syntactic correctness of the conclusion. Seen this way, the problem of checking syntactic correctness actually lies at the other end of a proof: the axioms. To check that an expression is an ‘instance’ of an axiom involves, in particular, checking that the expression is a formula. This yields a $\mathbf{TC}^0$ lower bound on checking, say, Hilbert-Frege style axiomatic proofs.

But what about systems where the axioms are atomic? Gentzen style sequent systems are the natural point of call. Indeed, taking a cedents-as-lists implementation seems rather promising, and indeed is the variant originally proposed by Gentzen. However, we hit another problem, namely the weakening and additive rules:

$\dfrac{\Gamma \to \Delta}{\Gamma, B \to \Delta}\qquad\dfrac{\Gamma \to \Delta}{\Gamma \to \Delta,B}\qquad\dfrac{\Gamma,A\to\Delta}{\Gamma,(A\wedge B)\to \Delta}\qquad\dfrac{\Gamma\to \Delta,A}{\Gamma \to \Delta, (B\vee A)}$

The problem with the rules above is that, in each case, the expression $B$ could be arbitrary and we only know that the conclusion is syntactically correct if we know that $B$ is a syntactically correct formula. A complete sequent calculus typically contains either the first two rules (and multiplicative $\wedge$ – $l$ and $\vee$ – $r$ ) or the second two rules (and contraction). Some calculi absorb weakening into the identity, but this gives us the same problem as for Hilbert-Frege systems since axioms are no longer atomic (see [BIBCITE%%6%] for a selection of such calculi).

Other classical proof formalisms exhibit the same problem of ‘new formulas’ occurring, top-down. For instance in natural deduction it is the elimination rules that are problematic. So I am left with the following curiosity:

Question. Is there a ‘natural’ proof system for which proof checking is in $\mathbf{AC}^0$ ?

One point of call could be deep inference proof theory, where all structural rules can be made atomic. (Note that this is impossible in sequent style systems, cf. [BIBCITE%%7%]). Such systems, in a sense, enjoy ‘local’ proof checking, though it does not seem that this has been formalised in the setting of computational complexity. For now this is beyond the scope of this post, but I aim to cover the complexity of checking deep inference proofs at some point in a future post.

Some special cases of efficient checkability

Notice that logics without ‘weakening behaviour’ do admit proof systems with $\mathbf {AC}^0$ -checkability. The simplest such example is that of Multiplicative Linear Logic, whose rules in a one-sided system are as follows:

$\dfrac{}{1}\qquad\dfrac{}{p,\bar p} \qquad \dfrac{\Gamma,A,B,\Delta}{\Gamma,B,A,\Delta}\qquad\dfrac{\Gamma}{\Gamma,\bot}\qquad\dfrac{\Gamma,A \quad \Gamma, B}{\Gamma,A\otimes B}\qquad\dfrac{\Gamma,A,B}{\Gamma,A\parr B}$

The weakening issue described above becomes present as soon as the additive connectives or exponential modalities are included.

There are also many systems that operate with a restricted syntax of formulas, such as clauses, e.g. Resolution. The problem of proof checking here is much simpler since we do not need to determine scoping. In particular, $\mathbf{AC}^0$ proof checking is possible with an appropriate implementation of the rules. For example the following conventions will suffice:

Clauses are implemented as lists, so that clause-identity is in $\mathbf{AC}^0$ .
The cut rule insists that the resolved literals occur in some fixed position in a clause, e.g. at the beginning or the end.
The structural rules exchange and contraction are explicit, due to the previous two points.

From the point of view of $\mathbf{AC}^0$ , it does not matter if the proof is tree-like or dag-like. This difference does, however, affect the amount of time taken in traversing the proof deterministically without random access.

Checking proofs with very low complexity

Abstract proof systems and the Cook-Reckhow criterion

The log-time hierarchy (aka $\mathbf{AC}^0$ )

Log-time hierarchy with counting (aka $\mathbf{TC}^0$ )

Proofs as parsing certificates

Some special cases of efficient checkability

References

Leave a Reply Cancel reply

Abstract proof systems and the Cook-Reckhow criterion

The log-time hierarchy (aka )

Log-time hierarchy with counting (aka )

Proofs as parsing certificates

Some special cases of efficient checkability

References

Leave a Reply Cancel reply

The log-time hierarchy (aka $\mathbf{AC}^0$ )

Log-time hierarchy with counting (aka $\mathbf{TC}^0$ )