[Proof Complexity] MIAO seminar Thu Jan 22 at 13:00 CET with Deniz Imrek: Separations above TFNP from Sherali-Adams lower bounds

[Jakob Nordström]

Dear all,

With apologies for the short notice, tomorrow Thursday January 22 at 13:00 CET (note the time!) we are happy to welcome Deniz Imrek from UT Austin, who will give a presentation titled "Separations above TFNP from Sherali-Adams lower bounds". You find the abstract at the bottom of this message.

We will run this as a MIAO hybrid seminar at Lund University. Local participants are warmly welcome to seminar room E:2405 at Ole Römers väg 3, while other participants are equally warmly welcome to join virtually at https://lu-se.zoom.us/j/61925271827 . Please feel free to share this information with colleagues who you think might be interested.

More information about the MIAO seminar series can be found at https://jakobnordstrom.se/miao-seminars/ . If you do not wish to receive these announcements, or receive several copies of them, please send a message to jn at di.ku.dk<mailto:jn at di.ku.dk>.

Best regards,
Jakob Nordström

**********

Thursday Jan 22 at 13:00 (note the time!) in seminar room E:2405, Ole Römers väg 3, Lund University, and on Zoom
Separations above TFNP from Sherali-Adams lower bounds
(Deniz Imrek, UT Austin)

Syntactical subclasses of black-box TFNP, the class of total, verifiable search problems, are known to be related to proof systems in the following way: A problem is in a subclass if and only if a specific proof system can efficiently prove that the problem is total. Using this relation and proof system lower bounds, every pair of the original TFNP subclasses introduced by Papadimitriou have now been shown to be inequal.

Recently, this link between TFNP and proof complexity was extended to the whole TFPH, the class of total search problems in the polynomial hierarchy. A TFΣ2 search problem, for example, can be verified by a coNP verifier. This new connection requires proof systems to have some extra power, in the sense of semantic weakening: A Σ2 proof system is allowed, before doing a regular proof, to semantically weaken every DNF it is working on.

Notably, Σ2 unary Sherali-Adams (Σ2 uSA) efficiently proves the totality of exactly the class of TFΣ2 problems that reduce to the Strong Range Avoidance problem. This problem has attracted a lot of attention recently, as its weak form has strong ties to recent circuit lower bounds.

In this work, we prove a Σ2 uSA lower bound for the Least Ordering Principles (LOP), exhibiting the first TFΣ2 problem that lies outside of the class of Strong Range Avoidance, and the first separation above TFNP using proof complexity. To do so, we build a pseudo-expectation that works for every semantic weakening of LOP. We show that each potential proof of a semantic weakening corresponds to some covering of total orders and prove that no such small covering exists.


Jakob Nordström, Professor
University of Copenhagen and Lund University
Phone: +45 28 78 38 11 / +46 70 742 21 98
https://jakobnordstrom.se