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 probabilistic 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 an 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 $\textsf{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的交互式协议，弥合了理论与实践的鸿沟。我们考虑统计QBF实例赋值数量的问题（$\#\textrm{CP}$），该问题已有基于BDD的自然算法。我们为$\#\textrm{CP}$给出了一种交互式协议，其证明者实现于扩展的BDD库之上。与自然算法相比，证明者的计算时间仅呈线性额外开销。我们已将协议实现为$\textsf{blic}$——一个针对$\#\textrm{CP}$的认证工具。在标准QBF基准测试上的实验表明，$\textsf{blic}$与最先进的QBF求解器性能相当。验证者的运行时间可忽略不计。虽然绝对确定性的缺失可能令人担忧，但在我们的实验中，错误概率至多为$10^{-10}$，且通过重复验证$k$次可降至$10^{-10k}$。