Quantum Automating TC0-Frege Is LWE-Hard

Noel Arteche; Gaia Carenini; Matthew Gray

doi:10.4230/LIPIcs.CCC.2024.15

Quantum Automating TC⁰-Frege Is LWE-Hard

Noel Arteche^*, Gaia Carenini, Matthew Gray

^*Corresponding author for this work

Algorithms and Complexity

Research output: Contribution to journal › Conference article › Research › peer-review

3 Citations (Scopus)

13 Downloads (Pure)

Abstract

We prove the first hardness results against efficient proof search by quantum algorithms. We show that under Learning with Errors (LWE), the standard lattice-based cryptographic assumption, no quantum algorithm can weakly automate TC⁰-Frege. This extends the line of results of Krajíček and Pudlák (Information and Computation, 1998), Bonet, Pitassi, and Raz (FOCS, 1997), and Bonet, Domingo, Gavaldà, Maciel, and Pitassi (Computational Complexity, 2004), who showed that Extended Frege, TC⁰-Frege and AC⁰-Frege, respectively, cannot be weakly automated by classical algorithms if either the RSA cryptosystem or the Diffie-Hellman key exchange protocol are secure. To the best of our knowledge, this is the first interaction between quantum computation and propositional proof search.

Original language	English
Article number	15
Journal	Leibniz International Proceedings in Informatics, LIPIcs
Volume	300
Number of pages	25
ISSN	1868-8969
DOIs	https://doi.org/10.4230/LIPIcs.CCC.2024.15
Publication status	Published - 2024
Event	39th Computational Complexity Conference, CCC 2024 - Ann Arbor, United States Duration: 22 Jul 2024 → 25 Jul 2024

Conference

Conference	39th Computational Complexity Conference, CCC 2024
Country/Territory	United States
City	Ann Arbor
Period	22/07/2024 → 25/07/2024

Bibliographical note

Funding Information:
Noel Arteche: This work was supported by the Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation. The question of the quantum non-automatability of strong proof systems was suggested to us by three different people. We thank Vijay Ganesh for bringing it up during the Dagstuhl Seminar 22411 Theory and Practice of SAT and Combinatorial Solving. We thank Susanna F. de Rezende for bringing our attention to the problem later and for insightful comments and careful proofreading. We would also like to thank J\u00E1n Pich for pointing us to the problem and discussing many details with us. We are particularly grateful for him directing us to the work of Soltys and Cook on LA. We also thank Rahul Santhanam for his insights and conversations and Yanyi Liu for pointing us to the existence of the certificates of injectivity. We also thank Mar\u00EDa Luisa Bonet, Jonas Conneryd, Ronald de Wolf, Eli Goldin, Peter Hall, Russell Impagliazzo, Erfan Khaniki, Alex Lombardi, Daniele Micciancio, Angelos Pelecanos and Michael Soltys for useful comments, suggestions and pointers. A preliminary version of this work was presented at the poster session of QIP 2024. We are thankful to the anonymous reviewers and their suggestions. We are also grateful to the anonymous CCC reviewers for their comments and particularly for observing that some crucial axioms were missing from the definition of LAQ in an earlier version of this work. This work was done in part while the authors were visiting the Simons Institute for the Theory of Computing at UC Berkeley during the spring of 2023 for the Meta-Complexity and Extended Reunion: Satisfiability programs.

Publisher Copyright:
© Noel Arteche, Gaia Carenini, and Matthew Gray.

Keywords

automatability
feasible interpolation
post-quantum cryptography

Access to Document

10.4230/LIPIcs.CCC.2024.15Licence: CC BY

FulltextFinal published version, 983 KBLicence: CC BY

Library access?

Check availability at the Royal Danish Library

Cite this

@inproceedings{95a789065631445ab280d5300e38d278,

title = "Quantum Automating TC0-Frege Is LWE-Hard",

abstract = "We prove the first hardness results against efficient proof search by quantum algorithms. We show that under Learning with Errors (LWE), the standard lattice-based cryptographic assumption, no quantum algorithm can weakly automate TC0-Frege. This extends the line of results of Kraj{\'i}{\v c}ek and Pudl{\'a}k (Information and Computation, 1998), Bonet, Pitassi, and Raz (FOCS, 1997), and Bonet, Domingo, Gavald{\`a}, Maciel, and Pitassi (Computational Complexity, 2004), who showed that Extended Frege, TC0-Frege and AC0-Frege, respectively, cannot be weakly automated by classical algorithms if either the RSA cryptosystem or the Diffie-Hellman key exchange protocol are secure. To the best of our knowledge, this is the first interaction between quantum computation and propositional proof search.",

keywords = "automatability, feasible interpolation, post-quantum cryptography",

author = "Noel Arteche and Gaia Carenini and Matthew Gray",

note = "Funding Information: Noel Arteche: This work was supported by the Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation. The question of the quantum non-automatability of strong proof systems was suggested to us by three different people. We thank Vijay Ganesh for bringing it up during the Dagstuhl Seminar 22411 Theory and Practice of SAT and Combinatorial Solving. We thank Susanna F. de Rezende for bringing our attention to the problem later and for insightful comments and careful proofreading. We would also like to thank J\u00E1n Pich for pointing us to the problem and discussing many details with us. We are particularly grateful for him directing us to the work of Soltys and Cook on LA. We also thank Rahul Santhanam for his insights and conversations and Yanyi Liu for pointing us to the existence of the certificates of injectivity. We also thank Mar\u00EDa Luisa Bonet, Jonas Conneryd, Ronald de Wolf, Eli Goldin, Peter Hall, Russell Impagliazzo, Erfan Khaniki, Alex Lombardi, Daniele Micciancio, Angelos Pelecanos and Michael Soltys for useful comments, suggestions and pointers. A preliminary version of this work was presented at the poster session of QIP 2024. We are thankful to the anonymous reviewers and their suggestions. We are also grateful to the anonymous CCC reviewers for their comments and particularly for observing that some crucial axioms were missing from the definition of LAQ in an earlier version of this work. This work was done in part while the authors were visiting the Simons Institute for the Theory of Computing at UC Berkeley during the spring of 2023 for the Meta-Complexity and Extended Reunion: Satisfiability programs. Publisher Copyright: {\textcopyright} Noel Arteche, Gaia Carenini, and Matthew Gray.; 39th Computational Complexity Conference, CCC 2024 ; Conference date: 22-07-2024 Through 25-07-2024",

year = "2024",

doi = "10.4230/LIPIcs.CCC.2024.15",

language = "English",

volume = "300",

journal = "Leibniz International Proceedings in Informatics, LIPIcs",

issn = "1868-8969",

publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH",

}

TY - GEN

T1 - Quantum Automating TC0-Frege Is LWE-Hard

AU - Arteche, Noel

AU - Carenini, Gaia

AU - Gray, Matthew

N1 - Funding Information: Noel Arteche: This work was supported by the Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation. The question of the quantum non-automatability of strong proof systems was suggested to us by three different people. We thank Vijay Ganesh for bringing it up during the Dagstuhl Seminar 22411 Theory and Practice of SAT and Combinatorial Solving. We thank Susanna F. de Rezende for bringing our attention to the problem later and for insightful comments and careful proofreading. We would also like to thank J\u00E1n Pich for pointing us to the problem and discussing many details with us. We are particularly grateful for him directing us to the work of Soltys and Cook on LA. We also thank Rahul Santhanam for his insights and conversations and Yanyi Liu for pointing us to the existence of the certificates of injectivity. We also thank Mar\u00EDa Luisa Bonet, Jonas Conneryd, Ronald de Wolf, Eli Goldin, Peter Hall, Russell Impagliazzo, Erfan Khaniki, Alex Lombardi, Daniele Micciancio, Angelos Pelecanos and Michael Soltys for useful comments, suggestions and pointers. A preliminary version of this work was presented at the poster session of QIP 2024. We are thankful to the anonymous reviewers and their suggestions. We are also grateful to the anonymous CCC reviewers for their comments and particularly for observing that some crucial axioms were missing from the definition of LAQ in an earlier version of this work. This work was done in part while the authors were visiting the Simons Institute for the Theory of Computing at UC Berkeley during the spring of 2023 for the Meta-Complexity and Extended Reunion: Satisfiability programs. Publisher Copyright: © Noel Arteche, Gaia Carenini, and Matthew Gray.

PY - 2024

Y1 - 2024

N2 - We prove the first hardness results against efficient proof search by quantum algorithms. We show that under Learning with Errors (LWE), the standard lattice-based cryptographic assumption, no quantum algorithm can weakly automate TC0-Frege. This extends the line of results of Krajíček and Pudlák (Information and Computation, 1998), Bonet, Pitassi, and Raz (FOCS, 1997), and Bonet, Domingo, Gavaldà, Maciel, and Pitassi (Computational Complexity, 2004), who showed that Extended Frege, TC0-Frege and AC0-Frege, respectively, cannot be weakly automated by classical algorithms if either the RSA cryptosystem or the Diffie-Hellman key exchange protocol are secure. To the best of our knowledge, this is the first interaction between quantum computation and propositional proof search.

AB - We prove the first hardness results against efficient proof search by quantum algorithms. We show that under Learning with Errors (LWE), the standard lattice-based cryptographic assumption, no quantum algorithm can weakly automate TC0-Frege. This extends the line of results of Krajíček and Pudlák (Information and Computation, 1998), Bonet, Pitassi, and Raz (FOCS, 1997), and Bonet, Domingo, Gavaldà, Maciel, and Pitassi (Computational Complexity, 2004), who showed that Extended Frege, TC0-Frege and AC0-Frege, respectively, cannot be weakly automated by classical algorithms if either the RSA cryptosystem or the Diffie-Hellman key exchange protocol are secure. To the best of our knowledge, this is the first interaction between quantum computation and propositional proof search.

KW - automatability

KW - feasible interpolation

KW - post-quantum cryptography

U2 - 10.4230/LIPIcs.CCC.2024.15

DO - 10.4230/LIPIcs.CCC.2024.15

M3 - Conference article

AN - SCOPUS:85199394442

SN - 1868-8969

VL - 300

JO - Leibniz International Proceedings in Informatics, LIPIcs

JF - Leibniz International Proceedings in Informatics, LIPIcs

M1 - 15

T2 - 39th Computational Complexity Conference, CCC 2024

Y2 - 22 July 2024 through 25 July 2024

ER -