We show that interactive protocols between a prover and a verifier, a well-known tool of complexity theory, can be used in practice to certify the correctness of automated reasoning tools. Theoretically, interactive protocols exist for all $\textsf{PSPACE}$ problems. The verifier of a protocol checks the prover's answer to a problem instance in polynomial time, with polynomially many bits of communication, and with exponentially small probability of error. (The prover may need exponential time.) Existing interactive protocols are not used in practice because their provers use naive algorithms, inefficient even for small instances, that are incompatible with practical implementations of automated reasoning. We bridge the gap between theory and practice by means of a novel interactive protocol whose prover uses BDDs. We consider the problem of counting the number of assignments to a QBF instance ($\#\textrm{CP}$), which has a natural BDD-based algorithm. We give an interactive protocol for $\#\textrm{CP}$ whose prover is implemented on top of an extended BDD library. The prover has only a linear overhead in computation time over the natural algorithm. We have implemented our protocol in $\textsf{blic}$, a certifying tool for $\#\textrm{CP}$. Experiments on standard QBF benchmarks show that \blic\ is competitive with state-of-the-art QBF-solvers. The run time of the verifier is negligible. While loss of absolute certainty can be concerning, the error probability in our experiments is at most $10^{-10}$ and reduces to $10^{-10k}$ by repeating the verification $k$ times.

翻译：我们证明，证明者与验证者之间的交互式协议——复杂性理论中一项众所周知的工具——可用于在实践中验证自动推理工具的正确性。理论上，交互式协议适用于所有$\textsf{PSPACE}$问题。协议的验证者可在多项式时间内、通过多项式比特的通信、且以指数级小的错误概率检查证明者对问题实例的答案（证明者可能需要指数时间）。现有交互式协议未在实践中使用，因其证明者采用朴素算法，即便对小规模实例也效率低下，与自动推理的实践实现不兼容。我们通过一种新颖的交互式协议弥合了理论与实践的鸿沟，该协议的证明者使用BDD。我们考虑量化布尔公式实例的赋值计数问题（$\#\textrm{CP}$），该问题存在一种基于BDD的自然算法。我们为$\#\textrm{CP}$给出了一个交互式协议，其证明者基于扩展的BDD库实现。相较于自然算法，证明者在计算时间上仅有线性开销。我们已在$\textsf{blic}$中实现了该协议，这是一个用于$\#\textrm{CP}$的认证工具。在标准QBF基准测试上的实验表明，\blick\与最先进的QBF求解器不相上下。验证者的运行时间可忽略。虽然绝对确定性的损失可能令人担忧，但实验中错误概率至多为$10^{-10}$，且通过重复验证$k$次可降至$10^{-10k}$。