Quantum Verification of Compressed Proofs through DLDS-to-Circuit Compilation
Lorenzo Saraiva, Edward Hermann Hæusler
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.
Simpósio Brasileiro de Computação e Comunicação Quânticas (SBCCQ)•Jul 19, 2026•0 citations