PICID让神经网络验证更可靠，能生成可被多方验证的证明。
PICID: Proof-Driven Clause Learning in Neural Network Verification
- 用标准Alethe格式生成可验证的证明，兼容多个检查器。
- 在多数案例中成功生成有效证明，性能优于同类工具。
- 利用不满足证明推导冲突子句，提升验证效率。
当前深度神经网络（DNN）验证工具通常优先考虑可扩展性而非可靠性。可靠性可通过生成由可信外部检查器验证的证明来增强。目前仅有少数验证器支持证明生成，且依赖特定格式，难以兼顾可扩展性、证明细节与检查器可信度。本文介绍PICID，一种可生成标准Alethe格式SMT证明的DNN验证器，支持多检查器验证。PICID采用并行CDCL(T)架构，集成先进的可证明SAT求解器与Marabou DNN验证器，并利用不满足证明推导冲突子句。评估表明，PICID在绝大多数情况下生成有效证明，显著优于现有可生成类似证明的工具。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。