PANDA is a scalable system that uses zero-knowledge proofs to prove the robustness and fairness properties of a model without revealing its private parameters, and can generate proofs of local robustness for neural networks with more than 2.9M parameters in 5 minutes, and can verify them in 10 seconds.
Abstract
With the growing deployment of machine learning models, formal guarantees of the robustness and fairness of these models have become increasingly important in safety-critical and legal-compliance settings. However, model parameters are often commercial secrets that cannot be disclosed to auditors or end users. To this end, we present PANDA, a scalable system that uses zero-knowledge proofs (ZKPs) to prove the robustness and fairness properties of a model without revealing its private parameters. PANDA is built on top of CROWN, an efficient robustness certification framework that is used in many state-of-the-art formal verification tools for neural networks. The core contribution of PANDA is a novel algorithm for proving linear relaxation bounds for non-linear activation layers, yielding simple, lightweight proofs. Remarkably, our system can generate proofs of local robustness for neural networks with more than 2.9M parameters in 5 minutes, and can verify them in 10 seconds. Prior ZKP-based robustness system rely on exponential-time algorithms that cannot scale to nontrivial networks. In contrast, PANDA scales polynomially in the number of neurons in a network, allowing us to support neural networks 4 orders of magnitude larger than previous approaches with significantly reduced prover overhead.
The SecureCROWN framework is built upon secure two-party computation (2PC), and enables a model owner and a data owner to jointly compute certified robustness bounds -- revealing only the final result while provably protecting both parties' private data under the semi-honest security model.
Nianyun Song, Xiaokun Luan, Yu Guo et al.· 1 citation
This work presents a novel meta-learning framework for anytime-valid certified robustness that adaptively deploys computational resources and demonstrates how anytime-validity enables adaptively allocating compute based upon application-specific risk thresholds, a form of resource triage impossible under classic certification frameworks.
A. C. Cullen, Paul Montague, Benjamin I. P. Rubinstein· arXiv.org· 0 citations
Machine-learned predictions can speed up offline NP-hard optimization, but asking a predictor what to do amounts to asking it to solve the problem, and committing an unchecked prediction forfeits every worst-case guarantee. CASP (Certificate-Augmented Solution Pruning) instead asks which parts of the search space may be ignored, and accepts each answer only after a sound polynomial-time verifier has checked it, so correctness never depends on prediction quality. We develop the learning theory of this design. The verifier makes the induced loss class uniformly bounded, so certificate parameters are learnable from $\tilde O(\varepsilon^{-2}\log K)$ samples ($K$ the maximum instance size), whereas the unverified commitment class admits no distribution-free rate and, under cost spread $R$, none below $\Omega(R/\varepsilon^2)$. Filtering noisy predictions by verifiable confidence dominates the standard min-combiner, with a margin we compute in closed form, and the prediction stays useful even given the LP, because it breaks ties on degenerate optimal faces, where every symmetric LP policy, meaning one whose commitments depend on the instance only through the verifiable confidence values, provably stalls. Experiments on five problems test the theory's quantitative predictions. With trained predictors, unverified pruning loses up to $26%$ of the optimum under distribution shift, while the verified deployment of the same predictions loses nothing.
This survey highlights how optimization- and certification-oriented reasoning can provide a useful framework for reasoning about differences in models, supporting tasks ranging from model training and selection to auditing and certification.
This work formalizes rigorous cryptographic security notions tailored to CMC frameworks, introduces a generic protocol template, and proves that it satisfies these requirements, which offer both cautionary evidence about existing approaches and constructive guidance for designing secure, privacy-preserving ML auditing protocols.
Carter Luck, Olive Franzese-McLaughlin, Elisaweta Masserova et al.· 0 citations
VeriDP is presented, a framework for verifiable differentially private training that cryptographically enforces and proves the correct execution of differentially private stochastic gradient descent (DP-SGD) in zero knowledge, uniting differential privacy and verifiable computation for secure and auditable ML.
B. Abdolmaleki, Amir R. Asadi, Vahid R. Asadi et al.· Proceedings on Privacy Enhan...· 0 citations
Related blog posts
MIT News · Artificial Intelligence· news.mit.eduAug 18, 2026
A new method for surgically removing training examples from a model reveals that as datasets grow, the link between what a model learns and what it produces dissolves.
