Example: Differential Verification of Two Networks

This example bounds f1(x) - f2(x) for two structurally identical networks whose weights differ slightly — the setting of quantization or pruning verification. Subtracting independent bounds is uninformative; the differential interpreter tracks the difference itself.

Part 1 — Instrumented model with DiffLinear

Pair the layers inside one module. Concretely the model behaves as network 1; under boundlab.diff.zono3.interpret both branches propagate at once.

import copy

import torch
from torch import nn

from boundlab import Error
from boundlab.utils import ShapeDtype
from boundlab.zono import Zono
from boundlab.diff.ops import DiffLinear
from boundlab.diff.zono3 import interpret as diff_interpret

torch.manual_seed(0)

# Network 1, and a slightly perturbed copy standing in for network 2.
fc1_a, fc1_b = nn.Linear(4, 8), nn.Linear(4, 8)
with torch.no_grad():
    fc1_b.weight.copy_(fc1_a.weight + 0.01 * torch.randn_like(fc1_a.weight))
    fc1_b.bias.copy_(fc1_a.bias)
head = nn.Linear(8, 3)


class Paired(nn.Module):
    def __init__(self):
        super().__init__()
        self.layer = DiffLinear(fc1_a, fc1_b)
        self.head = head

    def forward(self, x):
        return self.head(torch.relu(self.layer(x)))


model = Paired().eval()

center = torch.tensor([0.1, -0.2, 0.3, 0.0])
err = Error("input", ShapeDtype(center.shape, center.dtype))
x = Zono.error(err) * 0.1 + center

out = diff_interpret(model)(x)
diff_lb, diff_ub = out.diff.lbub()
print("difference bounds:", diff_lb, diff_ub)

# Compare against subtracting the two branch bounds.
x_lb, x_ub = out.x.lbub()
y_lb, y_ub = out.y.lbub()
print("naive width:  ", ((x_ub - y_lb) - (x_lb - y_ub)).mean().item())
print("tracked width:", (diff_ub - diff_lb).mean().item())

The tracked width is typically orders of magnitude below the naive one: everything the two networks share cancels in the difference component.

Part 2 — Two ONNX files with diff_net

When the networks exist as separate models, merge them: wherever both read a parameter, the merged graph pairs the initializers with boundlab::DiffPair nodes.

from boundlab.interp import onnx_export
from boundlab.diff.onnx import diff_net

net1 = nn.Sequential(nn.Linear(4, 8), nn.ReLU(), nn.Linear(8, 3)).eval()
net2 = copy.deepcopy(net1)
with torch.no_grad():
    for parameter in net2.parameters():
        parameter.add_(0.01 * torch.randn_like(parameter))

merged = diff_net(
    onnx_export(net1, (torch.zeros(4),)),
    onnx_export(net2, (torch.zeros(4),)),
)

out = diff_interpret(merged)(x)
diff_lb, diff_ub = out.diff.lbub()

# Monte-Carlo check on the difference.
samples = center + 0.1 * (torch.rand(2000, 4) * 2 - 1)
with torch.no_grad():
    diffs = net1(samples) - net2(samples)
assert (diffs >= diff_lb - 1e-4).all() and (diffs <= diff_ub + 1e-4).all()

Part 3 — Building the triple by hand

For custom inputs — e.g. the two networks reading different input regions — construct the DiffExpr3 yourself.

from boundlab.diff.expr import DiffExpr3

model3 = nn.Sequential(nn.Linear(4, 3), nn.ReLU()).eval()

x1 = Zono.error(err) * 0.1 + center            # network 1's input
x2 = Zono.error(err) * 0.1 + center + 0.05     # network 2's input, shifted
triple = DiffExpr3(x1, x2, x1 - x2)            # shared symbols: diff is exact

out = diff_interpret(model3)(triple)
print("diff bounds:", out.diff.lbub())

Notes

• boundlab.diff.polysp3.interpret is a drop-in replacement running the same differential algebra over sparse polynomials.

• Score-based pruning ops (heaviside_pruning, topk_pruning, softmax_pruning in boundlab.diff.ops) are handled exactly for concrete scores; symbolic scores are rejected rather than approximated.