Competitive Interactive Certification for Automated Reasoning

• Applicants: Professor Dr. Javier Esparza; Professor Dr. Rupak Majumdar
• Subject Area: Theoretical Computer Science
• Term: since 2026
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 568501586

Automated reasoning tools, such as SAT-solvers, SMT-solvers, and model-checkers, are widely used across many areas of computer science, but they are not immune to bugs. To address this, modern tools generate correctness certificates that can be independently verified. However, certificates for coNP-complete problems, like UNSAT, or PSPACE-complete problems, like hardware model checking, are inherently bound to have superpolynomial worst-case sizes unless NP=coNP or NP=PSPACE. Specifically, all existing solvers and model-checkers produce certificates with exponential worst-case sizes. This is becoming a practical issue, as certificates are now reaching terabyte size and beyond. Interactive proof systems are a principled way of overcoming this certificate size barrier: In this model, a prover and a polynomially bounded verifier exchange messages according to a protocol, after which the verifier decides whether the prover correctly performed a computation. Classical results of complexity theory show that, while conventional certification is only possible for NP, certification by interactive proof systems (interactive certification for short) is possible for all of PSPACE (Shamir's theorem), which includes fundamental automated reasoning problems like UNSAT, QBF, or hardware model checking. Despite numerous efforts, these theoretical results have not yet translated into practical automated reasoning tools. The main reason is that existing provers were designed to work with arbitrary computations and algorithms, making them inefficient in practice. In response, we have proposed a new approach in which we carefully select a specific solving algorithm for an important problem (e.g., UNSAT) and design a tailored, competitive interactive protocol for it. Here, "competitive" means that the prover incurs small time overhead relative to the algorithm. Building on this approach, we have implemented the first interactive protocol for QBF that is competitive with respect to a standard algorithm for QBF based on binary decision diagrams. The goal of this project is to extend our new approach to the algorithms currently used by SAT-solvers, SMT-solvers and model-checkers, including Davis-Putnam-Logemann-Loveland (DPLL), conflict-driven clause learning (CDCL), DPLL(T), or iterative model checking. Additionally, we will explore how to enhance our interactive proof systems to be zero-knowledge—ensuring that the verifier is convinced of the prover's claim without extracting any additional information from the process.

• DFG Programme: Research Grants