 Library Home /
 Search Collections /
 Open Collections /
 Browse Collections /
 BIRS Workshop Lecture Videos /
 Proof complexity lower bounds from algebraic circuit...
Open Collections
BIRS Workshop Lecture Videos
BIRS Workshop Lecture Videos
Proof complexity lower bounds from algebraic circuit complexity Shpilka, Amir
Description
Proof complexity studies the complexity of mathematical proofs, with the aim of exhibiting (true) statements whose proofs are always necessarily long. One wellknown proof system is Hilbert’s Nullstellensatz, which shows that if the family F={f1,…,fm} of nvariate polynomials have no common solution to the system f1=…=fm=0, then there is a proof of this fact of the following form: there are polynomials G={g1,…,gm} such that f1.g1+…+fm.gm=1 is an identity. From the perspective of computer science, it is most natural to ask how succinctly one can express the proof G. Substantial work on the Nullstellensatz system has measured the complexity of G in terms of their degree or sparsity, and obtained the desired lower bounds for these measures. Grochow and Pitassqi have recently argued that it is natural to measure the complexity of G by the size needed to express them as algebraic circuits. They called the resulting system the Ideal Proof System (IPS), and showed that it captures the power of wellknown strong proof systems such as the Frege proof system, as well as showing that certain natural lower bounds for the size of IPS proofs would imply VP≠VNP, an algebraic analogue of P≠NP. This is in contrast to other proof systems, where direct ties to computational lower bounds are often lacking. Motivated by their work, we study the IPS proof system further. We first show that weak subsystems of IPS can be quite powerful. We then consider lower bounds for subclasses of IPS. We obtain certain extensions to existing lower bound techniques, obtaining "functional lower bounds" as well as "lower bounds for multiples". Using these extensions, we show that variants of the subsetsum axiom require superpolynomially large proofs to prove their unsatisfiability when the size of the algebraic circuits are measured as readonce algebraic branching programs, sums of powers of lowdegree polynomials, or multilinear formulas. No specific knowledge of proof complexity or algebraic circuit complexity will be assumed. Joint work with Michael Forbes, Iddo Tzameret, and Avi Wigderson.
Item Metadata
Title 
Proof complexity lower bounds from algebraic circuit complexity

Creator  
Publisher 
Banff International Research Station for Mathematical Innovation and Discovery

Date Issued 
20160907T11:08

Description 
Proof complexity studies the complexity of mathematical proofs, with the aim of exhibiting (true) statements whose proofs are always necessarily long. One wellknown proof system is Hilbert’s Nullstellensatz, which shows that if the family F={f1,…,fm} of nvariate polynomials have no common solution to the system f1=…=fm=0, then there is a proof of this fact of the following form: there are polynomials G={g1,…,gm} such that f1.g1+…+fm.gm=1 is an identity. From the perspective of computer science, it is most natural to ask how succinctly one can express the proof G.
Substantial work on the Nullstellensatz system has measured the complexity of G in terms of their degree or sparsity, and obtained the desired lower bounds for these measures. Grochow and Pitassqi have recently argued that it is natural to measure the complexity of G by the size needed to express them as algebraic circuits. They called the resulting system the Ideal Proof System (IPS), and showed that it captures the power of wellknown strong proof systems such as the Frege proof system, as well as showing that certain natural lower bounds for the size of IPS proofs would imply VP≠VNP, an algebraic analogue of P≠NP. This is in contrast to other proof systems, where direct ties to computational lower bounds are often lacking.
Motivated by their work, we study the IPS proof system further. We first show that weak subsystems of IPS can be quite powerful. We then consider lower bounds for subclasses of IPS. We obtain certain extensions to existing lower bound techniques, obtaining "functional lower bounds" as well as "lower bounds for multiples". Using these extensions, we show that variants of the subsetsum axiom require superpolynomially large proofs to prove their unsatisfiability when the size of the algebraic circuits are measured as readonce algebraic branching programs, sums of powers of lowdegree polynomials, or multilinear formulas. No specific knowledge of proof complexity or algebraic circuit complexity will be assumed.
Joint work with Michael Forbes, Iddo Tzameret, and Avi Wigderson.

Extent 
53 minutes

Subject  
Type  
File Format 
video/mp4

Language 
eng

Notes 
Author affiliation: Tel Aviv University

Series  
Date Available 
20170309

Provider 
Vancouver : University of British Columbia Library

Rights 
AttributionNonCommercialNoDerivatives 4.0 International

DOI 
10.14288/1.0343125

URI  
Affiliation  
Peer Review Status 
Unreviewed

Scholarly Level 
Faculty

Rights URI  
Aggregated Source Repository 
DSpace

Item Media
Item Citations and Data
Rights
AttributionNonCommercialNoDerivatives 4.0 International