Proof complexity lower bounds from algebraic circuit complexity. / Forbes, Michael; Shpilka, Amir; Tzameret, Iddo; Wigderson, Avi.

31st Conference on Computational Complexity (CCC 2016). Vol. 50 Dagstuhl, Germany : Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2016. p. 1-17 (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 50).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Published

Standard

Proof complexity lower bounds from algebraic circuit complexity. / Forbes, Michael; Shpilka, Amir; Tzameret, Iddo; Wigderson, Avi.

31st Conference on Computational Complexity (CCC 2016). Vol. 50 Dagstuhl, Germany : Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2016. p. 1-17 (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 50).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Harvard

Forbes, M, Shpilka, A, Tzameret, I & Wigderson, A 2016, Proof complexity lower bounds from algebraic circuit complexity. in 31st Conference on Computational Complexity (CCC 2016). vol. 50, Leibniz International Proceedings in Informatics (LIPIcs), vol. 50, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, pp. 1-17, Computational Complexity Conference (CCC), Koyto, Japan, 29/05/16. https://doi.org/10.4230/LIPIcs.CCC.2016.32

APA

Forbes, M., Shpilka, A., Tzameret, I., & Wigderson, A. (2016). Proof complexity lower bounds from algebraic circuit complexity. In 31st Conference on Computational Complexity (CCC 2016) (Vol. 50, pp. 1-17). (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 50). Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. https://doi.org/10.4230/LIPIcs.CCC.2016.32

Vancouver

Forbes M, Shpilka A, Tzameret I, Wigderson A. Proof complexity lower bounds from algebraic circuit complexity. In 31st Conference on Computational Complexity (CCC 2016). Vol. 50. Dagstuhl, Germany: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. 2016. p. 1-17. (Leibniz International Proceedings in Informatics (LIPIcs)). https://doi.org/10.4230/LIPIcs.CCC.2016.32

Author

Forbes, Michael ; Shpilka, Amir ; Tzameret, Iddo ; Wigderson, Avi. / Proof complexity lower bounds from algebraic circuit complexity. 31st Conference on Computational Complexity (CCC 2016). Vol. 50 Dagstuhl, Germany : Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2016. pp. 1-17 (Leibniz International Proceedings in Informatics (LIPIcs)).

BibTeX

@inproceedings{c3b6f372410443e5847cb777cecf7c95,
title = "Proof complexity lower bounds from algebraic circuit complexity",
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~\cite{GrochowPitassi14}, 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 Frege proofs whose lines are circuits from restricted boolean circuit classes. Essentially 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).Our main contributions are two general methods of converting certain algebraic lower bounds into proof complexity ones. Both require stronger arithmetic lower bounds than common, which should hold not for a specific polynomial but for a whole family defined by it.These may be likened to some of the methods by which Boolean circuit lower bounds are turned into related proof-complexity ones, especially the ``feasible interpolation'' technique. We establish algebraic lower bounds of these forms for several explicit polynomials, against a variety of classes, and infer the relevant proof complexity bounds. These yield separations between IPS subsystems, which we complement by simulations to create a partial structure theory for IPS systems.Our first method is a \emph{functional lower bound}, a notion of Grigoriev and Razborov~\cite{GrigorievRazborov00}, which is a function $\hat{f}:\bits^n\to\F$ such that any polynomial $f$ agreeing with $\hat{f}$ on the boolean cube requires large algebraic circuit complexity. We develop functional lower bounds for a variety of circuit classes (sparse polynomials, depth-3 powering formulas, roABPs and multilinear formulas) where $\hat{f}(\vx)$ equals $\nicefrac{1}{p(\vx)}$ for a constant-degree polynomial $p$ depending on the relevant circuit class. We believe these lower bounds are of independent interest in algebraic complexity, and show that they also imply lower bounds for the size of the corresponding IPS refutations for proving that the relevant polynomial $p$ is non-zero over the boolean cube. In particular, we show super-polynomial lower bounds for refuting variants of the subset-sum axioms in these IPS subsystems.Our second method is to give \emph{lower bounds for multiples}, that is, to give explicit polynomials whose all (non-zero) multiples require large algebraic circuit complexity. By extending known techniques, we give lower bounds for multiples for various restricted circuit classes such sparse polynomials, sums of powers of low-degree polynomials, and roABPs. These results are of independent interest, as we argue that lower bounds for multiples is the correct notion for instantiating the algebraic hardness versus randomness paradigm of Kabanets and Impagliazzo~\cite{KabanetsImpagliazzo04}. Further, we show how such lower bounds for multiples extend to lower bounds for refutations in the corresponding IPS subsystem.",
keywords = "complexity theory",
author = "Michael Forbes and Amir Shpilka and Iddo Tzameret and Avi Wigderson",
year = "2016",
month = may,
day = "19",
doi = "10.4230/LIPIcs.CCC.2016.32",
language = "English",
isbn = "978-3-95977-008-8",
volume = "50",
series = "Leibniz International Proceedings in Informatics (LIPIcs)",
publisher = "Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik",
pages = "1--17",
booktitle = "31st Conference on Computational Complexity (CCC 2016)",
note = "Computational Complexity Conference (CCC) ; Conference date: 29-05-2016 Through 01-06-2016",

}

RIS

TY - GEN

T1 - Proof complexity lower bounds from algebraic circuit complexity

AU - Forbes, Michael

AU - Shpilka, Amir

AU - Tzameret, Iddo

AU - Wigderson, Avi

PY - 2016/5/19

Y1 - 2016/5/19

N2 - 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~\cite{GrochowPitassi14}, 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 Frege proofs whose lines are circuits from restricted boolean circuit classes. Essentially 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).Our main contributions are two general methods of converting certain algebraic lower bounds into proof complexity ones. Both require stronger arithmetic lower bounds than common, which should hold not for a specific polynomial but for a whole family defined by it.These may be likened to some of the methods by which Boolean circuit lower bounds are turned into related proof-complexity ones, especially the ``feasible interpolation'' technique. We establish algebraic lower bounds of these forms for several explicit polynomials, against a variety of classes, and infer the relevant proof complexity bounds. These yield separations between IPS subsystems, which we complement by simulations to create a partial structure theory for IPS systems.Our first method is a \emph{functional lower bound}, a notion of Grigoriev and Razborov~\cite{GrigorievRazborov00}, which is a function $\hat{f}:\bits^n\to\F$ such that any polynomial $f$ agreeing with $\hat{f}$ on the boolean cube requires large algebraic circuit complexity. We develop functional lower bounds for a variety of circuit classes (sparse polynomials, depth-3 powering formulas, roABPs and multilinear formulas) where $\hat{f}(\vx)$ equals $\nicefrac{1}{p(\vx)}$ for a constant-degree polynomial $p$ depending on the relevant circuit class. We believe these lower bounds are of independent interest in algebraic complexity, and show that they also imply lower bounds for the size of the corresponding IPS refutations for proving that the relevant polynomial $p$ is non-zero over the boolean cube. In particular, we show super-polynomial lower bounds for refuting variants of the subset-sum axioms in these IPS subsystems.Our second method is to give \emph{lower bounds for multiples}, that is, to give explicit polynomials whose all (non-zero) multiples require large algebraic circuit complexity. By extending known techniques, we give lower bounds for multiples for various restricted circuit classes such sparse polynomials, sums of powers of low-degree polynomials, and roABPs. These results are of independent interest, as we argue that lower bounds for multiples is the correct notion for instantiating the algebraic hardness versus randomness paradigm of Kabanets and Impagliazzo~\cite{KabanetsImpagliazzo04}. Further, we show how such lower bounds for multiples extend to lower bounds for refutations in the corresponding IPS subsystem.

AB - 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~\cite{GrochowPitassi14}, 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 Frege proofs whose lines are circuits from restricted boolean circuit classes. Essentially 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).Our main contributions are two general methods of converting certain algebraic lower bounds into proof complexity ones. Both require stronger arithmetic lower bounds than common, which should hold not for a specific polynomial but for a whole family defined by it.These may be likened to some of the methods by which Boolean circuit lower bounds are turned into related proof-complexity ones, especially the ``feasible interpolation'' technique. We establish algebraic lower bounds of these forms for several explicit polynomials, against a variety of classes, and infer the relevant proof complexity bounds. These yield separations between IPS subsystems, which we complement by simulations to create a partial structure theory for IPS systems.Our first method is a \emph{functional lower bound}, a notion of Grigoriev and Razborov~\cite{GrigorievRazborov00}, which is a function $\hat{f}:\bits^n\to\F$ such that any polynomial $f$ agreeing with $\hat{f}$ on the boolean cube requires large algebraic circuit complexity. We develop functional lower bounds for a variety of circuit classes (sparse polynomials, depth-3 powering formulas, roABPs and multilinear formulas) where $\hat{f}(\vx)$ equals $\nicefrac{1}{p(\vx)}$ for a constant-degree polynomial $p$ depending on the relevant circuit class. We believe these lower bounds are of independent interest in algebraic complexity, and show that they also imply lower bounds for the size of the corresponding IPS refutations for proving that the relevant polynomial $p$ is non-zero over the boolean cube. In particular, we show super-polynomial lower bounds for refuting variants of the subset-sum axioms in these IPS subsystems.Our second method is to give \emph{lower bounds for multiples}, that is, to give explicit polynomials whose all (non-zero) multiples require large algebraic circuit complexity. By extending known techniques, we give lower bounds for multiples for various restricted circuit classes such sparse polynomials, sums of powers of low-degree polynomials, and roABPs. These results are of independent interest, as we argue that lower bounds for multiples is the correct notion for instantiating the algebraic hardness versus randomness paradigm of Kabanets and Impagliazzo~\cite{KabanetsImpagliazzo04}. Further, we show how such lower bounds for multiples extend to lower bounds for refutations in the corresponding IPS subsystem.

KW - complexity theory

U2 - 10.4230/LIPIcs.CCC.2016.32

DO - 10.4230/LIPIcs.CCC.2016.32

M3 - Conference contribution

SN - 978-3-95977-008-8

VL - 50

T3 - Leibniz International Proceedings in Informatics (LIPIcs)

SP - 1

EP - 17

BT - 31st Conference on Computational Complexity (CCC 2016)

PB - Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik

CY - Dagstuhl, Germany

T2 - Computational Complexity Conference (CCC)

Y2 - 29 May 2016 through 1 June 2016

ER -