${\mathrm{AC}}^0[p]$-Frege Cannot Efficiently Prove That Constant-Depth Algebraic Circuit Lower Bounds Are Hard

We say that a sequence of formulas ${\varphi }_n$ is hard if there is no proof of ${\varphi }_n$ of polynomial size in $|{\varphi }_n|$. One of the earliest steps in the Cook-Reckhow program – establishing a lower bound on the size of proofs – was taken by Haken [25]. He showed a super-polynomial lower bound for the Pigeonhole Principle formulas in Resolution. Soon after, Ajtai [1] showed a super-polynomial lower bound for the Pigeonhole Principle in ${\mathrm{AC}}^0$-Frege, which is the Frege-style system where proof lines are constant-depth Boolean circuits. Since then, several improvements and extensions of Ajtai’s result have been obtained [2, 6, 13], and the lower bound techniques used in these works mirror the random restriction techniques used to prove lower bounds against the circuit class ${\mathrm{AC}}^0$, further reinforcing the analogy between proof complexity lower bounds and circuit complexity lower bounds (cf. [39, 31]). In the circuit complexity setting, we also know lower bounds for the circuit class ${\mathrm{AC}}^0[p]$ of constant-depth Boolean circuits with prime modular gates, shown using the polynomial method of Razborov and Smolensky [47, 56]. Can the polynomial method or other techniques used to show proof complexity lower bounds for the corresponding Frege-style proof system ${\mathrm{AC}}^0[p]$-Frege?

Despite much effort, this question has remained open for more than three decades, and continues to be a frontier question in proof complexity. It is already highlighted as a key open problem in the 1998 survey of Beame and Pitassi [7], and the recent survey of Razborov re-iterates this [53]. Progress on the question has focused on restricted algebraic subsystems of ${\mathrm{AC}}^0[p]$-Frege such as the Nullstellensatz [6] and Polynomial Calculus [14] proof systems, which we discussed next.

Much of the research on ${\mathrm{AC}}^0[p]$-Frege lower bounds has focused on subsystems such as Nullstellensatz and Polynomial Calculus, which encode a CNF and the Boolean constraints on its variables as polynomials and reduce the task of proving that the CNF has no satisfying Boolean assignments¹¹1We will sometimes switch back and forth in our discussion between the tasks of refuting that a CNF formula is satisfiable and of proving that a DNF formula is a tautology, which are equivalent by De Morgan’s laws. to proving that these polynomials do not have a common zero [6, 13]. Nullstellensatz and Polynomial Calculus are propositional proof systems in the Cook-Reckhow sense [15], since the verification of proofs can be done in deterministic polynomial time.

Pitassi [38] proposed more powerful algebraic proof systems where verifying the correctness of a proof requires identity testing of algebraic circuits, i.e., checking whether a given algebraic circuit is identically zero. Identity testing is known to be doable in randomized polynomial time, but it remains a long-standing open question whether it can be done in deterministic polynomial time for general algebraic circuits. Thus, the more general algebraic systems proposed by Pitassi are not propositional proof systems in the traditional Cook-Reckhow sense, but they do have efficient randomized verification.

Grochow and Pitassi [24] defined a strong algebraic proof system in this sense, called the Ideal Proof System (IPS), where a single algebraic circuit acts as a certificate that a set of polynomial equations does not have a common zero. The size of an IPS proof is simply the size of the corresponding algebraic circuit which acts as a certificate. [24] showed that IPS is at least as strong as EF, and also that super-polynomial IPS lower bounds for any sequence of unsatisfiable formulas implies that the Permanent does not have polynomial-size algebraic circuits. This gives a long sought-after connection between proof complexity lower bounds for strong proof systems and (algebraic) circuit complexity lower bounds, but for an algebraic proof system with randomized verification rather than for a propositional proof system. In a more recent paper [54], the implication from proof complexity lower bounds to algebraic complexity lower bounds was strengthened to an equivalence for a certain explicit sequence of formulas.

Given that a proof in IPS is a single algebraic circuit, we can define and study variants of IPS where this circuit is of a restricted form. This has been done in several works in the past decade [18, 5, 23, 26], which seek to show proof complexity lower bounds for subsystems of IPS or to find closer connections between IPS variants and propositional proof systems. Proof complexity lower bounds in this setting are typically shown by adapting algebraic circuit lower bound techniques. One apparent drawback to this approach is that the hard candidates in these works are not propositional formulas, but rather purely algebraic instances (e.g., $x_1+\mathrm{\cdots }+x_n+1=0$) that cannot be directly translated to propositional logic (cf. [16] for a discussion of this point).

In 2021, a breakthrough super-polynomial algebraic circuit lower bound against constant-depth algebraic circuits was shown by Limaye, Srinivasan and Tavenas [34] for large enough fields, and very recently has been extended by Forbes [17] to fields of characteristic $p$ for any prime $p$. This motivates the question of whether a similar super-polynomial proof size lower bound holds for constant-depth IPS, where the certificate is a constant-depth algebraic circuit. Some progress on this question has been made in recent work [5, 23, 26], but it remains open whether there are unsatisfiable CNF formulas (or propositional logic formulas more generally) requiring super-polynomial constant-depth IPS proofs.

While most lower bounds in propositional proof complexity for concrete tautologies rely on combinatorial or algebraic techniques, one can also try to use logic – specifically, diagonalization – for this purpose. This is a natural idea, but in the propositional setting it faces an inherent obstacle: self-reference. Suppose that a formula $\mathrm{\Phi }$ expresses a proof-complexity lower bound. Ideally, one would like $\mathrm{\Phi }$ to encode the statement that “$\mathrm{\Phi }$ itself has no short proofs.” This, however, is impossible: any reasonable propositional encoding of $\mathrm{\Phi }$ must use at least $|\mathrm{\Phi }|$ symbols, so $\mathrm{\Phi }$ would necessarily be longer than itself.²²2Friedman [19] and Pudlak [40, 41] show how to adapt the proof of Gödel’s Second Incompleteness Theorem to give sub-linear proof size lower bounds for strong enough propositional proof systems.

One way to circumvent this problem, due to Krajíček, is to encode proofs implicitly, and hence more economically, via a circuit that computes the bits of the proof given their index (see [32]).

Santhanam–Tzameret [54] proposed a different approach: instead of referring to itself directly, a formula refers to a smaller version of itself. Concretely, they introduced the iterated lower bound formulas, which encode inductively the statement that “the previous-level formula has no short proof,” thus avoiding direct self-reference. This yields diagonalization-based formulas that provably lack short proofs infinitely often. Specifically, if at level $\mathrm{\ell }$ the formula

has either a long proof or a short proof, then in both cases it establishes the truth of the no-short-proof claim for ${\phi }_{\mathrm{\ell }-1}$. If ${\phi }_{\mathrm{\ell }}$ has no proof at all, then in particular it has no short proof. Thus, we are done: either ${\phi }_{\mathrm{\ell }}$ or ${\phi }_{\mathrm{\ell }-1}$ has no short proof, and this holds for infinitely many $\mathrm{\ell }$.

By referring to a smaller (and therefore different) version of itself, the resulting formulas demonstrate that ${\phi }_{\mathrm{\ell }}$ has no short proofs infinitely often. However, this still leaves open whether these formulas are hard tautologies or not tautologies at all (and thus vacuously unprovable). Let us elaborate on the difference between showing that a statement is not easy, and showing that it is hard, i.e., that it is a tautology with no short proofs.

In general, given a proof system, every propositional formula $\phi$ falls into one of three categories: 1. a tautology with a short proof (easy), 2. a tautology without short proofs (hard), or 3. not a tautology (hence unprovable). This is depicted in Table 1.

The standard aim in proof complexity is to establish hardness, i.e., to identify a formula in cell 2. For strong proof systems this remains open. Thus, a natural intermediate step is ruling out that a formula is easy (cell 1), while leaving open whether it belongs to cell 2 or 3. For this to be meaningful, one must consider sequences of formulas whose tautological status is unknown. A natural choice is formulas expressing open lower bounds in complexity theory. This viewpoint was emphasised by Razborov [52], who highlighted the importance of studying the proof complexity of natural statements whose validity is unknown. This approach was pursued in the 1990s by Razborov and others [48, 49, 51, 52] (see also Krajíček [33] and Raz [43]).³³3Typically, these propositional formulas are known unconditionally to be tautologies for random objects. For example, if a formula encodes a circuit lower bound for some Boolean function $f$, then for random $f$ the lower bound holds. Thus, while the interesting candidate formula stating, say, SAT $⊈\mathrm{P}/\mathrm{poly}$ is not known to be a tautology, for a random $f$ the statement $f\notin \mathrm{P}/\mathrm{poly}$ is.

In this work, as in [54], we follow this approach. We show that a family of DNF formulas of unknown validity has no short proofs. This situation is illustrated in Table 2.

There is another reason to consider statements of unknown validity when proving lower bounds for strong systems: very few plausible hard candidates are known for Frege and Extended Frege. The only compelling ones are random CNFs and circuit lower bound formulas, and for neither do we have effective methods for certifying validity. Indeed, confirming the validity of a fixed formula $\varphi$ typically requires a proof, and existing proof methods can usually be captured in polynomial-size Frege or Extended Frege proofs – implying that $\varphi$ is not a plausible hardness candidate for these systems.

As mentioned above, iterated lower bound formulas provide a simple way to show that a sequence of formulas is not easy. However, unlike formulas asserting SAT $\notin \mathrm{P}/\mathrm{poly}$, it is unclear whether there is any reason to believe they are tautologies. What [54] demonstrated is that assuming some circuit lower bounds one can go beyond the iterated lower bound formulas: rule out that some formulas are easy for formulas that are more likely to be tautologies – specifically, formulas expressing that proving algebraic circuit lower bounds is hard. In particular, [54] combined the diagonalization framework with the [24] reduction from proof complexity to circuit lower bounds that showed that a proof-size lower bound implies an algebraic circuit-size lower bound (VP $\ne$ VNP). Hence, instead of stating recursively that lower bounds are hard to prove, one formulates $\phi$ to be the statement “there are no short proofs of algebraic circuit lower bounds of the Permanent”. This avoids the recursively defined statement of the iterated lower bound formulas, and is a statement whose validity is easier to assess and use. In this way we obtain:

However, this still leaves an extra conditional layer: we need to rely on $\mathrm{VP}\ne \mathrm{VNP}$ (the circuit lower bound) to rule out that $\phi$ is easy.

In the present work, we eliminate this conditionality in the constant-depth regime. Using the unconditional constant-depth algebraic circuit lower bound of Limaye, Srinivasan and Tavenas [34], we extend the diagonalization framework to constant-depth circuits.

We demonstrate formulas that unconditionally are not easy for ${\mathrm{AC}}^0[p]$-Frege, such that:

• $\mathrm{■}$

  Plausibly tautologies: we give some evidence supporting the validity of these formulas;

• $\mathrm{■}$

  Necessary (complete): any hard instance for a sufficiently strong proof system must imply that our formulas are also not easy for that system;

• $\mathrm{■}$

  Amplifying: exhibiting a form of existential depth amplification: there exists a constant $d$, such that if our formulas are hard for depth-$d$ proofs then they are hard for every constant-depth $d^{\prime }$ proofs.

As mentioned above, Theorem 1 is shown via a diagonalization argument applied to the algebraic proof system IPS. It exploits the lower bound in [34] and Forbes’ finite fields version [17], and the fact that Grochow-Pitassi [24] showed that constant-depth IPS over finite prime fields simulates ${\mathrm{AC}}^0[p]$-Frege.

The formulas ${\varphi }_n$ express proof size lower bounds for algebraic proof systems, and the evidence for their validity comes from several sources.

The CNF formulas we consider are related to the circuit lower bound formulas considered by Razborov [48, 49, 51, 52], but with two differences: we consider algebraic rather than Boolean circuits, and our formulas express lower bounds for proving constant-depth algebraic lower bounds in constant-depth IPS, rather than express the circuit lower bounds directly. This allows us to adapt the diagonalization technique used to show an equivalence between circuit complexity and proof complexity in [54] to derive an unconditional proof complexity lower bound in our setting.

To state our result more precisely we need the following notation. Let $𝔽$ be some underlying (finite) field. We let:

• $\mathrm{■}$

  ${\mathrm{ckt}}_d({\mathrm{perm}}_n,s)$: a CNF formula expressing that the Permanent on $n\times n$ matrices has depth-$d$ algebraic circuits of size $s$ over $𝔽$.

• $\mathrm{■}$

  $\mathrm{ref}\text{-}{\mathrm{IPS}}_d(\varphi ,t)$: a CNF formula expressing that $\varphi$ has size-$t$ IPS refutations of depth-$d$ over $𝔽$.

• $\mathrm{■}$

  The diagonalizing CNF formula is:

  $${\psi }_{d,d^{\prime },n}:=\mathrm{ref}\text{-}{\mathrm{IPS}}_{d^{\prime }}({\mathrm{ckt}}_d({\mathrm{perm}}_n,n^{O(1)}),N^{O(1)}),$$

  where $N=|{\mathrm{ckt}}_d({\mathrm{perm}}_n,n^{O(1)})|$ is $O(2^{n^{O(1)}})$, expressing that depth-$d^{\prime }$ IPS refutes in polynomial-size that the permanent is computed by a depth-$d$ algebraic circuit of polynomial-size.

The use of $O(1)$ in the notation above is informal. We use it to avoid using more quantifiers that would make the statement below hard to parse.

Theorem 2 states the existence of no polynomial constant-depth IPS refutations for formulas that themselves express constant-depth IPS short refutation of constant-depth circuit upper bounds.

Here the size of a proof is always measured as a function of the length of the formula being proved. The result holds for any finite field, and further for sequence of prime fields of increasing size that are not too large, as we show below in Theorem 7.

Theorem 1 follows from Theorem 2 as follows: i) take the same $p$ as in the statement of Theorem 2; ii) let the formulas ${\varphi }_n$ in the former result to be the negation of ${\psi }_{d,d^{\prime },n}$ in the latter result⁴⁴4We take negation because we consider ${\mathrm{AC}}^0[p]$-Frege to be a proof system for DNF tautologies, while constant-depth IPS is a refutation system for unsatisfiable CNFs., where $d$ (the stated depth of circuit computing Permanent) is chosen to be large enough and $d^{\prime }$ (the stated depth of IPS refutations) is chosen as a function of $d$ so that Theorem 2 holds; iii) finally, use the fact that constant-depth IPS over fields of characteristic $p$ simulates ${\mathrm{AC}}^0[p]$-Frege [24].

Theorem 1 gives a first instance in which a formula whose validity is unknown is shown unconditionally to have no short proofs in ${\mathrm{AC}}^0[p]$-Frege. Razborov [50] and Krajíček [33] conjecture that all Boolean circuit lower bound formulas are hard for EF, but this is open even for ${\mathrm{AC}}^0$-Frege and even when we relax hardness to being non-easy (as we do in our work). Our lower bound is for proof complexity lower bound formulas rather than for circuit lower bound formulas, but our work is somewhat similar in spirit to [48].

From a technical point of view, our work is related to recent works by [54, 36], which also use diagonalization ideas. The main result of [54] is a conditional existence of hard formulas for IPS, under the assumption that $\mathrm{VNP}\ne \mathrm{VP}$. In contrast, our result ruling out easy formulas for constant-depth IPS, i.e., Theorem 2, is unconditional. One way to interpret our result is that it strengthens the equivalence between proof complexity lower bounds and circuit complexity lower bounds shown in [54] to hold for constant-depth circuits, and then applies the recent breakthroughs constant-depth algebraic circuit lower bounds [34, 17] to get unconditional proof complexity lower bounds.

Unconditional lower bounds for conjectured tautologies are also shown in [37] using a somewhat different diagonalization technique, however these are for highly non-explicit formulas⁷⁷7There are two sources of non-explicitness in [37]. First, they consider a distribution on conjectured hard formulas rather than a fixed hard formula at every length. Second the formulas refer to a non-constructively defined proof system with non-uniform verification., and do not seem directly relevant to progress on lower bounds for tautologies. In contrast, Theorem 6 shows that Theorem 2 is a necessary step toward super-polynomial lower bounds for constant-depth IPS.

One novel aspect in Theorem 1 is that a proof complexity lower bound for a propositional proof system is shown via algebraic circuit lower bounds. The theory of feasible interpolation in propositional proof complexity enables proof complexity lower bounds for weak systems such as Resolution and Cutting Planes to be derived from lower bounds on monotone circuit complexity [10, 28, 42]. However, there is cryptographic evidence against the applicability of feasible interpolation techniques to ${\mathrm{AC}}^0$-Frege and stronger proof systems [11]. Implications from average-case circuit lower bounds to proof size lower bounds for strong systems were conjectured by Razborov [52] in the context of proof complexity generators [3], but these conjectures are so far unproven.

We note that the question of proving proof complexity lower bounds for constant-depth IPS has in itself been highlighted and studied in recent works [5, 23, 26, 16, 8]. Andrews and Forbes [5] show a super-polynomial constant-depth IPS lower bound for refuting certain sets of polynomial equations. However, their hard instances do not themselves have polynomial-size constant-depth circuits, and in particular are not CNFs. Govindasamy, Hakoniemi and Tzameret [23] give a super-polynomial multilinear constant-depth IPS lower bound for refuting polynomial equations expressible as small depth-2 algebraic circuits. Hakoniemi, Limaye and Tzameret [26] extend and strengthen these results from multilinear to low individual degree proofs [23]. However, they also show that the lower bound framework of [23, 26] is incapable of proving lower bounds for CNFs. Elbaz, Govindasamy, Lu and Tzameret [16] showed that any constant-depth IPS lower bounds over finite fields would lead to lower bounds for CNF formulas and thus ${\mathrm{AC}}^0[p]$-Frege lower bounds. Alas, the strongest constant-depth IPS lower bounds [26] are restricted to low individual degree refutations, for which the result of [16] do not hold. Proving lower bounds for CNFs is essential for the application to ${\mathrm{AC}}^0[p]$-Frege lower bounds, and none of the previous works achieve this. Our work provides an explicit CNF formula with no short refutations and with some evidence for its unsatisfiability.

Let $𝔽$ be a field. Denote by $𝔽[\overline{x}]$ the field of polynomials with coefficients from $𝔽$ and variables $\overline{x}=[x_1,\mathrm{\cdots },x_n]$. A polynomial is a formal linear combination of monomials, where a monomial is a product of variables. Two polynomials are identical if all their monomials have the same coefficients. The degree of a polynomial is the maximum total degree of a monomial in it. We assume some familiarity with algebraic complexity. Basic definition in algebraic complexity can be found in [55].

Iterated Matrix Multiplication is in $\mathrm{VP}$.

This lower bound for $\mathrm{IMM}$ against constant-depth circuits was improved in [9]. Let $\mu (\mathrm{\Delta })=1/(F(\mathrm{\Delta })-1)$, where $F(n)=\mathrm{\Theta }({\phi }^n)$ is the $n$th Fibonacci number (starting with $F(0)=1$, $F(1)=2$) and $\phi =(1+\sqrt{5})/2$ is the golden ratio.

A recent result by Forbes [17] extended these results to any field, including finite fields.

Since ${\mathrm{IMM}}_{n,d}$ is a p-projection of the Permanent polynomial with $\mathrm{poly}(n,d)$ many variables, it follows that the Permanent does not have constant-depth polynomial-size circuits over any field, in the following sense.

Given $f_1,\mathrm{\cdots },f_m\in 𝔽[x_1,\mathrm{\cdots },x_n]$ over some field $𝔽$, Hilbert’s Nullstellensatz shows that $f_1(\overline{x})=\mathrm{\cdots }=f_m(\overline{x})=0$ is unsatisfiable (over the algebraic closure of $𝔽$) if and only if there are polynomials $g_1,\mathrm{\cdots },g_m\in 𝔽[\overline{x}]$ such that ${\sum }_j{g}_j(\overline{x})f_j(\overline{x})=1$ (as a formal identity), or equivalently, that 1 is in the ideal generated by the ${\{f_j\}}_j$.

We shall also use the algebraic version of $\mathrm{IPS}$(which does not use the Boolean axioms):

Now, we introduce some notation we will use in the following sections. Let $\overline{ℱ}={\{f_i(\overline{x})=0\}}_{i=1}^m$ be a collection of circuit equations, namely the $f_i$’s are written as algebraic circuits. We use $|\overline{ℱ}|$ to denote the total size of the circuit equations in $\overline{ℱ}$. We denote by $C:\overline{ℱ}{⊢}_{\mathrm{IPS}}^{s,\mathrm{\Delta }}1=0$ the fact that $\overline{ℱ}$ has an $\mathrm{IPS}$ refutation $C$ of size at most $s$ and depth at most $\mathrm{\Delta }$. If we do not care about the explicit size of the $\mathrm{IPS}$ refutation, we denote by $C:\overline{ℱ}{⊢}_{\mathrm{IPS}}^{\ast ,\mathrm{\Delta }}1=0$ the fact that $\overline{ℱ}$ has an $\mathrm{IPS}$ refutation $C$ of size polynomially bounded by $|\overline{ℱ}|$ and of depth $\mathrm{\Delta }$.

When we deal with algebraic $\mathrm{IPS}$ refutations, we will use the same notation as above, only using ${\mathrm{IPS}}^{\mathrm{alg}}$ instead of $\mathrm{IPS}$.

Polynomial identities are proved for free in $\mathrm{IPS}$, which was observed in [4], and this also holds for constant-depth IPS proofs.

The following theorem is from [24], and it already holds for ${\mathrm{IPS}}^{\mathrm{alg}}$.

In the section, we are working in the finite field ${𝔽}_q$ where $q$ is a constant (independent of the size of the formulas and their number of variables). When we work with $\mathrm{CNF}$ formulas in $\mathrm{IPS}$ we assume that the $\mathrm{CNF}$ formulas are translated as follows:

Notice that a $\mathrm{CNF}$ formula is satisfiable by 0-1 assignment if and only if the assignment satisfies all the equations in the algebraic translation of the $\mathrm{CNF}$.

The following definitions are taken from [54], and we supply them here for completeness.

Using results in [16], we could remove some extension axioms used in [54] when working over fixed finite fields. We use ${\mathrm{UBIT}}_j(x)$ to denote the following Lagrange polynomial:

where $x$ can be a single variable or an algebraic circuit. Hence, it is easy to observe that

Also, suppose $x$ has size $|x|$ and depth $0pt(x)$ (when $x$ is a single variable, it has size $1$ and depth $1$), ${\mathrm{UBIT}}_j(x)$ can be computed by an algebraic circuit of size $O({|x|}^{q-1})$ and depth $0pt(x)+2$.

We call $x^q-x=0$ the field axiom for the variable $x$.

We will use our new translation lemma for the next section, which is our main result in fixed finite fields. For polynomial-size finite fields, we have a different translation lemma.