Testing neural network verifiers with known-answer problems

Neural network verifiers claim to provide formal guarantees, but existing benchmarks lack ground-truth labels, making it impossible to measure verifier accuracy or diagnose failure modes. This work introduces a reusable framework that analytically constructs verification instances with known-in-advance robustness labels. The authors discovered multiple numeric tolerance issues and an implementation bug in widely-used verifiers, demonstrating the value of ground-truth evaluation. They also define Difficulty Profiles—measurable properties that characterize what makes a verification instance hard—and use these to show that different verifiers struggle with different problem aspects. Code is released publicly.