Goose

The verification of deep neural networks is a recent algorithmic challenge that has attracted significant interest, resulting in a wide array of complete and incomplete solvers that draw on diverse techniques. As is typical in hard search problems, no single solver is expected to be the fastest on all inputs. While this insight has been leveraged to boost Boolean Satisfiability (SAT), for instance, by combining or tuning solvers, it is yet to lead to a leap in the neural network verification domain.

Goose is an upcoming meta-solver for deep neural network verification. Goose’s architecture supports a wide variety of complete and incomplete solvers and leverages three key meta-solving techniques to improve efficiency: algorithm selection, probabilistic satisfiability inference, and time iterative deepening. Using Goose we observe an \percimprove improvement in \partwo score across over 800 benchmarks and 13 solvers from VNN-COMP ‘21.

People

Joseph Scott
Guanting Pan
Piyush Jha
Elias B. Khalil
Vijay Ganesh (Principal Investigator)