Noel Arteche: 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 standard lattice-based cryptographic assumptions, no quantum algorithm can weakly automate \(\mathsf{TC}^0\)-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 et al. (Computational Complexity, 2004), who showed that Extended Frege, \(\mathsf{TC}^0\)-Frege and \(\mathsf{AC}^0\)-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.

This is joint work with Gaia Carenini and Matthew Gray.