一句话：提出凸近似提升问题及支撑三角形机器，将单神经元近似提升为更精确的多神经元近似，用于DNN验证。
深度神经网络验证依赖近似，但单神经元近似易构造而精度低，多神经元近似精度高但构造复杂，二者间存在明显空白。本文将这一过渡形式化为新问题“凸近似提升”（CAL），并提出构造性方法“支撑三角形机器”（STM）。STM 基于两点：支撑三角形这一简单几何结构及高效三角形提升技术可连接单神经元与多神经元近似；典型单神经元近似可分解为多个可原子提升分量。对每个 CAL 实例，STM 逐输出坐标将单神经元近似分解为线性部分，分别提升并合成中间近似，迭代进行。作者证明了 STM 的正确性，并在多种 CAL 问题与 DNN 验证任务上实验，表明其适用性广、精度更高且效率稳定。
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 servers 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 approximation construction process in more general tasks, and we expect it to catalyze further research in related fields.