TFNP characterizations of proof systems and monotone circuits
Buss, Sam ; Fleming, Noah LU
and Impagliazzo, Russell
(2023)
In Leibniz International Proceedings in Informatics (LIPIcs)
251.
- Abstract
- Connections between proof complexity and circuit complexity have become major tools for obtaining lower bounds in both areas. These connections – which take the form of interpolation theorems and query-to-communication lifting theorems – translate efficient proofs into small circuits, and vice versa, allowing tools from one area to be applied to the other. Recently, the theory of TFNP has emerged as a unifying framework underlying these connections. For many of the proof systems which admit such a connection there is a TFNP problem which characterizes it: the class of problems which are reducible to this TFNP problem via query-efficient reductions is equivalent to the tautologies that can be efficiently proven in the system. Through this,... (More)
- Connections between proof complexity and circuit complexity have become major tools for obtaining lower bounds in both areas. These connections – which take the form of interpolation theorems and query-to-communication lifting theorems – translate efficient proofs into small circuits, and vice versa, allowing tools from one area to be applied to the other. Recently, the theory of TFNP has emerged as a unifying framework underlying these connections. For many of the proof systems which admit such a connection there is a TFNP problem which characterizes it: the class of problems which are reducible to this TFNP problem via query-efficient reductions is equivalent to the tautologies that can be efficiently proven in the system. Through this, proof complexity has become a major tool for proving separations in black-box TFNP. Similarly, for certain monotone circuit models, the class of functions that it can compute efficiently is equivalent to what can be reduced to a certain TFNP problem in a communication-efficient manner. When a TFNP problem has both a proof and circuit characterization, one can prove an interpolation theorem. Conversely, many lifting theorems can be viewed as relating the communication and query reductions to TFNP problems. This is exciting, as it suggests that TFNP provides a roadmap for the development of further interpolation theorems and lifting theorems. (Less)
Please use this url to cite or link to this publication:
https://lup.lub.lu.se/record/750e6b68-04a2-4474-86d9-acb5135f7923
- author
- Buss, Sam
; Fleming, Noah
LU
and Impagliazzo, Russell
- publishing date
- 2023
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- host publication
- 14th Innovations in Theoretical Computer Science Conference (ITCS 2023)
- series title
- Leibniz International Proceedings in Informatics (LIPIcs)
- volume
- 251
- pages
- 40 pages
- publisher
- Schloss Dagstuhl - Leibniz-Zentrum für Informatik
- ISSN
- 1868-8969
- language
- English
- LU publication?
- no
- id
- 750e6b68-04a2-4474-86d9-acb5135f7923
- alternative location
- https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2023.30
- date added to LUP
- 2025-10-28 20:30:21
- date last changed
- 2025-11-04 16:40:43
@inproceedings{750e6b68-04a2-4474-86d9-acb5135f7923,
abstract = {{Connections between proof complexity and circuit complexity have become major tools for obtaining lower bounds in both areas. These connections – which take the form of interpolation theorems and query-to-communication lifting theorems – translate efficient proofs into small circuits, and vice versa, allowing tools from one area to be applied to the other. Recently, the theory of TFNP has emerged as a unifying framework underlying these connections. For many of the proof systems which admit such a connection there is a TFNP problem which characterizes it: the class of problems which are reducible to this TFNP problem via query-efficient reductions is equivalent to the tautologies that can be efficiently proven in the system. Through this, proof complexity has become a major tool for proving separations in black-box TFNP. Similarly, for certain monotone circuit models, the class of functions that it can compute efficiently is equivalent to what can be reduced to a certain TFNP problem in a communication-efficient manner. When a TFNP problem has both a proof and circuit characterization, one can prove an interpolation theorem. Conversely, many lifting theorems can be viewed as relating the communication and query reductions to TFNP problems. This is exciting, as it suggests that TFNP provides a roadmap for the development of further interpolation theorems and lifting theorems.}},
author = {{Buss, Sam and Fleming, Noah and Impagliazzo, Russell}},
booktitle = {{14th Innovations in Theoretical Computer Science Conference (ITCS 2023)}},
issn = {{1868-8969}},
language = {{eng}},
publisher = {{Schloss Dagstuhl - Leibniz-Zentrum für Informatik}},
series = {{Leibniz International Proceedings in Informatics (LIPIcs)}},
title = {{TFNP characterizations of proof systems and monotone circuits}},
url = {{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2023.30}},
volume = {{251}},
year = {{2023}},
}