Approximations play a pivotal role in verifying deep neural networks (DNNs). Existing approaches typically rely on either single-neuron approximations (simpler to design but less precise) or multi-neuron approximations (higher precision but significantly more complex to construct). Between them, a notable gap exists.
This work bridges the gap. The idea is to lift single-neuron approximations into multi-neuron approximations with precision gain. To this end, we formulate the approximation transition as a novel problem, named Convex Approximation Lifting (CAL), and propose a constructive approach, Support Triangle Machine (STM), to solving it. STM is grounded in two core insights: (i) there exists a simple geometric structure, called the support triangle, along with an efficient triangle lifting technique that connects single-neuron approximations and multi-neuron approximations; and (ii) typical single-neuron approximations can be easily decomposed into multiple atomically liftable components. Specifically, given a CAL instance, STM constructs a multi-neuron approximation by iteratively processing each output coordinate. For each coordinate, it decomposes the single-neuron approximation into several linear parts, lifts each of them using the triangle lifting technique, and then synthesize an intermediate approximation, which later serves as input for the next iteration.
We theoretically prove the correctness of STM and empirically evaluate its performance on a variety of CAL problems and DNN verification tasks. Experimental results demonstrate STM’s broad applicability, improved precision, and sustained efficiency. Beyond DNN verification, STM has the potential to facilitate the approximation construction process in more general tasks, and we expect it to catalyze further research in related fields.
Wed 18 JunDisplayed time zone: Seoul change
14:00 - 15:20 | Numerics and ApproximationPLDI Research Papers at Cosmos, Violet & Tulip Chair(s): Pavel Panchekha University of Utah | ||
14:00 20mTalk | Solving Floating-Point Constraints with Continuous Optimization PLDI Research Papers Qian Chen Nanjing University, Chenqi Cui Nanjing University, Fengjuan Gao Nanjing University of Science and Technology, Yu Wang Nanjing University, Ke Wang Visa Research, Linzhang Wang Nanjing University DOI | ||
14:20 20mTalk | Support Triangle Machine PLDI Research Papers DOI | ||
14:40 20mTalk | Correctly Rounded Math Libraries without Worrying about the Application’s Rounding Mode PLDI Research Papers Sehyeok Park Rutgers University, Justin Kim Rutgers University, Santosh Nagarakatte Rutgers University DOI | ||
15:00 20mTalk | Bean: A Language for Backward Error Analysis PLDI Research Papers Ariel E. Kellison Cornell University, Laura Zielinski Cornell University, David Bindel Cornell University, Justin Hsu Cornell University DOI |