Jump operators, interactive proofs and proof complexity generators

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F24%3A00604013" target="_blank" >RIV/67985840:_____/24:00604013 - isvavai.cz</a>

Výsledek na webu

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

DOI - Digital Object Identifier

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

Jazyk výsledku

angličtina

Název v původním jazyce

Jump operators, interactive proofs and proof complexity generators

Popis výsledku v původním jazyce

A jump operator J in proof complexity is a function such that for any proof system P, J(P) is a proof system that P cannot simulate. Some candidate jump operators were proposed by Krajicek and Pudlak [63] and Krajicek [57], but it is an open problem whether computable jump operators exist or not. In this regard, we introduce a new candidate jump operator based on the power of interactive proofs which given a proof system P, [I P, P] (I P-randomized implicit proof system based on P) is an M A proof system. In the first step, we investigate the relationship between IP - randomized implicit proof systems and Cook-Reckhow proof systems. In particular, we show that if i EF (Krajicek's implicit Extended Frege) proves exponential hard on average circuit lower bounds efficiently, then i E F simulates [IP, EF]. Moreover, we show that IP-randomized implicit proof systems can be used to prove new connections between different well-studied concepts in complexity theory. Namely, we prove new results about the hardness magnification in proof complexity, the hardness of proving proof complexity lower bounds, the automatability and the feasible disjunction property for Extended Frege using IP - randomized implicit proof systems. One ingredient of our proofs is a formalization of the sum-check protocol [65] in S21 which might be of independent interest. We also look at the general theory of jump operators and consider an old conjecture by Pudlak [78] about finite consistency sentences for first-order theories of arithmetic. In this direction, we prove that certain statements are equivalent, in particular, we prove that the widely believed assumption about the existence of computable jump operators in proof complexity is equivalent to a weaker form of Pudlak's conjecture.

Název v anglickém jazyce

Jump operators, interactive proofs and proof complexity generators

Popis výsledku anglicky

A jump operator J in proof complexity is a function such that for any proof system P, J(P) is a proof system that P cannot simulate. Some candidate jump operators were proposed by Krajicek and Pudlak [63] and Krajicek [57], but it is an open problem whether computable jump operators exist or not. In this regard, we introduce a new candidate jump operator based on the power of interactive proofs which given a proof system P, [I P, P] (I P-randomized implicit proof system based on P) is an M A proof system. In the first step, we investigate the relationship between IP - randomized implicit proof systems and Cook-Reckhow proof systems. In particular, we show that if i EF (Krajicek's implicit Extended Frege) proves exponential hard on average circuit lower bounds efficiently, then i E F simulates [IP, EF]. Moreover, we show that IP-randomized implicit proof systems can be used to prove new connections between different well-studied concepts in complexity theory. Namely, we prove new results about the hardness magnification in proof complexity, the hardness of proving proof complexity lower bounds, the automatability and the feasible disjunction property for Extended Frege using IP - randomized implicit proof systems. One ingredient of our proofs is a formalization of the sum-check protocol [65] in S21 which might be of independent interest. We also look at the general theory of jump operators and consider an old conjecture by Pudlak [78] about finite consistency sentences for first-order theories of arithmetic. In this direction, we prove that certain statements are equivalent, in particular, we prove that the widely believed assumption about the existence of computable jump operators in proof complexity is equivalent to a weaker form of Pudlak's conjecture.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

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

Projekt

<a href="/cs/project/GX19-27871X" target="_blank" >GX19-27871X: Efektivní aproximační algoritmy a obvodová složitost</a><br>

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2024

Kód důvěrnosti údajů

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

Název statě ve sborníku

2024 IEEE 65th Annual Symposium on Foundations of Computer Science (FOCS)

ISBN

979-833151674-1

ISSN

0272-5428

e-ISSN

—

Počet stran výsledku

21

Strana od-do

573-593

Název nakladatele

IEEE

Místo vydání

Philadelphia

Místo konání akce

Chicago

Datum konání akce

27. 10. 2024

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

001419526400035