SHF: Efficient, Scalable and Certified Convex Hull Computation in High Dimensions for Verifying Neural Networks and Generating Correctly-rounded Math Libraries

The growing adoption of neural networks in safety-critical domains mandates techniques for verifying their robustness, safety and consistency. Precisely encoding the architecture of the network into a first-order logic formula does not scale to large problem sizes due to the large number of non-linear activations and complex shapes of general activation functions. Thus, state-of-the-art verifiers use abstract interpretation to over-approximate the effect of each activation layer with convex polyhedra for scalability. The most precise polyhedral approximation can be computed via the convex hull of the network’s input-output pairs. However, computing the convex hull for billions of points in high dimensions is a challenging problem, as this problem asymptotically scales as n raised to the power of d, where n is the number of points and d is the dimension. This project observes that the high complexity of computing the convex hull in high dimensions arises because of the mesh connectivity of the convex hull. For most practical applications, it is only necessary to compute the vertices that lie on the convex hull. Thus, in contrast to existing methods for computing the convex hull, this project's novelty lies in developing an output-sensitive algorithm whose computational complexity only depends on the number of vertices of the convex hull. This project's impacts are in designing more accurate algorithms for formal verification of deep neural networks and the generation of correctly-rounded Math libraries. This project will also educate practitioners, graduate and undergraduate students on foundational abstractions in computing. This project makes the following foundational advances. (1) It explores an output-sensitive algorithm whose computational complexity depends only on the number of vertices on the convex hull. Internally, this algorithm uses a linear program to determine if a point p is a linear combination of points in a set S or not. (2) The linear combination test can become a bottleneck as the number of points increases. To efficiently scale to large problem sizes, this project draws on insights from geometry for fast computation of an over-approximation of the vertices that lie on the convex hull. This method avoids the solution of a linear program and only requires vector arithmetic operations. (3) To develop certified implementations for computing the convex hull using floating-point (FP) arithmetic, this project will formalize geometric predicates underlying orientation and convexity and use it to prove the correctness and termination of the proposed algorithms. (4) The resulting algorithms and tools will be evaluated in two domains: verifying neural networks and generation of correctly-rounded Math libraries with the RLIBM (Rutgers Architecture and Programming Languages Lab's Correctly Rounded Libm) approach, which also uses a convex hull to solve a linear program. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria. NSF Award ID: 2551479 | Program: 01002627DB NSF RESEARCH & RELATED ACTIVIT | Principal Investigator: Mridul Aanjaneya | Institution: Rutgers University New Brunswick, NEW BRUNSWICK, NJ | Award Amount: $850,000 View on NSF Award Search: https://www.nsf.gov/awardsearch/show-award/?AWD_ID=2551479 View on Research.gov: https://www.research.gov/awardapi-service/v1/awards/2551479.html