PaperlayerView exact revision on arXiv

Source-linked AI summary

Training Mixed-Monotone Neural Networks for Verification Without Set Propagation

Jonas Fingerhut, Lukas Koller, Matthias Althoff

arXiv:2610.30853v1cs.LG

TL;DR

Tight neural-network output enclosures are computationally hard to obtain with set-propagation approaches. This paper uses a difference of monotone subnetworks to compute enclosures with two opposite-corner forward passes and directly optimize their size during training. Across the reported evaluation, training approaches a proven lower bound while preserving prediction accuracy, with favorable speed and tightness comparisons.

  • Problem

    Set-propagation approaches conservatively enclose neural-network outputs, but computing tight output enclosures is generally computationally hard.

    Source: §1 · p. 1

  • Method

    The architecture represents a mixed-monotone network as the difference of two monotone subnetworks, enabling enclosure computation from two opposite-corner forward passes and direct enclosure-size optimization during training.

    Source: §1 · p. 1, §6 · p. 9

  • Results

    Training reduces enclosure size to within 0.5% of the lower bound without sacrificing prediction accuracy; on deep networks, enclosure size exceeds α-CROWN by only 5.1%.

    Source: §6 · p. 10

  • Takeaways & Limitations

    The generalized total-variation lower bound provides a reference for comparing learned enclosure tightness, while enclosure computation is orders of magnitude faster than CROWN and α-CROWN.

    Source: §6 · p. 10

    The evaluation considers regression tasks, and its multiple-time-step evaluation is restricted to a cooperative system with constant input.

    Source: §6 · p. 10

Abstract

from arXiv · show

Most formal verification approaches for neural networks conservatively enclose the output set of the neural network. However, computing a tight output enclosure is in general computationally hard. We sidestep this challenge with a novel neural network architecture that realizes mixed-monotone functions as the difference of monotone subnetworks. By utilizing the theory on mixed-monotone systems, this reduces the computation of a tight output enclosure from complicated set propagation to two simple forward passes of opposite corners of an input interval. Moreover, because the size of the resulting enclosure is a closed-form function of the weights of the neural network, we can directly minimize it during training. We prove a lower bound on the size of any such enclosure, given by the total variation of the represented function generalized to several inputs, which makes it possible to compare the tightness of the enclosure against the optimum. Our evaluation on regression and dynamical-system benchmarks demonstrates that our training reduces the enclosure size to within 0.5% of the lower bound without sacrificing prediction accuracy. Computing our enclosure is orders of magnitude faster than CROWN and $\alpha$-CROWN and on deep networks it is also tighter than zonotope propagation and CROWN, while its size exceeds that of $\alpha$-CROWN by only 5.1%.

1 INTRODUCTION

Set propagation can accumulate abstraction error and become costly to refine, motivating an enclosure method that avoids propagation. The paper constructs a difference of monotone subnetworks and reports near-lower-bound enclosure size with favorable runtime and tightness comparisons.

1 INTRODUCTION

  • Set-propagation abstraction error accumulates with network depth and input-set size, while reducing it can require costly higher-order abstractions or branch-and-bound.Practical verification tools propagate intervals, zonotopes, linear relaxations, or polynomial zonotopes layer by layer.Source: §1 · p. 1
  • Two opposite-corner evaluations of a difference of monotone subnetworks enclose an input interval’s output without set propagation.The two forward passes are independent of network depth, width, and input dimension.Source: §1 · p. 1, Figure 1 · p. 2
  • Within 0.5% of the proven lower bound, training reduces enclosure size without sacrificing prediction accuracy.The enclosure is orders of magnitude faster than CROWN and α-CROWN; on deep networks it is tighter than zonotope propagation and CROWN, while exceeding α-CROWN in size by only 5.1%.Source: §1 · pp. 1–2
  • The architecture builds on sign-constrained neural networks, while prior monotonicity work had not, to the authors’ knowledge, used enforced monotonicity for formal verification.Earlier mixed-monotone approaches obtain decompositions after fixing the network, whereas this work optimizes enclosure tightness during training.Source: §1 · p. 2
  • The paper proves that the smallest enclosure achievable by a difference of two monotone functions equals the represented function’s generalized total variation.This lower bound gives a reference for assessing enclosure tightness.Source: §1 · p. 2

2 PRELIMINARIES

The preliminaries define interval-based enclosure size and the monotonicity concepts used to construct verification-friendly networks. They frame the task as efficiently enclosing neural-network outputs for all inputs in a bounded interval.

2 PRELIMINARIES

  • The interval norm measures a set by the sum of the edge lengths of its smallest containing interval.For a nonempty bounded set, that interval hull uses coordinate-wise infima and suprema.Source: §2 · p. 3

2.2 MONOTONIC NEURAL NETWORKS

  • In this paper, a monotone function or network means a non-decreasing one.The work considers sign-constrained neural networks that represent monotonic functions.Source: §2.1 · p. 3, §2.2 · p. 3

2.1 MONOTONE FUNCTIONS AND MIXED-MONOTONE DECOMPOSITIONS

  • A mixed-monotone function has a decomposition function that is non-decreasing in its first argument and non-increasing in its second, yielding an interval output enclosure from opposite corners.The decomposition must agree with the original function when both arguments are equal; decompositions are not unique, and their enclosure tightness can be optimized through training.Source: §2.1 · p. 3

2.3 PROBLEM STATEMENT

  • Verification seeks to prove that every input in a bounded set maps outside an unsafe output set, using an enclosure of the network’s output set.The stated goal is an efficient computation of tight enclosures to make verification practical and scalable.Source: §2.3 · p. 4

3 A MONOTONE-DIFFERENCE ARCHITECTURE

The proposed architecture represents a network as the difference of two monotone subnetworks, allowing mixed-monotone enclosure computation without set propagation. The resulting enclosure requires two forward passes and has lower stated computational complexity than zonotope propagation or linear relaxations.

3 A MONOTONE-DIFFERENCE ARCHITECTURE

  • Two forward passes through the network compute the enclosure via its decomposition function, avoiding complicated set propagation.The architecture uses sign constraints to make both subnetworks monotone, so their difference is mixed-monotone by construction.Source: §3 · p. 4
  • Enclosure computation takes O(n_max^2 κ) time, versus O(n_max^2 q κ) for zonotope propagation and O(n_max^3 κ^2) for linear relaxations.Here q grows with the network size; the paper states that the enclosure saves a factor growing linearly with the number of neurons compared with both alternatives.Source: §3 · p. 4
  • Different decompositions of the same function can yield enclosures of different sizes.Figure 2 illustrates this dependence of enclosure size on the chosen decomposition.Source: Figure 2 · p. 5

4 VERIFICATION-AWARE TRAINING

The section uses a difference of monotone subnetworks to form mixed-monotone enclosures, then trains the network to reduce their size. A total-variation lower bound provides a reference for enclosure tightness.

4 VERIFICATION-AWARE TRAINING

  • Different decompositions of the same function can produce enclosures of different sizes.The section illustrates this with f(x) = 1 − |x − 1| on [0, 2].Source: §4 · p. 5
  • The training objective combines mean-squared error with a penalty on enclosure size for inputs within a fixed perturbation radius.The enclosure-size term can be optimized without set propagation, and each training iteration requires three forward passes.Source: §4 · pp. 5–6
  • Between consecutive inputs in a chain, output change is bounded by the summed increases of the two monotone subnetworks.This bound underlies the total-variation lower bound on enclosure size.Source: §4 · p. 6
  • The enclosure size cannot be smaller than the represented function’s total variation along input chains, and this lower bound is independent of the decomposition.The total variation generalizes the scalar-function definition to several inputs.Source: §4 · p. 6

5 EVALUATION

The evaluation covers analytic regression models and two dynamical systems, assessing prediction accuracy, enclosure tightness, runtime, verification-aware training, and scalability. Results include close lower-bound tightness, depth-dependent comparisons with set-propagation methods, and enclosures that stay close to sampled reachable sets over multiple time steps.

5 EVALUATION

  • The evaluation spans scalar and multi-input analytic models and the Pendulum and Tanks dynamical systems.Tanks is cooperative and Pendulum is non-cooperative; only two inputs enter the multi-input model nonlinearly.Source: §5 · p. 6

5.1 PREDICTION ACCURACY

  • Mean R2 differences from the unconstrained baseline are at most 0.011 across reported configurations, while the tested mixed-monotone networks maintain high prediction accuracy.The comparison uses the same training protocol.Source: §5.1 · p. 7, Table 1 · p. 7

5.2 VERIFICATION TIGHTNESS AND RUNTIMES

  • At eight layers, the enclosure is tighter than zonotope propagation and CROWN, exceeds α-CROWN’s size by only 5.1%, and computes 32×, 256×, and 20 600× faster than zonotope propagation, CROWN, and α-CROWN, respectively.The comparisons are on the scalar analytic model; at four layers, all methods’ enclosures exceed sampled-image size by at most 17%.Source: §5.2 · p. 7, Table 2 · p. 8

5.3 VERIFICATION-AWARE TRAINING AND THE LOWER BOUND

  • For β ≥ 0.05, enclosures coincide with the sampled image on both benchmarks; larger β can only shrink them by reducing function variation, which decreases accuracy.Varying β trades accuracy against enclosure tightness.Source: §5.3 · p. 7, Table 3 · p. 8

5.4 SCALABILITY

  • At 100 input dimensions, the proposed enclosure remains significantly tighter than zonotope propagation, whose tightness explodes.Source: §5.4 · p. 9, Table 4 · p. 9
  • Across multiple time steps in the Tanks system, the enclosure stays close to the sampled reachable set, while the zonotope enclosure diverges for κ = 8 layers.The network predicts one-step state transitions for a constant input, and the enclosure is iterated by passing each step’s interval to the next.Source: §5.4 · p. 9

6 CONCLUSION

The architecture computes an output enclosure with two forward passes and closed-form enclosure size enables direct optimization during training. The reported results compare its tightness and speed with verification baselines, while the authors identify important scope limits.

6 CONCLUSION

  • Two forward passes at opposite input-interval corners replace set propagation, and the enclosure size is a closed-form function of network weights.This architecture realizes mixed-monotone functions as the difference of two monotone subnetworks.Source: §6 · p. 9
  • Figure 3 plots reachable-set enclosure size over time for the Tanks system with iterative neural-network application.The conclusion passage says the proposed enclosure stays close to the sampled reachable set in this setting.Source: Figure 3 · p. 10, §6 · p. 10
  • Training brings enclosure size within 0.5% of the lower bound without sacrificing prediction accuracy, and the advantage grows with depth, input dimension, and iterative application.On deep networks, the enclosure is tighter than zonotope propagation and CROWN, while its size exceeds α-CROWN by 5.1%; computation is orders of magnitude faster than CROWN and α-CROWN.Source: §6 · p. 10
  • The enclosure bounds neural-network outputs, not the outputs of the systems those networks approximate.The evaluation is limited to regression tasks, and its multi-step evaluation uses a cooperative system with constant input.Source: §6 · p. 10

7 AI USE STATEMENT

The authors disclose generative-AI assistance in drafting, literature work, implementation, proofs, editing, and figure or image creation, and report reviewing the assisted work.

7 AI USE STATEMENT

  • Generative AI assisted with drafting, literature identification and summarization, implementation, proofs, editing, and TikZ figures or images.The authors say they reviewed the AI-assisted work for correctness.Source: §7 · p. 10
  • The authors report carefully checking the correctness of their AI-assisted implementation and reported results.Source: §7 · p. 10
  • The authors state that they checked every claim and reference against its source.Source: §7 · p. 10

8 REPRODUCIBILITY STATEMENT

The paper points readers to benchmark definitions and evaluation details in Sections A.2–A.4 and provides supplementary source code for reproducing its results.

8 REPRODUCIBILITY STATEMENT

  • Benchmark definitions and evaluation details are in Sections A.2–A.4.Source: §8 · p. 10
  • The supplementary reproducibility package contains all source code.Source: §8 · p. 10
  • The package allows readers to reproduce all reported results.Source: §8 · p. 10

A.1 PROOFS

The proof bounds the enclosure size below by the represented function’s total variation over chains. It also constructs a decomposition that attains this lower bound.

A.1 PROOFS

  • The proof computes enclosure bounds by evaluating the monotone subnetworks at the input interval’s opposite corners.Monotonicity makes the corner evaluations bound the network output; the difference between those bounds determines enclosure size.Source: §A.1 · p. 13
  • The proof establishes that the enclosure’s interval norm is at least the total variation of the represented function over the input interval.It bounds the variation along any chain by the enclosure size, then takes the supremum over chains.Source: §A.1 · p. 13
  • A suitable decomposition of the represented function attains the lower bound on enclosure size.The proof constructs monotone components whose difference equals the function.Source: §A.1 · pp. 13–14
  • The construction prescribes the component difference and sum using accumulated variation from the lower corner to each point.The proof argues these components are non-decreasing and that the resulting decomposition attains the bound.Source: §A.1 · pp. 13–14

A.2 BENCHMARK DEFINITIONS

The benchmarks include static analytic models and the Pendulum and Tanks dynamical systems. For Tanks, the evaluation predicts the next state because that map is monotone for a constant input.

A.2 BENCHMARK DEFINITIONS

  • The scalar analytic model is evaluated on [−3, 3] and is non-monotone, with six local extrema in that interval.The subsection also introduces the two dynamical systems and the multi-input analytic model.Source: §A.2 · p. 14
  • Tanks is cooperative, whereas Pendulum is non-cooperative because its sine term violates the stated condition.The Tanks dynamics use parameters k1 = 0.5, k2 = 0.4, k3 = 0.3, k4 = 0.12, and u in [0, 10].Source: §A.2 · p. 15
  • For Tanks evaluations of verification-aware training and multiple time steps, the network predicts the next state, which is monotone for a constant input.For prediction-accuracy evaluation, it instead predicts the state change, which need not be monotone; with eight layers and ϵ = 0.05, enclosure tightness is 1.08 for next state and 1.37 for state change.Source: §A.2 · p. 15
  • The multi-input analytic model has n0 inputs in [−3, 3], with only the first two entering nonlinearly; perturbations cover either all inputs or only those two.Perturbing all inputs makes input-set size grow with n0, while perturbing only the first two keeps it independent of n0.Source: §A.2 · p. 15

A.3 COMPUTATION OF THE TIGHTNESS

These appendices describe how enclosure tightness is estimated, detail the experimental settings, and report additional results on accuracy, verifier comparisons, network depth, input dimension, and multi-step reachability. The reported comparisons include scope-specific sampling and training conditions.

A.3 COMPUTATION OF THE TIGHTNESS

  • The reported tightness divides enclosure size by sampled-output size, so it upper-bounds tightness relative to the exact image, which is unavailable.For dynamical systems, inputs and outputs are standardized for the network, but enclosure and sampled-output sizes are computed in original output units.Source: §A.3 · p. 15

A.4 EXPERIMENTAL DETAILS

  • The experimental architectures use sign-constrained subnetworks, and training stages increase the enclosure-size loss weight from 0 to β/2 to β.The architecture comparisons use parameter counts within 2%; absolute weights in the forward pass keep weights non-negative, while unconstrained weights are optimized using the chain rule.Source: §A.4 · pp. 15–16

A.5 ADDITIONAL RESULTS ON THE PREDICTION ACCURACY

  • Our architecture’s mean R2 differs from the unconstrained baseline by at most 0.01 across tested depths, while both Lipschitz-constrained architectures lose accuracy at six and eight layers.At eight layers, monotone and non-monotone Lipschitz-constrained models reach R2 = 0.752 ± 0.048 and R2 = 0.635 ± 0.074, respectively.Source: §A.5 · pp. 16–17, Table 7 · p. 17

A.6 ADDITIONAL RESULTS ON THE COMPARISON OF VERIFICATION METHODS

  • CROWN is tighter than our enclosure at two and three layers, while ours is tighter at six and eight; α-CROWN tightness is at most 1.004 at every tested depth.At four layers, the difference is smaller than the standard deviation over seeds; α-CROWN uses 20 optimization iterations with learning rate 0.1.Source: §A.6 · p. 17, Table 8 · p. 18

A.7 ADDITIONAL RESULTS ON THE NUMBER OF LAYERS

  • At eight layers, our enclosure-to-perturbation-radius ratio falls from 1.448 to 1.219 across two orders of magnitude of radius, while the zonotope ratio rises twelvefold.The six- and eight-layer crossover-radius medians differ by one tested-radius step and their seed ranges overlap, so the measurements do not show a further decrease from six to eight layers.Source: §A.7 · p. 18

A.8 ADDITIONAL RESULTS ON THE INPUT DIMENSION

  • When only the first two inputs are perturbed, our enclosure tightness stays below 1.05 across tested input dimensions; zonotope propagation takes 4.5 to 7.5 times as long.Our enclosure takes 13 to 16 µs per input set in CORA across those dimensions.Source: §A.8 · p. 19, Table 9 · p. 19

A.9 DETAILS ON THE EVALUATION OVER MULTIPLE TIME STEPS

  • At eight layers, the zonotope enclosure median exceeds 10^6 after 11 steps and reaches 2.9·10^37 after 30; zonotope propagation fails in 26 of 60 runs.The sampled reachable set contracts by more than four orders of magnitude within the evaluated steps; increasing zonotope order from 20 to 200 reduces its size after 20 steps by about one order, without changing the median first step at which it is over 100 times larger than the sampled set.Source: §A.9 · pp. 19–20
Loading 2610.30853v1…