Current Deep Neural Network (DNN) verifiers are typically designed to prioritize scalability over reliability. Reliability can be reinforced through the generation of proofs that are checkable by trusted, external proof checkers. To date, only a handful of verifiers support proof production; and these rely on verifier-specific formats, and balance between scalability, proof detail, and the trustworthiness of their proof checker. In this tool paper, we introduce PICID, a DNN verifier that produces proofs in the standard Alethe format for SMT solving, checkable by multiple existing checkers. PICID implements a parallel CDCL(T) architecture that integrates a state-of-the-art, proof-producing SAT solver with the Marabou DNN verifier. Furthermore, PICID leverages UNSAT proofs to derive conflict clauses. Our evaluation shows that PICID generates valid proofs in the vast majority of cases and significantly outperforms existing tools that produce comparable proofs.

翻译：当前的深度神经网络（DNN）验证器通常被设计为优先考虑可扩展性而非可靠性。通过生成可由可信的外部证明检查器检查的证明，可以增强可靠性。迄今为止，只有少数验证器支持证明生成；这些验证器依赖于特定于验证器的格式，并在可扩展性、证明细节及其证明检查器的可信度之间进行权衡。在本工具论文中，我们介绍了PICID，这是一种能够以标准的、用于SMT求解的Alethe格式生成证明的DNN验证器，其证明可由多种现有检查器验证。PICID实现了一种并行的CDCL(T)架构，该架构将最先进的、可生成证明的SAT求解器与Marabou DNN验证器集成在一起。此外，PICID利用UNSAT证明来推导冲突子句。我们的评估表明，PICID在绝大多数情况下都能生成有效的证明，并且显著优于现有的、能生成可比证明的工具。