__Preprint:__

**
Sam Buss, Noah Fleming, and Russell Impagliazzo
TFNP Characterizations of Proof Systems and
Monotone Circuits
In: Proc. Innovations in Theoretical Computer Science (ITCS),
January 2023.
LIPIcs volume 251, 30:1-30, 2023..
**

**
Download
ITCS conference version.
**

**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.
In this paper we begin to develop a more systematic understanding of
when these connections to TFNP occur. We give exact conditions
under which a proof system or circuit model admits a characterization
by a TFNP problem. We show:

- Every well-behaved proof system which can prove its
own soundness (a
*reflection principle*) is characterized by a TFNP problem. Conversely, every TFNP problem gives rise to a well-behaved proof system which proves its own soundness. - Every well-behaved monotone circuit model which
admits a
*universal family*of functions is characterized by a TFNP problem. Conversely, every TFNP problem gives rise to a well-behaved monotone circuit model with a universal problem.