 Library Home /
 Search Collections /
 Open Collections /
 Browse Collections /
 BIRS Workshop Lecture Videos /
 and Edward Hirsch: SemiAlgebraic Proofs, IPS Lower...
Open Collections
BIRS Workshop Lecture Videos
BIRS Workshop Lecture Videos
and Edward Hirsch: SemiAlgebraic Proofs, IPS Lower Bounds and the $\tau$Conjecture: Can a Natural Number be Negative Tzameret, Iddo
Description
We introduce the binary value principle which is a simple subsetsum instance expressing that a natural number written in binary cannot be negative, relating it to central problems in proof and algebraic complexity. We prove conditional superpolynomial lower bounds on the Ideal Proof System (IPS) refutation size of this instance, based on a wellknown hypothesis by Shub and Smale about the hardness of computing factorials, where IPS is the strong algebraic proof system introduced by Grochow and Pitassi (2018). Conversely, we show that short IPS refutations of this instance bridge the gap between sufficiently strong algebraic and semialgebraic proof systems. Our results extend to fullfledged IPS the paradigm introduced in Forbes et al. (2016), whereby lower bounds against subsystems of IPS were obtained using restricted algebraic circuit lower bounds, and demonstrate that the binary value principle captures the advantage of semialgebraic over algebraic reasoning, for sufficiently strong systems. Specifically, we show the following: *Conditional IPS lower bounds:* The ShubSmale hypothesis (1995) implies a superpolynomial lower bound on the size of IPS refutations of the binary value principle over the rationals defined as the unsatisfiable linear equation $\sum_{i=1}^{n} 2^{i1}x_i = 1$, for boolean $x_i$'s. Further, the related $\tau$conjecture (1995) implies a superpolynomial lower bound on the size of IPS refutations of a variant of the binary value principle over the ring of rational functions. No prior conditional lower bounds were known for IPS or for apparently much weaker propositional proof systems such as Frege. *Algebraic vs. semialgebraic proofs:* Admitting short refutations of the binary value principle is necessary for any algebraic proof system to fully simulate any known semialgebraic proof system, and for strong enough algebraic proof systems it is also sufficient. In particular, we introduce a very strong proof system that simulates all known semialgebraic proof systems (and most other known concrete propositional proof systems), under the name Cone Proof System (CPS), as a semialgebraic analogue of the ideal proof system: CPS establishes the unsatisfiability of collections of polynomial equalities and inequalities over the reals, by representing sumofsquares proofs (and extensions) as algebraic circuits. We prove that IPS is polynomially equivalent to CPS iff IPS admits polynomialsize refutations of the binary value principle (for the language of systems of equations that have no 0/1solutions), over both $\mathbb{Z}$ and $\mathbb{Q}$. Joint work with Yaroslav Alekseev and Dima Grigoriev.
Item Metadata
Title 
and Edward Hirsch: SemiAlgebraic Proofs, IPS Lower Bounds and the $\tau$Conjecture: Can a Natural Number be Negative

Creator  
Publisher 
Banff International Research Station for Mathematical Innovation and Discovery

Date Issued 
20200121T10:01

Description 
We introduce the binary value principle which is a simple subsetsum instance expressing that a natural number written in binary cannot be negative, relating it to central problems in proof and algebraic complexity. We prove conditional superpolynomial lower bounds on the Ideal Proof System (IPS) refutation size of this instance, based on a wellknown hypothesis by Shub and Smale about the hardness of computing factorials, where IPS is the strong algebraic proof system introduced by Grochow and Pitassi (2018). Conversely, we show that short IPS refutations of this instance bridge the gap between sufficiently strong algebraic and semialgebraic proof systems. Our results extend to fullfledged IPS the paradigm introduced in Forbes et al. (2016), whereby lower bounds against subsystems of IPS were obtained using restricted algebraic circuit lower bounds, and demonstrate that the binary value principle captures the advantage of semialgebraic over algebraic reasoning, for sufficiently strong systems. Specifically, we show the following:
*Conditional IPS lower bounds:* The ShubSmale hypothesis (1995) implies a superpolynomial lower bound on the size of IPS refutations of the binary value principle over the rationals defined as the unsatisfiable linear equation $\sum_{i=1}^{n} 2^{i1}x_i = 1$, for boolean $x_i$'s. Further, the related $\tau$conjecture (1995) implies a superpolynomial lower bound on the size of IPS refutations of a variant of the binary value principle over the ring of rational functions. No prior conditional lower bounds were known for IPS or for apparently much weaker propositional proof systems such as Frege.
*Algebraic vs. semialgebraic proofs:* Admitting short refutations of the binary value principle is necessary for any algebraic proof system to fully simulate any known semialgebraic proof system, and for strong enough algebraic proof systems it is also sufficient. In particular, we introduce a very strong proof system that simulates all known semialgebraic proof systems (and most other known concrete propositional proof systems), under the name Cone Proof System (CPS), as a semialgebraic analogue of the ideal proof system: CPS establishes the unsatisfiability of collections of polynomial equalities and inequalities over the reals, by representing sumofsquares proofs (and extensions) as algebraic circuits. We prove that IPS is polynomially equivalent to CPS iff IPS admits polynomialsize refutations of the binary value principle (for the language of systems of equations that have no 0/1solutions), over both $\mathbb{Z}$ and $\mathbb{Q}$.
Joint work with Yaroslav Alekseev and Dima Grigoriev.

Extent 
60.0 minutes

Subject  
Type  
File Format 
video/mp4

Language 
eng

Notes 
Author affiliation: Royal Holloway, University of London

Series  
Date Available 
20200720

Provider 
Vancouver : University of British Columbia Library

Rights 
AttributionNonCommercialNoDerivatives 4.0 International

DOI 
10.14288/1.0392463

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