New Bounds for the Ideal Proof System in Positive Characteristic

A long-standing open question in proof complexity, open for almost three decades [23], is to prove superpolynomial lower bounds against ${\text{AC}}^0[p]$-Frege proof systems, i.e., a proof system in which the lines of the proof are constant-depth Boolean circuits that use modular gates. In the late 80s, Razborov [28] and Smolensky [33, 34] resolved the Boolean circuit lower bound question for ${\text{AC}}^0[p]$, but the corresponding proof complexity question has proved to be elusive.

Over the years, several attempts have been made to resolve this question. The most relevant to our work is the result by Grochow and Pitassi [17, Theorem 3.5] which showed that constant-depth-IPS over characteristic $p$ can efficiently simulate ${\text{AC}}^0[p]$-Frege proofs. This means that proving superpolynomial lower bounds against constant-depth-IPS refutations will give superpolynomial lower bounds against ${\text{AC}}^0[p]$-Frege. This gives a strong motivation to prove IPS lower bounds over small characteristics.

Building on the work of [17], [13] further explored the power of IPS refutations. They proposed a concrete approach towards proving size lower bounds for IPS refutations via functional lower bounds (further explained in Section 1.4). Their method was inspired by the notion of functional lower bounds in in Boolean circuit complexity [16, 12]. They demonstrated the promise of their method by proving several lower bounds for different fragments of IPS.

For example, the strong algebraic complexity lower bounds known for $\mathrm{roABP}$s [25] and multilinear formulas [27] follow from understanding the evaluation dimension complexity measure in these models. Since this measure is essentially functional in nature, [13] used it to successfully prove lower bounds for $𝒞$-IPS when $𝒞$ is a class of read-once branching programs or multilinear formulas. Their bounds are over characteristic $0$.

This approach of [13] was further adapted by Govindasamy, Hakoniemi, and Tzameret [14] to prove superpolynomial lower bounds against (multilinear) constant-depth-IPS refutations. Their proof builds on some of the key components of the superpolynomial lower bound against constant-depth algebraic circuits by Limaye, Srinivasan, and Tavenas. The latter lower bound of [24] only worked over characteristic $0$; for this and other reasons, the result of [14] was also limited to characteristic $0$. In a recent paper, however, Forbes [11] improved the circuit lower bound result of [24] and proved the same⁴⁴4Some parameters in the lower bound by [24] were subsequently improved by [5] and [11] achieves those improved parameters. lower bound over any characteristic.

In light of these results, the next obvious step is to prove the lower bounds of [13, 14] over any characteristic. We achieve that in this work.⁵⁵5The subset-sum instances from [13, 14] are not always unsatisfiable over fields of positive characteristic; this requires that we tweak their instances to ensure unsatisfiability. Barring these changes, we qualitatively match their lower bounds over fields of positive characteristic.

A polynomial $f(𝐱)\in 𝔽[x_1,\mathrm{\dots },x_n]$ is a multilinear if the individual degree is at most $1$. For a polynomial $f(𝐱)$, the multilinearization operator, denoted by $\mathrm{𝗆𝗅}[\cdot ]$, changes for each variable $x_j$ and any $k$, every occurrence of $x_j^k$ in $f(𝐱)$ to $x_j$.

A polynomial $f(𝐱)\in 𝔽[x_1,\mathrm{\dots },x_n]$ is said to be a symmetric polynomial if the polynomial remains invariant under any permutation of the input variables. For a degree parameter $0\le d\le n$, the $d^{th}$ elementary symmetric polynomial $e_{n,d}(x_1,\mathrm{\dots },x_n)$ is defined to be the following multilinear polynomial $e_{n,d}(x_1,\mathrm{\dots },x_n)={\sum }_{\begin{array}{c}S\subseteq [n]\\ |S|=d\end{array}}{\prod }_{i\in S}{x}_i$. Whenever $n$ is clear from the context, we will denote the $d^{th}$ elementary symmetric polynomial by $e_d(𝐱)$.

We recall definitions of some of the standard models of computation relevant to our results.

Algebraic circuits and formulas. An algebraic circuit is a directed acyclic graph in which each node either computes a sum (or a linear combination) of its inputs, or a product of its inputs. The leaf nodes are either variables or constants. The size of an algebraic circuit is the number of edges in the circuit, and the depth of an algebraic circuit is the longest path from the output node (a sink) to a leaf node (a source). An algebraic formula is an algebraic circuit where the output of each node feeds into at most another node; in other words, the underlying graph of an algebraic formula is a tree. An algebraic formula is a multilinear formula if every gate of the formula computes a multilinear formula.

Sparse polynomials and constant-depth circuits. The class $\sum \prod$ consists of depth-2 formulas with an addition gate in the top layer and multiplication gates in the bottom (second) layer. All the gates have unbounded fan-in. $\sum \prod$ formulas essentially compute polynomials in the sparse representation i.e. as a sum of monomials. In general, a constant-depth algebraic circuit has $O(1)$ alternating layers of additional and multiplication gates.

Read-Once Oblivious Algebraic Branching Programs. A read-once oblivious algebraic branching program in the variable-order $\pi \in {𝒮}_n$⁶⁶6${𝒮}_n$ denotes the set of all permutation of $[n]$. is a directed acyclic graph whose vertices are partitioned into $n$ layers $V_0=\{s\},V_1,V_2,\mathrm{\dots },V_n=\{t\}$. For each $i\in \{1,2,\mathrm{\dots },n\}$, there are edges directed from layer $V_{i-1}$ to $V_i$ that are labelled by univariate polynomials in the variable $x_{\pi (i)}$. For each $s$-to-$t$ path $p$, the polynomial computed by $p$ is defined to be product of the edge labels on $p$. The polynomial computed by the $\mathrm{roABP}$ is defined as the sum of polynomials computed by all $s$-to-$t$ paths. The width of an $\mathrm{roABP}$ is ${\max }_{0\le i\le n}|V_i|$ i.e. the size of the largest layer of vertices.

For more background on these models of computation, please refer to one of the standard surveys in algebraic complexity ([32],[30]).

Our proof uses the functional lower bound method introduced by [13], which can be described as follows. We know that a $𝒞$-${\mathrm{IPS}}_{{\mathrm{LIN}}^{\prime }}$ refutation for $f(𝐱)$ consists of $A(𝐱)$, $B_i(𝐱)\in 𝔽[𝐱]$ such that

where $A(𝐱),B_1(𝐱),\mathrm{\dots },B_n(𝐱)$ belong to $𝒞$. As $f(𝐱)$ is unsatisfiable over the Boolean hypercube, this implies that over the Boolean hypercube, $A(𝐱)$ is a well-defined reciprocal of $f(𝐱)$. Hence, to show that $A(𝐱)$ cannot belong to $𝒞$, it is enough to show that any polynomial that agrees with $1/f(𝐱)$ cannot be computed by $𝒞$. That is, the problem of proving a lower bound on the size of $𝒞$-${\mathrm{IPS}}_{{\mathrm{LIN}}^{\prime }}$ is reduced to proving a functional lower bound for $1/f(𝐱)$.

At the heart of such a functional lower bound lies a degree lower bound, i.e., a lower bound on the degree of $\tilde{f}(𝐱)$, where $\tilde{f}(𝐱)$ and $f(𝐱)$ are related. In fact, $f(𝐱)$ is a lifted version of $\tilde{f}(𝐱)$. Once we have such a degree lower bound for $\tilde{f}(𝐱)$, we can apply proof ideas from algebraic complexity theory such as the rank-based lower bound methods. These methods allow for the degree lower bounds for $\tilde{f}(𝐱)$ to be lifted to size lower bounds for $f(𝐱)$.

For their machinery to work over positive characteristic, we prove a positive characteristic version of the degree lower bound (see Lemma 17 for the formal statement). In the case of the lower bound argument in [13], it was important to obtain a tight degree lower bound of exactly $n$. They needed it for the next step, i.e., lifting, to work. In our case, we show that such a degree lower bound holds with high probability (over the choice of coefficients of the hard instance). Once we have the degree lower bound, the rest of the lower bound proof works similar to the proof by [13]. Please refer to the full version for all the proofs.

We start by describing the main ideas in the proof of Theorem 8. Here, we proceed in two steps. First, we observe that for any sparse polynomial of degree $d$, we can flatten it to a linear polynomial by renaming the monomials by fresh variables. Our hard instance is indeed sparse, hence the observation can be used to rewrite the polynomial as a linear polynomial over a fresh set of variables.

Now, consider a linear polynomial $L(𝐱)-\beta$ such that $L(𝐱)={\alpha }_1{x}_1+{\alpha }_2{x}_2+\mathrm{\dots }+{\alpha }_n{x}_n$, where ${\alpha }_1,\mathrm{\dots },{\alpha }_n\in {𝔽}_{p^k}$ for some $k$ and prime $p$ and $\beta \in 𝔽\setminus {𝔽}_{p^k}$ such that it is not satisfiable over $0$-$1$ assignments.

To prove that the polynomial has a refutation over constant-depth circuits, we first prove that for every $j$, $L_j(𝐱)={\alpha }_1^{p^j}{x}_1+{\alpha }_2^{p^j}{x}_2+\mathrm{\dots }+{\alpha }_n^{p^j}{x}_n-{\beta }^{p^j}$ can be expressed as a multiple of $L(𝐱)$ modulo the ideal ${𝐱}^p-𝐱$, which is a shorthand for the ideal generated by ${\{x_i^p-x_i\}}_{i\in [n]}$.

We then observe that for $j=k$, $L_k(𝐱)-L(𝐱)$ is a non-zero constant and use this observation to construct small depth circuits for the refutation of $L(𝐱)-\beta$. Throughout, we use some standard but useful tricks available to positive characteristic fields. Please refer to the full version for all the proofs.

Now we discuss the proof outline for Theorem 10. For ease of exposition, we explain the ideas for the case of $m=1$ in Theorem 10, i.e. there is one multilinear symmetric polynomial $f(𝐱)$ that does not have a solution over the Boolean cube ${\{0,1\}}^n$. Suppose $𝔽$ has characteristic $p>0$. Any symmetric polynomial is a polynomial of the $n$ elementary symmetric polynomials¹¹¹¹11This follows from the Fundamental Theorem of Symmetric Polynomials. i.e. $e_1(𝐱),\mathrm{\dots },e_n(𝐱)$. However, if we restrict to the Boolean cube ${\{0,1\}}^n$, then any symmetric polynomial is a polynomial of just $𝒪(\log n)$ elementary symmetric polynomials. Let $\widehat{𝐞}(𝐱)$ denotes the tuple of those $𝒪(\log n)$ elementary symmetric polynomials.

Let $F(𝐲)$ be the $𝒪(\log n)$ variate polynomial such that $F(𝐲)\circ \widehat{𝐞}(𝐱)$ agrees with $f(𝐱)$ on the Boolean cube ${\{0,1\}}^n$. The Boolean cube ${\{0,1\}}^n$ is mapped to ${𝔽}_p^{𝒪(\log n)}$ under the map $\widehat{𝐞}(𝐱)$ because $\mathrm{char}(𝔽)=p$. The unsatisfiability of $f(𝐱)$ over the Boolean cube ${\{0,1\}}^n$ implies the unsatisfiability of $F(𝐲)$ over ${𝔽}_p^{𝒪(\log n)}$. Applying Hilbert’s Nullstellensatz Theorem (see Theorem 15) on the unsatisfiability¹²¹²12To capture the restriction of ${𝔽}_p^n$, we add $n$ univariate polynomials, each of which vanishes on one coordinate of ${𝔽}_p^n$. of $F(𝐲)$ over ${𝔽}_p^{𝒪(\log n)}$, we get a low-variate Nullstellensatz certificate (it is a Nullstellensatz certificate in just $𝒪(\log n)$ variables)¹³¹³13Loosely speaking, one can imagine this as a “dimension reduction” of our problem. The symmetric structure of $f(𝐱)$ led us to convert a problem in $n$ variables to a problem in just $𝒪(\log n)$ variables.. The coefficients of this low-variate Nullstellensatz certificate can be computed via $\mathrm{poly}(n)$-sized constant-depth circuits. This follows from the fact that we are working over constant characteristic. Refer to the diagram below for a schematic representation of what we discussed so far.

Next we “lift” the Nullstellensatz back to the $n$ variables $(x_1,\mathrm{\dots },x_n)$. To do so, we plug-in $\widehat{𝐞}(𝐱)$ in place of $𝐲$. Observe that this substitution by $\widehat{𝐞}(𝐱)$ preserves the size and the depth of the coefficients of the low-variate Nullstellensatz certificate because of the Ben-Or’s construction (see Theorem 12).
It remains to prove via constant-depth circuits that $F(\widehat{𝐞}(𝐱))$ agrees with $f(𝐱)$ on the Boolean cube, i.e. $F(\widehat{𝐞}(𝐱))-f(𝐱)$ lie in the ideal $({𝐱}^2-𝐱)$. Here “to prove in constant-depth circuits” refers to giving a certificate for the ideal membership whose coefficients can be computed by constant-depth circuits. More precisely, we want to prove that there exists polynomials $B_j(𝐱)$’s which have $\mathrm{poly}(n)$-sized constant-depth circuits such that

This is the key step in our proof. To prove this, it suffices to prove the following special case.

Please refer to the full version for all the proofs.

1. 1.

   Using the word polynomials framework of [24], construct a knapsack polynomial ${\mathrm{ks}}_{𝐰}$ (for a partition given by a word $w\in {\mathbb{Z}}^d$) with the property that the set-multilinear projection of $\frac{1}{{\mathrm{ks}}_{𝐰}}$ over the Boolean cube requires superpolynomially large set-multilinear constant-depth circuits.

2. 2.

   Consider a degree-4 subset-sum variant $f(𝐳,𝐱):={\sum }_{i,j,k,l}{z}_{i,j,k,l}{x}_i{x}_j{x}_k{x}_l-\beta$ so that for the word $w\in {\mathbb{Z}}^d$ that will be used to instantiate the previous point, there exists an assignment of some of the variables in $𝐳$, $𝐱$ that maps $f(𝐳,𝐱)$ to ${\mathrm{ks}}_{𝐰}$ (upto a renaming of variables).

3. 3.

   If there is a multilinear polynomial computing $1/f(𝐳,𝐱)$ over ${\{0,1\}}^n$ that has a small constant-depth circuit, then there is a multilinear polynomial computing $1/{\mathrm{ks}}_{𝐰}$ over ${\{0,1\}}^n$ that has a small constant-depth circuit. Moreover by the set-multilinearization of [24], there is a small set-multilinear constant-depth circuit computing the set-multilinear projection of $1/{\mathrm{ks}}_{𝐰}$.

4. 4.

   Combining the first point with the contrapositive of the third point, conclude that any multilinear polynomial computing $1/f(𝐳,𝐱)$ over ${\{0,1\}}^n$ requires superpolynomially large constant-depth circuits. The multilinear constant-depth ${\mathrm{IPS}}_{{\mathrm{LIN}}^{\prime }}$ lower bound follows.

In [14], the proof for the hardness of $\frac{1}{{\mathrm{ks}}_{𝐰}}$ requires the underlying field to be of large characteristic essentially because it requires the degree lower bound from [13], which requires large characteristic. To make Theorem 20 work over fields of positive characteristic, we will employ our degree lower bound from Lemma 19 with a variant of the knapsack polynomial; the rest of the proof remains the same as that of Theorem 20. To provide the necessary details, we first describe the construction of the knapsack polynomial. Then, we state the particular claim from [14] that uses the degree lower bound from [13]. Finally, we show how our degree lower bound Lemma 19 fits into the rest of the proof.

We shall now recall the definitions required for defining the hard polynomial in [14] via the word polynomials template of [24].

Let $𝐰\in {\mathbb{Z}}^d$ be an arbitrary word. For any $S\subseteq [d]$, let ${w|}_S$ denote the subword of $w$ indexed by the set $S$. Consider the sequence $\overline{X}(w)=(X(w_1),\mathrm{\dots },X(w_d))$ of sets of variables. Define the positive indices and negative indices of $𝐰$ as:

Let any $i\in P_{𝐰}$, the variables of $X(w_i)$ will be of the form $x_{\sigma }^{(i)}$, where $\sigma$ is a binary string indexed by the set:

We will call these sets positive indexing sets. The size of each $A_{𝐰}^{(i)}$ is $|w_i|$. The number of strings in $A_{𝐰}^{(i)}$ is $2^{|w_i|}$.
For $i\in N_{𝐰}$, we similarly define the negative indexing sets $B_{𝐰}^{(i)}$ that will be used to index the variables of $X(w_i)$ for $i\in N_{𝐰}$.
A word $w\in {\mathbb{Z}}^d$ is balanced if:

1. 1.

   $\forall i\in P_{𝐰}\exists j\in N_{𝐰}$ such that $A_{𝐰}^{(i)}\cap B_{𝐰}^{(j)}\ne \mathrm{\varnothing }$ (i.e. $j\in N_{𝐰}$ is a witness that $𝐰$ is balanced at $i\in P_{𝐰}$)

2. 2.

   $\forall j\in N_{𝐰}\exists i\in P_{𝐰}$ such that $A_{𝐰}^{(i)}\cap B_{𝐰}^{(j)}\ne \mathrm{\varnothing }$ (i.e. $i\in P_{𝐰}$ is a witness that $𝐰$ is balanced at $j\in N_{𝐰}$)

For any $i\in P_{𝐰},\sigma \in {\{0,1\}}^{A_{𝐰}^{(i)}}$, define:

The product ranges over each $j\in N_{𝐰}$ that witnesses the fact that $𝐰$ is balanced at $i$. The sum ranges over each ${\sigma }_j$ that is consistent with $\sigma$ on $A_{𝐰}^{(i)}\cap B_{𝐰}^{(j)}$. Now, we define the knapsack polynomial as

where $\beta \in 𝔽$ is any field element such that ${\mathrm{ks}}_{𝐰}$ has no Boolean roots. To make the proof work over fields of positive characteristic, we define a variant of ${\mathrm{ks}}_{𝐰}$ as: