Document Open Access Logo

Quantum Automating TC⁰-Frege Is LWE-Hard

Authors Noel Arteche , Gaia Carenini , Matthew Gray

PDF
Thumbnail PDF

File

LIPIcs.CCC.2024.15.pdf
  • Filesize: 0.96 MB
  • 25 pages

Document Identifiers

Author Details

Noel Arteche
  • Lund University, Sweden
  • University of Copenhagen, Denmark
Gaia Carenini
  • École Normale Supérieure (ENS-PSL), Paris, France
  • University of Cambridge, UK
Matthew Gray
  • University of Oxford, UK

Funding

  • Arteche, Noel: This work was supported by the Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation.

Acknowledgements

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án 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ía 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 LA_ℚ 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.

Cite As Get BibTex

Noel Arteche, Gaia Carenini, and Matthew Gray. Quantum Automating TC⁰-Frege Is LWE-Hard. In 39th Computational Complexity Conference (CCC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 300, pp. 15:1-15:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.CCC.2024.15

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
  • Theory of computation → Quantum complexity theory
Keywords
  • automatability
  • post-quantum cryptography
  • feasible interpolation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Dorit Aharonov and Oded Regev. Lattice problems in NP ∩ coNP. Journal of the ACM (JACM), 52(5):749-765, 2005. Google Scholar
  2. Miklós Ajtai. Generating hard instances of lattice problems. In Proceedings of the twenty-eighth annual ACM symposium on Theory of computing, pages 99-108, 1996. Google Scholar
  3. Miklós Ajtai and Cynthia Dwork. A public-key cryptosystem with worst-case/average-case equivalence. In Proceedings of the twenty-ninth annual ACM symposium on Theory of computing, pages 284-293, 1997. Google Scholar
  4. Michael Alekhnovich, Sam Buss, Shlomo Moran, and Toniann Pitassi. Minimum propositional proof length is NP-hard to linearly approximate. In Mathematical Foundations of Computer Science 1998: 23rd International Symposium, pages 176-184. Springer, 2006. Google Scholar
  5. Michael Alekhnovich and Alexander A Razborov. Resolution is not automatizable unless 𝐖[𝐏] is tractable. SIAM Journal on Computing, 38(4):1347-1363, 2008. Google Scholar
  6. Sanjeev Arora and Boaz Barak. Computational Complexity: A Modern Approach. Cambridge University Press, 2009. Google Scholar
  7. Noel Arteche, Gaia Carenini, and Matthew Gray. Quantum automating TC⁰-Frege is LWE-hard. Electronic Colloquium on Computational Complexity (ECCC), 2024. URL: https://eccc.weizmann.ac.il/report/2024/029/.
  8. Albert Atserias and María Luisa Bonet. On the automatizability of resolution and related propositional proof systems. Information and Computation, 189(2):182-201, 2004. Google Scholar
  9. Albert Atserias and Elitza Maneva. Mean-payoff games and propositional proofs. Information and Computation, 209(4):664-691, 2011. Google Scholar
  10. Albert Atserias and Moritz Müller. Automating resolution is NP-hard. Journal of the ACM (JACM), 67(5):1-17, 2020. Google Scholar
  11. Wojciech Banaszczyk. New bounds in some transference theorems in the geometry of numbers. Mathematische Annalen, 296:625-635, 1993. Google Scholar
  12. P. Beame and T. Pitassi. Simplified and improved resolution lower bounds. In Proceedings of 37th Conference on Foundations of Computer Science, pages 274-282, 1996. Google Scholar
  13. Arnold Beckmann, Pavel Pudlák, and Neil Thapen. Parity games and propositional proofs. ACM Transactions on Computational Logic (TOCL), 15(2):1-30, 2014. Google Scholar
  14. Zoë Bell. Automating regular or ordered resolution is NP-hard. Electronic Colloquium on Computational Complexity (ECCC), 2020. URL: https://eccc.weizmann.ac.il/report/2020/105/.
  15. Huck Bennett and Chris Peikert. Hardness of the (Approximate) Shortest Vector Problem: A Simple Proof via Reed-Solomon Codes. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023), volume 275, pages 37:1-37:20, 2023. Google Scholar
  16. María Luisa Bonet, Carlos Domingo, Ricard Gavaldà, Alexis Maciel, and Toniann Pitassi. Non-automatizability of bounded-depth Frege proofs. computational complexity, 13:47-68, 2004. Google Scholar
  17. María Luisa Bonet, Toniann Pitassi, and Ran Raz. On interpolation and automatization for Frege systems. SIAM Journal on Computing, 29(6):1939-1967, 2000. Google Scholar
  18. Sam Buss and Jakob Nordström. Proof complexity and SAT solving. Handbook of Satisfiability, 336:233-350, 2021. Google Scholar
  19. Samuel R Buss. On Gödel’s theorems on lengths of proofs II: Lower bounds for recognizing k symbol provability. In Feasible mathematics II, pages 57-90. Springer, 1995. Google Scholar
  20. Stephen Cook and Phuong Nguyen. Logical Foundations of Proof Complexity. Cambridge University Press, 2010. Google Scholar
  21. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. Logic, Automata, and Computational Complexity, 1979. Google Scholar
  22. Stefan Dantchev, Barnaby Martin, and Stefan Szeider. Parameterized proof complexity. Computational Complexity, 20:51-85, 2011. Google Scholar
  23. Susanna F. de Rezende, Mika Göös, Jakob Nordström, Toniann Pitassi, Robert Robere, and Dmitry Sokolov. Automating algebraic proof systems is NP-hard. In Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing, pages 209-222, 2021. Google Scholar
  24. Michal Garlík. Failure of feasible disjunction property for k-DNF resolution and NP-hardness of automating it, 2020. URL: https://arxiv.org/abs/2003.10230.
  25. Mika Göös, Sajin Koroth, Ian Mertz, and Toniann Pitassi. Automating cutting planes is NP-hard. In Proceedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing, pages 68-77, 2020. Google Scholar
  26. Rishab Goyal, Venkata Koppula, Satyanarayana Vusirikala, and Brent Waters. On perfect correctness in (lockable) obfuscation. In Theory of Cryptography Conference, pages 229-259. Springer, 2020. Google Scholar
  27. Lov K Grover. A fast quantum mechanical algorithm for database search. In Proceedings of the twenty-eighth annual ACM symposium on Theory of computing, pages 212-219, 1996. Google Scholar
  28. Lei Huang and Toniann Pitassi. Automatizability and simple stochastic games. In International Colloquium on Automata, Languages, and Programming, pages 605-617. Springer, 2011. Google Scholar
  29. Dmitry Itsykson and Artur Riazanov. Automating OBDD proofs is NP-hard. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022), 2022. Google Scholar
  30. Kazuo Iwama. Complexity of finding short resolution proofs. In Mathematical Foundations of Computer Science 1997, pages 309-318. Springer Berlin Heidelberg, 1997. Google Scholar
  31. Emil Jeřábek. Weak pigeonhole principle, and randomized computation. PhD thesis, Faculty of Mathematics and Physics, Charles University, Prague, 2005. Google Scholar
  32. Emil Jeřábek. Elementary analytic functions in VTC⁰. Annals of Pure and Applied Logic, 174(6):103269, 2023. Google Scholar
  33. Jan Krajíček. Bounded Arithmetic, Propositional Logic and Complexity Theory. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1995. Google Scholar
  34. Jan Krajíček. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. The Journal of Symbolic Logic, 62(2):457-486, 1997. Google Scholar
  35. Jan Krajíček. Proof Complexity. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2019. Google Scholar
  36. Jan Krajíček. Information in propositional proofs and algorithmic proof search. The Journal of Symbolic Logic, 87(2):852-869, 2022. Google Scholar
  37. Jan Krajíček and Pavel Pudlák. Some consequences of cryptographical conjectures for 𝖲₂¹ and EF. Information and Computation, 140(1):82-94, 1998. Google Scholar
  38. Ian Mertz, Toniann Pitassi, and Yuanhao Wei. Short proofs are hard to find. In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019), 2019. Google Scholar
  39. Daniele Micciancio. The Geometry of Lattice Cryptography, pages 185-210. Springer Berlin Heidelberg, 2011. Google Scholar
  40. Daniele Micciancio and Chris Peikert. Trapdoors for lattices: Simpler, tighter, faster, smaller. In Annual International Conference on the Theory and Applications of Cryptographic Techniques, pages 700-718. Springer, 2012. Google Scholar
  41. Theodoros Papamakarios. Depth d Frege systems are not automatable unless 𝐏 = NP. Electronic Colloquium on Computational Complexity (ECCC), 2023. URL: https://eccc.weizmann.ac.il/report/2023/121/.
  42. Chris Peikert. A decade of lattice cryptography. Foundations and Trends in Theoretical Computer Science, 10(4):283-424, 2016. Google Scholar
  43. Chris Peikert and Brent Waters. Lossy trapdoor functions and their applications. In Proceedings of the fortieth annual ACM symposium on Theory of computing, pages 187-196, 2008. Google Scholar
  44. Ján Pich and Rahul Santhanam. Learning Algorithms Versus Automatability of Frege Systems. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022), volume 229, pages 101:1-101:20, 2022. Google Scholar
  45. Pavel Pudlák. Quantum deduction rules. Annals of Pure and Applied Logic, 157(1):16-29, 2009. Google Scholar
  46. Pavel Pudlák. On reducibility and symmetry of disjoint NP pairs. Theoretical Computer Science, 295(1):323-339, 2003. Mathematical Foundations of Computer Science. Google Scholar
  47. Nael Rahman and Vladimir Shpilrain. MOBS (Matrices Over Bit strings) public key exchange, 2021. URL: https://arxiv.org/abs/2106.01116.
  48. Oded Regev. On lattices, learning with errors, random linear codes, and cryptography. Journal of the ACM (JACM), 56(6):1-40, 2009. Google Scholar
  49. P.W. Shor. Algorithms for quantum computation: discrete logarithms and factoring. In Proceedings 35th Annual Symposium on Foundations of Computer Science, pages 124-134, 1994. Google Scholar
  50. Michael Soltys and Stephen Cook. The proof complexity of linear algebra. Annals of Pure and Applied Logic, 130(1):277-323, 2004. Papers presented at the 2002 IEEE Symposium on Logic in Computer Science (LICS). Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact