Source-linked AI summary
Training verified learners with learned verifiers
Krishnamurthy Dvijotham, Sven Gowal, Robert Stanforth, Relja Arandjelovic, Brendan O'Donoghue, Jonathan Uesato, Pushmeet Kohli
TL;DR
The paper addresses the challenge of training neural networks that both fit data and provably satisfy desired input-output properties. It introduces predictor-verifier training, which jointly trains a predictor and a verifier using task loss and a violation bound. The approach achieves state-of-the-art verified robustness on MNIST and SVHN and scales to verifiably robust CIFAR-10 models.
Problem
Existing verification can be costly, while verified-training methods are limited in supported activations or architectures and require optimization during training.
Method
Predictor-verifier training jointly trains a task-performing predictor and a verifier that bounds worst-case specification violation.
Results
The approach achieves state-of-the-art verified accuracy on MNIST and SVHN and obtains the first nontrivial verified accuracy bounds on CIFAR-10.
Takeaways & Limitations
PVT provides a scalable framework for training verified models across general feedforward architectures and larger image-classification datasets.
Takeaways & Limitations
The verification method assumes simple transfer functions with efficient solution procedures and backpropagation-compatible parameters, and the robustness setting focuses on ℓ∞ input perturbations.
Abstract
from arXiv · showhide
This paper proposes a new algorithmic framework, predictor-verifier training, to train neural networks that are verifiable, i.e., networks that provably satisfy some desired input-output properties. The key idea is to simultaneously train two networks: a predictor network that performs the task at hand,e.g., predicting labels given inputs, and a verifier network that computes a bound on how well the predictor satisfies the properties being verified. Both networks can be trained simultaneously to optimize a weighted combination of the standard data-fitting loss and a term that bounds the maximum violation of the property. Experiments show that not only is the predictor-verifier architecture able to train networks to achieve state of the art verified robustness to adversarial examples with much shorter training times (outperforming previous algorithms on small datasets like MNIST and SVHN), but it can also be scaled to produce the first known (to the best of our knowledge) verifiably robust networks for CIFAR-10.
1 Introduction
Neural networks can be highly vulnerable to small adversarial perturbations, while existing verification and verified-training methods face scalability and computational limitations. Predictor-verifier training addresses these challenges and achieves strong verified robustness on MNIST and SVHN while scaling to CIFAR-10.
- Small, carefully chosen input deviations can cause neural networks to make highly confident incorrect predictions.
- Formal verification can be exponentially costly and has typically been limited to small networks.
- Existing verified-training approaches have been restricted by activation or architecture assumptions and costly optimization inside each training iteration.
- Predictor-verifier training jointly trains a task predictor and verifier using task loss plus an upper bound on specification violation.
- PVT supports arbitrary feedforward architectures and amortizes verification costs across multiple examples.
- State-of-the-art verified accuracy under ℓ∞ adversarial perturbations is achieved on MNIST and SVHN.
- PVT scales to CIFAR-10 and obtains the first nontrivial verified accuracy bounds reported by the authors.
2 Verification using duality
The verification framework expresses desired network properties as constraints over all inputs in a nominal set, then uses optimization and dual relaxation to obtain certificates or counterexamples. It supports efficient bound computation under simple transfer functions and provides the basis for predictor-verifier training.
- General specifications: Specifications require the network output to lie in a half-space for every input in a nominal set, encompassing robustness and other properties.The specification is defined by c, d, and the network mapping φ; examples include monotonicity and avoiding unsafe labels.
- Adversarial robustness: Adversarial robustness requires that no perturbed input changes the prediction away from the nominal true label.The perturbation set Sin(xnom) models the adversary’s allowed changes, including ℓ∞-norm perturbations.
- Counterexample optimization: Verification searches for a counterexample by maximizing the specification violation subject to input-set and layer-transition constraints; an optimum below 0 certifies the property.The network is represented as layered transfer functions, with x0 as the input and xK as the logits.
- Assumptions: The method assumes simple, backpropagation-compatible transfer functions, whose bound problems can be solved efficiently; ReLU-like monotone nonlinearities are an example.The framework treats efficient solution as access to a cheap oracle, potentially via closed form or convex optimization.
- Dual relaxation: Because exact verification is NP-hard, Lagrangian relaxation introduces multipliers and valid intermediate-layer bounds to compute tractable upper bounds.Bounds tighten the relaxation, while any dual variables yielding a negative bound provide a valid certificate; a positive optimum supplies a counterexample.
- Predictor-verifier training: Predictor-verifier training updates predictor parameters using a minibatch loss so the predictor improves while becoming more verifiable.The algorithm initializes predictor and verifier parameters, estimates the loss, and updates the predictor during training.
3 Predictor-Verifier Training
Predictor-verifier training learns verifier networks to approximate dual optimization solutions, jointly training them with predictors so specification satisfaction can be optimized during ordinary backpropagation-based training. The framework supports multiple verifier architectures and reduces verification overhead relative to per-example optimization.
- Learned verification: PVT uses a verifier network to predict dual variables that approximately minimize an upper bound on specification violation for each input.The predictor simultaneously adjusts its weights to reduce specification violation.
- Training objective: The training objective combines supervised task loss with a weighted logarithmic dual-loss term that bounds worst-case specification violation.κ controls the relative emphasis on satisfying the specification versus fitting the data.
- Computational motivation: Learning dual variables avoids solving a separate optimization problem for every training example or minibatch element during training.Prior approaches either retained per-example optimization or required intensive semidefinite programs.
- Scalability: Because verification requires only a forward pass through the verifier, its computational complexity is linear in network size and can amortize verification across examples.This scaling is intended to support much larger verifiable models than prior approaches.
- Verifier architectures: Verifier architectures include constant, direct, and backward-forward designs, with the latter two using input and layer information to predict layer-specific dual variables.The backward-forward design propagates intermediate information downward before a forward pass predicts dual variables.
4 Experimental results
Experiments show that direct and backward-forward verifier architectures provide the strongest verified adversarial-error bounds, while PVT improves verified robustness and verification efficiency across image benchmarks. PVT also outperforms prior verified-training and adversarial-training comparisons, although nominal test error can remain higher.
- Verifier architecture: Direct and backward-forward verifier architectures achieve the best verified bounds on adversarial error rates among the evaluated PVT designs.The comparison includes constant, direct, and backward-forward architectures.
- Comparison with prior methods: PVT achieves lower normal and adversarial error rates and better verifiable bounds than Kolter and Wong, setting the state-of-the-art in verified robustness.The result is reported for comparable ConvNet architectures.
- Comparison with adversarial training: PVT achieves adversarial error rates of 2.87% on MNIST and 67.28% on CIFAR-10 against adversarial training for the evaluated ConvNet architecture.The adversarially trained networks achieve only a trivial 100% upper bound on adversarial error, whereas PVT networks are provably robust.
- Verification time: PVT reaches nearly optimal MNIST verification bounds within a 15 ms per-test-example budget, while adversarially trained models have weaker bounds at every verification-time limit.The comparison uses fully connected models with tuned L1 regularization for adversarial training.
- Verifier architecture: The constant verifier performs worst, while the backward-forward architecture achieves a much lower nominal error rate than the direct architecture on SVHN.Table 2 uses κ = 1 and reports nominal, attacked, and directly predicted verified errors.
5 Conclusions
The paper presents predictor-verifier training as a novel approach for training verified models and reports faster training with tighter verified and nominal error bounds in image classification.
- Predictor-verifier training is presented as a novel approach for training verified models.
- The approach outperforms competing techniques on verified bounds for adversarial and nominal error rates in image classification.
- The proposed approach also trains faster than competing techniques.
A.1 Closed form dual objective function
The dual objective decomposes into layer-specific terms under separable constraints, enabling efficient optimization for fixed dual variables when transfer functions are simple.
- The optimization over x can be solved efficiently for fixed λ under the stated input-set and layer-bound constraints.
- The objective and constraints are separable, so optimization proceeds independently for each x_k.
- For intermediate layers, each optimal term is denoted f_k(λ_k−1, λ_k) after solving the corresponding bounded optimization.
- The input-layer and output-layer subproblems are solved similarly or in closed form, yielding f_0(λ_0) and f_K(λ_K−1).
- The resulting dual objective is expressed as a sum of the layer-specific terms.
A.2 Derivation of backward-forward architecture
The backward-forward verifier architecture approximates the dynamic-programming solution of the dual optimization and maps predictor activations and labels to dual variables that can be trained end-to-end.
- The dual optimization can be solved as a dynamic program using backward value-function recursions.
- The theoretical recursion may be impractical when value functions lack closed-form representations or require excessive computation or storage.
- Small neural networks approximate the computational graph to produce dual variables from predictor activations and labels.
- The backward-forward equations define a mapping from (x, y) to λ that can be trained end-to-end to minimize the dual bound.
- Because the mapping is differentiable, gradients propagate into both verifier parameters θ and predictor parameters w.
A.3 Implementation details
The implementation uses specified verifier architectures, datasets, training schedules, and bound-propagation optimizations, including a 2× speedup for affine layers.
- The appendix provides implementation details on model architectures, training procedures, and faster bound propagation.
- The direct verifier uses fully connected layers, while the backward-forward verifier combines backward and forward fully connected paths.
- Experiments cover MNIST, SVHN, and CIFAR-10 with dataset-specific preprocessing and training-data augmentation choices.
- Training uses Adam with an initial learning rate of 10^-3 and dataset-specific epochs, batch sizes, and κ values.
- 2× speedup is obtained for affine bound propagation by using center-radius bounds, requiring two affine operations instead of four.
A.4 Other experimental results
Varying κ exposes a clear trade-off between nominal accuracy and verified robustness on MNIST and CIFAR-10.
- Increasing preference for nominal accuracy lowers robustness, producing an anti-correlation between nominal error and the verified upper bound.The models were trained with κ values from 0.05 to 1 and evaluated at the end of training.