Revised: January 3, 2021

Published: November 1, 2021

**Keywords:**proof complexity, algebraic circuit complexity, lower bounds, algebraic proof systems, IPS, polynomial calculus, hardness versus randomness, functional lower bounds, ABPs

**Categories:**complexity theory, lower bounds, proof complexity, algebraic complexity, algebraic circuits, algebraic proof systems, IPS, polynomial calculus, hardness versus randomness, functional lower bounds, ABPs, CCC, CCC 2016 special issue

**ACM Classification:**F.1.3, F.1.2

**AMS Classification:**68Q17, 68Q15, 03F20

**Abstract:**
[Plain Text Version]

We give upper and lower bounds on the power of subsystems of the *Ideal Proof System (IPS)*, the algebraic proof system recently proposed by
Grochow and Pitassi (J. ACM, 2018),
where the circuits comprising the proof come from various restricted algebraic circuit classes. This mimics an established research direction in the Boolean setting for subsystems of *Extended Frege* proofs, where proof-lines are circuits from restricted Boolean circuit classes. Except one, all of the subsystems considered in this paper can simulate the well-studied *Nullstellensatz* proof system, and prior to this work there were no known lower bounds when measuring proof size by the algebraic complexity of the polynomials (except with respect to degree, or to sparsity).

We give two general methods of converting certain algebraic circuit lower bounds into proof complexity ones. However, we need to strengthen existing lower bounds to hold for either the *functional* model or for *multiplicities* (see below). Our techniques are reminiscent of existing methods for converting Boolean circuit lower bounds into related proof complexity results, such as *feasible interpolation*. We obtain the relevant types of lower bounds for a variety of classes (*sparse polynomials*, *depth-3 powering formulas*, *read-once oblivious algebraic branching programs*, and *multilinear formulas*), and infer the relevant proof complexity results. We complement our lower bounds by giving short refutations of the
previously studied
*subset-sum* axiom using IPS subsystems, allowing us to conclude strict separations between some of these subsystems.

Our first method is a *functional lower bound*, a notion due to
Grigoriev and Razborov (Appl. Algebra Eng. Commun. Comput., 2000),
which says that not only does a polynomial $f$ require large algebraic circuits, but that *any* polynomial $g$
agreeing with $f$ on the Boolean cube also requires large algebraic circuits. For our classes of interest, we develop functional lower bounds where
$g(\vx)$ equals
$1/p(\vx)$
where $p$ is a constant-degree polynomial, which in turn yield corresponding IPS lower bounds for proving that $p$ is nonzero over the Boolean cube. In particular, we show superpolynomial lower bounds for refuting variants of the subset-sum axiom in various IPS subsystems.

Our second method is to give *lower bounds for multiples*, that is, to give explicit polynomials whose all (nonzero) multiples require large algebraic circuit complexity. By extending known techniques, we are able to obtain such lower bounds for our classes of interest, which we then use to derive corresponding IPS lower bounds. Such lower bounds for multiples are of independent interest, as they have tight connections with the algebraic hardness versus randomness paradigm.

----------------

A conference version of this paper appeared in the Proceedings of the 31st Computational Complexity Conference (CCC'16).