- 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 well-known proof system is Hilbert’s Nullstellensatz, which shows that if the family F={f1,…,fm} of n-variate 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 well-known 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 subset-sum axiom require super-polynomially large proofs to prove their unsatisfiability when the size of the algebraic circuits are measured as read-once algebraic branching programs, sums of powers of low-degree 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 |
2016-09-07T11:08
|
Description |
Proof complexity studies the complexity of mathematical proofs, with the aim of exhibiting (true) statements whose proofs are always necessarily long. One well-known proof system is Hilbert’s Nullstellensatz, which shows that if the family F={f1,…,fm} of n-variate 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 well-known 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 subset-sum axiom require super-polynomially large proofs to prove their unsatisfiability when the size of the algebraic circuits are measured as read-once algebraic branching programs, sums of powers of low-degree 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 |
2017-03-09
|
Provider |
Vancouver : University of British Columbia Library
|
Rights |
Attribution-NonCommercial-NoDerivatives 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
Attribution-NonCommercial-NoDerivatives 4.0 International