Symmetric Proofs in the Ideal Proof System

A central project within the subject of proof complexity [2, 32, 25] is to define ever more powerful proof systems for propositional logic for which it is possible to establish superpolyonomial lower bounds on the size of proofs. The Ideal Proof System (IPS), introduced by Grochow and Pitassi in [21], is a powerful algebraic proof system that subsumes many previous algebraic and propositional proof systems such as the polynomial calculus and Frege proof systems. No superpolynomial lower bounds are known for the unrestricted IPS and it has been shown, for instance, that it efficiently simulates powerful proof systems such as extended Frege, for which such lower bounds are a long-standing open problem. On the other hand, lower bounds have been shown for interesting restrictions of IPS.

In IPS, like other algebraic proof systems, propositional formulas are coded as polynomial equations and a proof (or refutation) is a certificate showing that a given equation system has no solution. Equivalently, the certificate shows that the input polynomials, or axioms, have no common zero. In IPS, the certificate is an algebraic circuit which witnesses that the unit polynomial $1$ is in the ideal generated by the axioms, and we measure the complexity of the certificate in terms of the size of the circuit. Here, an algebraic circuit is a representation of a polynomial as a circuit with constants and variables as inputs and addition and multiplication gates. In order to make progress on showing lower bounds for IPS, it has been suggested [21] to study fragments of IPS given by restrictions on the circuits considered. A successful recent line of work has established super-polynomial lower bounds for fragments such as bounded-depth circuits, multilinear formulas and so-called read-once oblivious algebraic branching programs (roABPs) [17, 18, 23]. The common method behind these results has been named the functional lower bound technique.

In the present paper, we consider a natural restriction on IPS proofs based on symmetric circuits. Non-trivial lower bounds for symmetric algebraic circuits have recently been established [15, 16, 13] and this raises the question of whether, when the input polynomials have natural symmetries, the corresponding proof can also be made symmetric. Or, perhaps more interestingly, whether the lower bound methods for symmetric algebraic circuits can be possibly combined with functional lower bound techniques to obtain lower bounds for symmetric IPS proofs.

The present paper lays the foundations for this. We formalise the symmetry requirement in IPS proofs and show that any proof can be symmetrised though the interaction with linear IPS and other natural fragments is subtle. Beyond this, our work has two main contributions. First, we show how the study of symmetric IPS fits into the context of a larger project that investigates the role of symmetry in lower bounds in a number of areas of complexity theory (see [9]). This project is centred around the concept of symmetric computation in the sense of symmetric circuits and logics from finite model theory [10, 12]. Specifically, it seeks to lift game-based methods from finite model theory which are used to show inexpressiveness results in logic to lower bounds in other models of computing. There is a well-established connection between the expressive power of such logics and propositional proof complexity. In particular, it has been shown that, by encoding propositional axioms as relational structures in a suitable way, the problem of the existence of a resolution refutation of a given width, or of a polynomial calculus refutation of a fixed degree are expressible in existential fixed-point logic and fixed-point logic with counting (FPC) respectively and are indeed complete for these logics under weak, symmetry-preserving reductions [29]. Hence, in a precise sense these logics exactly characterise the power of the corresponding proof systems and from lower bounds on the expressive power of the logics we can extract lower bounds in proof complexity. Moreover, the stronger logic Choiceless Polynomial Time (CPT) can, in a symmetry-preserving way, be simulated in the bounded-degree extended polynomial calculus [27]. CPT is of great importance in descriptive complexity as a candidate logic for capturing PTIME [28, 19].

As the results we show in Section 5 establish, symmetric IPS proofs offer a suitable unifying formalism in which the results from [29, 27] can be recast. The expressive power of FPC corresponds to the bounded-degree symmetric IPS proofs, and the stronger logic CPT can only be simulated by symmetric IPS proofs of unbounded degree. Importantly, the symmetries of the IPS proofs we consider are the inherent symmetries of the input structure, which are the symmetries under which the corresponding FPC or CPT computation is invariant.

The second focus of this paper is upper bounds for the size of symmetric IPS refutations of various families of instances that possess natural symmetries. One example, where upper (and lower) bounds actually follow from results in finite model theory, is a formulation of the graph isomorphism problem as a system of polynomial equations [3] over $\mathbb{Q}$. The equations expressing that two graphs $G$ and $H$ are isomorphic are symmetric under the automorphism groups of $G$ and $H$. We show that the complexity of symmetric IPS refutations with these symmetry groups matches the descriptive complexity of distinguishing $G$ and $H$: Graphs that are distinguishable in FPC, or equivalently by the $k$-dimensional Weisfeiler-Leman algorithm [24] for fixed $k$, admit bounded-degree polynomial-size symmetric IPS refutations. Graphs that are distinguishable in the stronger logic CPT, but not in FPC, admit polynomial-size symmetric IPS refutations, but not of bounded degree. This separates in particular the bounded-degree fragment of symmetric IPS from its unbounded-degree version (Theorem 13).

A related family of instances we consider is a system of linear equations over the finite field ${𝔽}_2$ that expresses the isomorphism problem on Cai-Fürer-Immerman (CFI) graphs [6, 1] which is known to be inexpressible in FPC. Even though the instances exhibit a large number of interesting symmetries and are the core of numerous finite model theory lower bounds, it turns out quite surprisingly that they do admit polynomial-size symmetric IPS refutations. However, we are not able to exhibit a linear symmetric IPS refutation of the CFI equations of less than exponential size, making them a candidate for separating the linear fragment from the full symmetric IPS. Here the linear (or Hilbert-like) fragment is as defined in [21] (see also Section 3.2).

Besides the CFI equations, we consider standard hard examples from proof complexity, namely the pigeonhole principle (PHP) and the subset sum problem. The former is the classic tautology asserting that there is no injective function from a set of $n+1$ elements to a set of $n$ elements. The latter is simply the equation ${\sum }_{i=1}^n{x}_i-\beta =0$, together with the equations $x_i^2-x_i=0$ for all $i$, which is unsatisfiable when $\beta >n$. The pigeonhole principle has been used to obtain lower bounds for resolution [22] and bounded-degree polynomial calculus [30]. This is again a promising candidate for showing lower bounds on the size of symmetric IPS proofs as the tautologies are rich in symmetries and we know of no sub-exponential size symmetric IPS refutations for PHP.

In contrast, for subset sum, we do obtain polynomial size symmetric IPS refutations, which is significant because subset sum and its variations are the key instances where the functional lower bound method [17, 18, 23] has been used to obtain lower bounds. Thus, symmetry alone is a limitation of a rather different nature than others, e.g. multilinear-formula, constant depth or roABP-IPS where functional lower bounds have been established.

Our upper bounds on proof sizes are summarised in the table below. In this table, the entry “none” indicates that no proofs with the given restrictions exist. In the first row, $k$ is an arbitrary positive integer and $c$ is a function of $k$. In the other rows $c$ is a fixed constant. Our upper bounds for the graph isomorphism problem depend on the graphs: We consider graphs that are distinguishable by the $k$-dimensional Weisfeiler Leman (WL) algorithm versus graphs that are distinguished by CPT; the latter distinguishes strictly more graphs [14]. It should be noted that even the exponential lower bounds are non-trivial as the trivial bound for a symmetric circuit may be $n!$.

We denote by $[n]$ the set $\{1,\mathrm{\dots },n\}$. We call a set $X$, with the action of a group $\mathrm{\Gamma }$ on it a $\mathrm{\Gamma }$-set. The action of $\mathrm{\Gamma }$ on $X$ has a natural extension to a number of other sets defined from $X$. In particular, the following are $\mathrm{\Gamma }$-sets: $X^k$ for any $k\in \mathbb{N}$ ($\pi \in \mathrm{\Gamma }$ takes $(x_1,\mathrm{\dots },x_k)$ to $(\pi (x_1),\mathrm{\dots },\pi (x_k))$; the set $A^X$ of functions from $X$ to any set $A$ (here $\pi \in \mathrm{\Gamma }$ takes $f:X\to A$ to $f\circ {\pi }^{-1}$); and the collection $𝔽[X]$ of polynomials over $X$ with coefficients from a field $𝔽$.

If $X$ is a $\mathrm{\Gamma }$-set and $p\in 𝔽[X]$ a polynomial, then we say that $p$ is $\mathrm{\Gamma }$-symmetric or $\mathrm{\Gamma }$-invariant if $\pi (p)=p$ for every $\pi \in \mathrm{\Gamma }$. A set of polynomials $ℱ\subseteq 𝔽[X]$ is $\mathrm{\Gamma }$-invariant if $\{\pi (f)\mid f\in ℱ\}=ℱ$ for every $\pi \in \mathrm{\Gamma }$. We write $\mathrm{𝐒𝐲𝐦}(X)$ for the symmetric group on $X$ and for a finite relational structure $𝔄$ we write $\mathrm{𝐀𝐮𝐭}(𝔄)$ for the automorphism group of $𝔄$.

In what follows, $X$ denotes a finite set of variables, $𝔽$ denotes a field, and $𝔽[X]$ is the corresponding ring of polynomials in the variables $X$. Instances for the algebraic proof systems we consider are systems of polynomial equations. A system of polynomial equations is a finite set $ℱ\subseteq 𝔽[X]$, and a solution for $ℱ$ is an assignment $s:X\to 𝔽$ such that $f(s(\overrightarrow{x}))=0$ for each $f(\overrightarrow{x})\in ℱ$. We say that $ℱ$ is satisfiable if it has a solution, and unsatisfiable otherwise. If we wish to encode Boolean satisfiability problems, where the assignments are in $\{0,1\}$ only, then we include in $ℱ$ the Boolean axioms $x^2-x$ for each $x\in X$.

For a system of polynomial equations $ℱ$, the degree $\mathrm{deg}(ℱ)$ of $ℱ$ is the maximum degree of any polynomial in $ℱ$. The size $|ℱ|$ of $ℱ$ is the total number of variables and equations, i.e. if $ℱ=\{f_j\in 𝔽[X]|1\le j\le m\}$, then $|ℱ|≔m+|X|$.

Algebraic proof systems are formalisms for refuting the satisfiability of polynomial equation systems. A refutation is a certificate of unsatisfiability checkable in deterministic or randomized polynomial time. Usually, the certificate is based on Hilbert’s Nullstellensatz: It states that for any polynomial system of equations over an algebraically closed field $𝔽$, $ℱ\subseteq 𝔽[X]$, $ℱ$ is unsatisfiable if, and only if, $1$ is in the ideal generated by $ℱ$, which means that there are $g_1,g_2,\mathrm{\dots },g_m\in 𝔽[X]$ such that ${\sum }_{i\le m}{f}_i{g}_i=1$. Thus, a refutation of $ℱ$ in an algebraic proof system is typically a systematic proof of the existence of such $g_1,g_2,\mathrm{\dots },g_m$. The proof systems we are concerned with are (variants of) the polynomial calculus (PC) and the Ideal Proof System (IPS). In the following, whenever we consider unsatisfiable polynomial systems of equations over a field $𝔽$ and their refutations, we always implicitly mean the algebraic closure of $𝔽$ – otherwise the algebraic proof systems are not complete because the Nullstellensatz does not hold.

The efficiency of different proof systems is compared using the standard notion of $p$-simulation: Let $P_1,P_2$ be two proof systems and ${\mu }_1,{\mu }_2$ be complexity measures for them, that is, functions that map refutations to natural numbers. Then we write $P_2{\le }_p{P}_1$ (with respect to the measures ${\mu }_1,{\mu }_2$, which will usually be clear from the context) if for every system of polynomial equations $ℱ$, and every $P_2$-refutation $R_2$, there exists a $P_1$-refutation $R_1$ of $ℱ$ with ${\mu }_1(R_1)\le \text{poly}({\mu }_2(R_2))$. We write $P_1{\equiv }_p{P}_2$ if $P_2{\le }_p{P}_1$ and $P_1{\le }_p{P}_2$.

We now introduce the symmetry restriction on IPS proofs. That is to say, we consider when a set $ℱ$ of polynomials that is $\mathrm{\Gamma }$-invariant for a group $\mathrm{\Gamma }$ acting on its variables, admits a $\mathrm{\Gamma }$-symmetric circuit as an IPS refutation. We start with a formal definition.

Note that if $\mathrm{\Gamma }=\{\mathrm{id}\}$, then any IPS refutation of $ℱ$ is also a $\mathrm{\Gamma }$-symmetric IPS refutation of $ℱ$. The complexity of a symmetric IPS refutation in general heavily depends on the choice of $\mathrm{\Gamma }$. The bigger $\mathrm{\Gamma }$ is and hence the more symmetric the circuits are required to be, the bigger we can expect the proof size to be.

We generally write $\mathrm{\Gamma }$-sym-IPS to mean the proof system allowing only $\mathrm{\Gamma }$-symmetric proofs. Of course, this only makes sense for sets $ℱ$ of polynomials that are $\mathrm{\Gamma }$-invariant. For these, as we show below, $\mathrm{\Gamma }$-sym-IPS is a complete proof system. Where $\mathrm{\Gamma }$ is clear from context, we may write just sym-IPS.

Let $\mathrm{\Gamma }$ and ${\mathrm{\Gamma }}^{\prime }$ be groups acting on $X$ with $\mathrm{\Gamma }\le {\mathrm{\Gamma }}^{\prime }$. We say that ${\mathrm{\Gamma }}^{\prime }$-sym-IPS $p$-simulates $\mathrm{\Gamma }$-sym-IPS if for every ${\mathrm{\Gamma }}^{\prime }$-invariant $ℱ$ and a $\mathrm{\Gamma }$-sym-IPS refutation $C$ of $ℱ$, there is a ${\mathrm{\Gamma }}^{\prime }$-sym-IPS refutation of $ℱ$ with size polynomial in the size of $C$. We also use this notion of $p$-simulation in the context of restricted proof systems, such as linear or bounded degree systems. For instance, in Theorem 7 below, we show that (in suitably defined cases) ${\mathrm{deg}}_k\text{-}\mathrm{IPS}{\le }_p{\mathrm{deg}}_k\text{-}\mathrm{sym}\text{-}\mathrm{IPS}$. This means that for each $k$, there is a fixed polynomial $p$ such that whenever a $\mathrm{\Gamma }$-invariant $ℱ$ has any (i.e. $\{\mathrm{id}\}$-symmetric) IPS proof of size $n$ and degree $k$, it also has a $\mathrm{\Gamma }$-symmetric IPS proof of size $p(n)$ and degree $k$.

We now turn to other well-studied symmetry-invariant formalisms and show that they are subsumed by the symmetric IPS in a certain sense. These formalisms are logics from finite model theory, specifically fixed-point logic with counting (FPC) and Choiceless Polynomial Time (CPT). Drawing on previous work [29, 27], we show how their expressive power relates to the power of sym-IPS, specifically with respect to the graph isomorphism problem.