A method (BICCOS) for making branch-and-bound neural-network verifiers scale by generating cutting planes that are specific to the verification problem instead of borrowing generic cuts from a mixed-integer-programming solver. It infers valid cuts from already-verified subproblems in the search tree, precludes the same ReLU-state combinations in sibling subproblems, strengthens cuts by dropping unnecessary neuron dependencies via influence scores, and presolves with a multi-tree search, letting verification reach networks too large for prior cutting-plane approaches.
Formal neural network verification proves certified bounds on a network's outputs, such as robustness to adversarial perturbations, and for ReLU networks is commonly solved by branch and bound that s…