Quantum Automating $\mathbf{TC}^0$-Frege Is LWE-Hard
Noel Arteche, Gaia Carenini, Matthew Gray
TL;DR
The paper defines quantum automatability for propositional proof systems and proves a conditional hardness result: if there exists a polynomial-time quantum algorithm that weakly automates $ ext{$TC^0$-Frege}$, then the lattice-based Learning with Errors ($LWE$) problem can be solved by polynomial-size quantum circuits. Extending the argument, a weak automatizer for $ ext{$AC^0$-Frege}$ would break $LWE$ in subexponential quantum time. The authors develop quantum feasible interpolation, build injective lattice-based one-way functions with succinct injectivity certificates, and formalize the requisite linear-algebra reasoning inside a conservative extension $ ext{$LA_ extbf{Q}$}$ that translates to short $ ext{$TC^0$-Frege}$ proofs. This work generalizes classical cryptography-based non-automatability results to the quantum setting, establishing the first conditional hardness results for quantum proof search and suggesting directions for future exploration of generic hardness assumptions and limitations of quantum speedups in proof complexity.
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 $\mathbf{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, Domingo, Gavaldà, Maciel, and Pitassi (Computational Complexity, 2004), who showed that Extended Frege, $\mathbf{TC}^0$-Frege and $\mathbf{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.