Quantum Verification of Compressed Proofs through DLDS-to-Circuit Compilation - Saraiva, Lorenzo; Haeusler, Edward Hermann (Anais do Simpósio Brasileiro de Computação e Comunicação Quânticas (SBCCQ), 2026)
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(n 2 ) 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.