Quantum Verification of Compressed Proofs through DLDS-to-Circuit Compilation
Resumo
Quantum computation provides a natural mechanism for verifying global properties of exponentially large combinatorial spaces when these spaces admit compact representations. We present a quantum verification architecture for compressed proof objects based on Dag-Like Derivability Structures (DLDS), polynomial-size directed acyclic graphs obtained by horizontally compressing Natural Deduction proofs. A single DLDS may encode exponentially many tree-shaped derivations, called readings, so explicit reading-by-reading verification is exponential in the number of branching points. We develop a polynomial-time compiler that translates the reading semantics of a restricted class of DLDSs into a reversible quantum oracle. The admissible regime covered by the correctness proof consists of normalized implicational DLDSs with a reading-independent introduction suffix, handled through a deferred-discharge criterion. The resulting oracle is compatible with Grover-style amplitude amplification over the reading space. We prove correctness for this class, establish O(n2) bounds for qubits and gates, and validate the construction using Qiskit simulations on synthetic and pipeline-derived DLDS instances. The construction provides concrete quantum verification infrastructure motivated by the conjectured inclusion coNP ⊆ QCMA, while leaving the underlying proof-theoretic certificate question as a separate open problem.
Referências
Bennett, C. H. (1989). Time/space trade-offs for reversible computation. SIAM Journal on Computing, 18(4):766–776.
Boyer, M., Brassard, G., Høyer, P., and Tapp, A. (1998). Tight bounds on quantum searching. Fortschr. Phys., 46(4–5):493–505.
Cook, S. A. and Reckhow, R. A. (1979). The relative efficiency of propositional proof systems. J. Symbolic Logic, 44(1):36–50.
Gentzen, G. (1935). Investigations into logical deduction. Math. Z., 39:176–210.
Gordeev, L. and Haeusler, E. H. (2019). Proof compression and np versus pspace. Studia Logica, 107(1):53–83.
Gordeev, L. and Haeusler, E. H. (2022). Proof compression and np versus pspace ii: Addendum. Bull. Sect. Log., 51(2):197–205.
Grover, L. K. (1996). A fast quantum mechanical algorithm for database search. In Proc. 28th ACM STOC, pages 212–219.
Haeusler, E. H. (2015). Propositional logics complexity and the sub-formula property. EPTCS, 179:1–16.
Haeusler, E. H. (2022). Exponentially huge natural deduction proofs are redundant: Preliminary results on m⊃. FLAP, 9(1):287–326.
Haeusler, E. H., Barros Junior, J. F. C., and Callou, R. (2025). On the horizontal compression of dag-derivations in minimal purely implicational logic. arXiv:2206.02300.
Krajíček, J. (1995). Bounded Arithmetic, Propositional Logic and Complexity Theory. Cambridge Univ. Press.
Prawitz, D. (1965). Natural Deduction: A Proof-Theoretical Study. Almqvist & Wiksell.
Statman, R. (1979). Lower bounds on herbrand’s theorem. Proc. Amer. Math. Soc., 75(1):104–107.
