Overview
Formal verification of neural networks typically requires computing conservative enclosures of network output sets. To bypass the computational difficulty of calculating tight output enclosures through standard set propagation, researchers introduced an architecture that represents mixed-monotone functions as the difference of monotone subnetworks. Grounded in the theory of mixed-monotone systems, this formulation computes tight output enclosures through two forward passes evaluated at opposite corners of an input interval.
Research Context
Most formal verification techniques rely on enclosing the output set of a neural network to guarantee behavioral specifications. However, determining a tight enclosure around an output set is computationally hard in the general case. Existing verification tools, such as zonotope propagation, CROWN, and $\alpha$-CROWN, use various relaxation and propagation strategies to bound outputs, but these approaches often entail high computational overhead or yield loose approximations.
Approach
The proposed method addresses output set computation by structuring the neural network as a difference between monotone subnetworks, directly implementing mixed-monotone functions. Under mixed-monotone systems theory, the output enclosure for an interval input does not require multi-step or non-linear set propagation algorithms; instead, it is derived by evaluating the network at only two points: the opposite corners of the input interval.
Because the size of the resulting output enclosure can be expressed as a closed-form function of the network's weights, the enclosure size can be integrated directly into the objective function and minimized during model training. The authors also proved a theoretical lower bound on the size of any such output enclosure. This lower bound corresponds to the total variation of the represented function generalized across multiple inputs, providing an absolute benchmark for evaluating enclosure tightness against the optimal possible value.
Findings
The authors evaluated the mixed-monotone architecture and its training method on regression and dynamical-system benchmarks:
- Tightness relative to the theoretical limit: Training directly on the closed-form enclosure size minimized the output bounds to within 0.5% of the proven lower bound without compromising prediction accuracy.
- Computational efficiency: Computing output enclosures through two corner evaluations was orders of magnitude faster than evaluating bounds with CROWN and $\alpha$-CROWN.
- Comparative tightness on deep networks: On deep network architectures, the enclosure was tighter than those produced by zonotope propagation and CROWN.
- Comparison with $\alpha$-CROWN: The resulting enclosure size was within 5.1% of the size achieved by $\alpha$-CROWN while avoiding its computational overhead.
Why This Matters
The architecture reduces the computational complexity of formal verification by eliminating set propagation entirely. By enabling output enclosure calculation via two standard forward evaluations and permitting direct optimization of enclosure tightness during training, the framework aligns verification speed with standard inference while maintaining tight guarantees on dynamical-system and regression tasks.