ECCC-Report TR22-141https://eccc.weizmann.ac.il/report/2022/141Comments and Revisions published for TR22-141en-usWed, 30 Nov 2022 03:22:34 +0200
Revision 2
| TFNP Characterizations of Proof Systems and Monotone Circuits |
Noah Fleming,
Sam Buss,
Russell Impagliazzo
https://eccc.weizmann.ac.il/report/2022/141#revision2Connections 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 low communication. 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.
As an example, we provide a TFNP characterization of the Polynomial Calculus, answering a question of Goos et al., and show that it can prove its own soundness.Wed, 30 Nov 2022 03:22:34 +0200https://eccc.weizmann.ac.il/report/2022/141#revision2
Revision 1
| TFNP Characterizations of Proof Systems and Monotone Circuits |
Noah Fleming,
Sam Buss,
Russell Impagliazzo
https://eccc.weizmann.ac.il/report/2022/141#revision1Connections 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 low communication. 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.
As an example, we provide a TFNP characterization of the Polynomial Calculus, answering a question of Goos et al., and show that it can prove its own soundness.Sun, 27 Nov 2022 20:14:03 +0200https://eccc.weizmann.ac.il/report/2022/141#revision1
Paper TR22-141
| TFNP Characterizations of Proof Systems and Monotone Circuits |
Noah Fleming,
Sam Buss,
Russell Impagliazzo
https://eccc.weizmann.ac.il/report/2022/141Connections 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 low communication. 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.
As an example, we provide a TFNP characterization of the Polynomial Calculus, answering a question of Goos et al., and show that it can prove its own soundness.Sun, 23 Oct 2022 04:10:16 +0300https://eccc.weizmann.ac.il/report/2022/141