Why are proof complexity lower bounds hard?

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F19%3A00523286" target="_blank" >RIV/67985840:_____/19:00523286 - isvavai.cz</a>

Result on the web

<a href="http://dx.doi.org/10.1109/FOCS.2019.00080" target="_blank" >http://dx.doi.org/10.1109/FOCS.2019.00080</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1109/FOCS.2019.00080" target="_blank" >10.1109/FOCS.2019.00080</a>

Result language

angličtina

Original language name

Why are proof complexity lower bounds hard?

Original language description

We formalize and study the question of whether there are inherent difficulties to showing lower bounds on propositional proof complexity. We establish the following unconditional result: Propositional proof systems cannot efficiently show that truth tables of random Boolean functions lack polynomial size non-uniform proofs of hardness. Assuming a conjecture of Rudich, propositional proof systems also cannot efficiently show that random k-CNFs of linear density lack polynomial size non-uniform proofs of unsatisfiability. Since the statements in question assert the average-case hardness of standard NP problems (MCSP and 3-SAT respectively) against co-nondeterministic circuits for natural distributions, one interpretation of our result is that propositional proof systems are inherently incapable of efficiently proving strong complexity lower bounds in our formalization. Another interpretation is that an analogue of the Razborov-Rudich 'natural proofs' barrier holds in proof complexity: under reasonable hardness assumptions, there are natural distributions on hard tautologies for which it is infeasible to show proof complexity lower bounds for strong enough proof systems. For the specific case of the Extended Frege (EF) propositional proof system, we show that at least one of the following cases holds: (1) EF has no efficient proofs of superpolynomial circuit lower bound tautologies for any Boolean function or (2) There is an explicit family of tautologies of each length such that under reasonable hardness assumptions, most tautologies are hard but no propositional proof system can efficiently establish hardness for most tautologies in the family. Thus, under reasonable hardness assumptions, either the Circuit Lower Bounds program toward complexity separations cannot be implemented in EF, or there are inherent obstacles to implementing the Cook-Reckhow program for EF.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

<a href="/en/project/GA19-05497S" target="_blank" >GA19-05497S: Complexity of mathematical proofs and structures</a><br>

Continuities

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Publication year

2019

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

2019 IEEE 60th Annual Symposium on Foundations of Computer Science (FOCS 2019)

ISBN

978-1-7281-4952-3

ISSN

0272-5428

e-ISSN

—

Number of pages

20

Pages from-to

1305-1324

Publisher name

IEEE

Place of publication

Los Alamitos

Event location

Baltimore

Event date

Nov 9, 2019

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

000510015300071