Theory of Computing
-------------------
Title     : Proof Complexity Lower Bounds from Algebraic Circuit Complexity
Authors   : Michael A. Forbes, Amir Shpilka, Iddo Tzameret, and Avi Wigderson
Volume    : 17
Number    : 10
Pages     : 1-88
URL       : https://theoryofcomputing.org/articles/v017a010

Abstract
--------

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(\x)$ equals
$1/p(\x)$ 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).