PLDI 2025
Mon 16 - Fri 20 June 2025 Seoul, South Korea
Wed 18 Jun 2025 14:20 - 14:40 at Cosmos, Violet & Tulip - Numerics and Approximation Chair(s): Pavel Panchekha

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 Jun

Displayed 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
20m
Talk
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
20m
Talk
Support Triangle Machine
PLDI Research Papers
Jiaying Li R3 Lab, Chunxue Hao China CITIC Bank
DOI
14:40
20m
Talk
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
20m
Talk
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