{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:05:55Z","timestamp":1784199955870,"version":"3.55.0"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>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.<\/jats:p>\n                  <jats:p>\n                    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\n                    <jats:italic toggle=\"yes\">Convex Approximation Lifting<\/jats:italic>\n                    (CAL), and propose a constructive approach,\n                    <jats:italic toggle=\"yes\">Support Triangle Machine<\/jats:italic>\n                    (STM), to solving it. STM is grounded in two core insights:\n                    <jats:italic toggle=\"yes\">(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;<\/jats:italic>\n                    and\n                    <jats:italic toggle=\"yes\">(ii) typical single-neuron approximations can be easily decomposed into multiple atomically liftable components<\/jats:italic>\n                    . 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.\n                  <\/jats:p>\n                  <jats:p>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\u2019s 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.<\/jats:p>","DOI":"10.1145\/3729255","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"225-248","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Support Triangle Machine"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1187-7521","authenticated-orcid":false,"given":"Jiaying","family":"Li","sequence":"first","affiliation":[{"name":"OmniVision Technologies, Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-1174-6056","authenticated-orcid":false,"given":"Chunxue","family":"Hao","sequence":"additional","affiliation":[{"name":"China CITIC Bank, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17953-3_3"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/109648.109659"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01581273"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/235815.235821"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/358315.358392"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v34i04.5729"},{"key":"e_1_3_2_8_2","article-title":"Branch and Bound for Piecewise Linear Neural Network Verification.","author":"Bunel Rudy","year":"2019","unstructured":"Rudy Bunel, Jingyue Lu, Ilker Turkaslan, Philip H. S. Torr, Pushmeet Kohli, and M. Pawan Kumar. 2019 Branch and Bound for Piecewise Linear Neural Network Verification. CoRR abs\/1909.06588 (2019).","journal-title":"CoRR"},{"key":"e_1_3_2_9_2","first-page":"4795","article-title":"A Unified View of Piecewise Linear Neural Network Verification.","author":"Bunel Rudy","year":"2018","unstructured":"Rudy Bunel, Ilker Turkaslan, Philip H. S. Torr, Pushmeet Kohli, and Pawan Kumar Mudigonda. 2018 A Unified View of Piecewise Linear Neural Network Verification. In NeurIPS, SamyBengio, Hanna. M Wallach, Hugo Larochelle, KristenGrauman, Nicol\u00f3 Cesa-Bianchi, and Romann Garnett. (Eds.). 4795-4804.","journal-title":"In NeurIPS"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/321556.321564"},{"key":"e_1_3_2_11_2","volume-title":"Linear programming: Theory and extensions.","author":"Dantzig George Bernard","year":"2003","unstructured":"George Bernard Dantzig, and Mukund N Thapa. 2003 Linear programming: Theory and extensions. 2 Springer"},{"key":"e_1_3_2_12_2","article-title":"Scaling the convex barrier with active sets","author":"Palma Alessandro De","year":"2021","unstructured":"Alessandro De Palma, Harkirat S Behl, Rudy Bunel, Philip Torr, and M Pawan Kumar. 2021 Scaling the convex barrier with active sets. In Proceedings of the ICLR 2021 Conference. Open Review.","journal-title":"In Proceedings of the ICLR 2021 Conference."},{"key":"e_1_3_2_13_2","article-title":"Training verified learners with learned verifiers.","author":"Dvijotham Krishnamurthy","year":"2018","unstructured":"Krishnamurthy Dvijotham, Sven Gowal, Robert Stanforth, Relja Arandjelovic, Brendan O\u2019Donoghue, Jonathan Uesato, and Pushmeet Kohli. 2018 Training verified learners with learned verifiers. arXiv preprint arXiv:1805.10265 (2018).","journal-title":"arXiv preprint arXiv:1805.10265"},{"key":"e_1_3_2_14_2","first-page":"550","volume-title":"In UAI","author":"Dvijotham Krishnamurthy","year":"2018","unstructured":"Krishnamurthy Dvijotham, Robert Stanforth, Sven Gowal, Timothy A. Mann, and Pushmeet Kohli. 2018 A Dual Approach to Scalable Verification of Deep Networks. In UAI, Amir Globerson and Ricardo Silva (Eds.) AUAI Press 550-559."},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-61568-9"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"e_1_3_2_17_2","unstructured":"ETH SRI Team. 2022 ERAN: ETH Robustness Analyzer for Neural Networks https:\/\/github.com\/eth-sri\/eran"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00058"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCV.2019.00494"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(72)90045-2"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1111\/j.1467-9469.2006.00452.x"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-05148-1_1"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"e_1_3_2_26_2","unstructured":"Georgiy Klimenko and Benjamin Raichel. 2021 Fast and exact convex hull simplification. arXiv preprint arXiv:2110.00671 (2021)."},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/QRS60937.2023.00062"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632917"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2022.3197697"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498704"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2017.2737234"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_9"},{"key":"e_1_3_2_33_2","first-page":"10900","article-title":"Semidefinite relaxations for certifying robustness to adversarial examples.","author":"Raghunathan Aditi","year":"2018","unstructured":"Aditi Raghunathan, Jacob Steinhardt, and Percy Liang. 2018. Semidefinite relaxations for certifying robustness to adversarial examples. In NeurIPS, Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicol\u00f3 Cesa-Bianchi, and Roman Garnett (Eds.). 10900-10910.","journal-title":"In NeurIPS"},{"key":"e_1_3_2_34_2","first-page":"15072","article-title":"Beyond the Single Neuron Convex Barrier for Neural Network Certification.","author":"Singh Gagandeep","year":"2019","unstructured":"Gagandeep Singh, Rupanshu Ganvir, Markus P\u00fcschel, and Martin T. Vechev. 2019. Beyond the Single Neuron Convex Barrier for Neural Network Certification. In NeurIPS, Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d\u2019Alch\u00e9 Buc, Emily B. Fox, and Roman Garnett (Eds.). 15072-15083.","journal-title":"In NeurIPS,"},{"key":"e_1_3_2_35_2","first-page":"10825","article-title":"Fast and Effective Robustness Certification.","author":"Singh Gagandeep","year":"2018","unstructured":"Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus P\u00fcschel, and Martin T. Vechev. 2018 Fast and Effective Robustness Certification. In NeurIPS,, Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicol\u00f3 Cesa-Bianchi, and Roman Garnett (Eds.). 10825-10836.","journal-title":"In NeurIPS,"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290354"},{"key":"e_1_3_2_37_2","article-title":"Intriguing properties of neural networks.","author":"Szegedy Christian","year":"2014","unstructured":"Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian J. Goodfellow, and Rob Fergus. 2014. Intriguing properties of neural networks. In ICLR (Poster), Yoshua Bengio and Yann LeCun (Eds.).","journal-title":"In ICLR (Poster)"},{"key":"e_1_3_2_38_2","unstructured":"Vincent Tjeng Kai Xiao and Russ Tedrake. 2019. Evaluating Robustness of Neural Networks with Mixed Integer Programming. arXiv: 1711.07356 [cs.LG]"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00031"},{"key":"e_1_3_2_40_2","first-page":"1599","article-title":"Formal security analysis of neural networks using symbolic intervals.","author":"Wang Shiqi","year":"2018","unstructured":"Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. 2018 Formal security analysis of neural networks using symbolic intervals. In 27th USENIX Security Symposium (USENIX Security 18). 1599-1614.","journal-title":"In 27th USENIX Security Symposium (USENIX Security 18)."},{"key":"e_1_3_2_41_2","first-page":"29909","article-title":"Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification.","volume":"34","author":"Wang Shiqi","year":"2021","unstructured":"Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. 2021. Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. Advances in Neural Information Processing Systems 34 (2021) 29909-29921","journal-title":"Advances in Neural Information Processing Systems"},{"key":"e_1_3_2_42_2","first-page":"5273","volume-title":"In ICML (Proceedings of Machine Learning Research, Vol. 80)","author":"Weng Tsui-Wei","year":"2018","unstructured":"Tsui-Wei Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsieh, Luca Daniel, Duane S. Boning, and Inderjit S. Dhillon. 2018 Towards Fast Computation of Certified Robustness for ReLU Networks. In ICML (Proceedings of Machine Learning Research, Vol. 80), Jennifer G. Dy and Andreas Krause (Eds.). PMLR, 5273-5282"},{"key":"e_1_3_2_43_2","first-page":"5283","volume-title":"In ICML (Proceedings of Machine Learning Research, Vol. 80),","author":"Wong Eric","year":"2018","unstructured":"Eric Wong and J. Zico Kolter. 2018. Provable Defenses against Adversarial Examples via the Convex Outer Adversarial Polytope. In ICML (Proceedings of Machine Learning Research, Vol. 80), Jennifer G. Dy and Andreas Krause (Eds.). PMLR, 5283-5292."},{"key":"e_1_3_2_44_2","article-title":"Scaling provable adversarial defenses.","volume":"31","author":"Wong Eric","year":"2018","unstructured":"Eric Wong, Frank Schmidt, Jan Hendrik Metzen, and J Zico Kolter. 2018. Scaling provable adversarial defenses. Advances in Neural Information Processing Systems. 31 (2018)","journal-title":"Advances in Neural Information Processing Systems."},{"key":"e_1_3_2_45_2","article-title":"Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers.","author":"Xu Kaidi","year":"2021","unstructured":"Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. 2021. Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers. In International Conference on Learning Representation (ICLR).","journal-title":"In International Conference on Learning Representation (ICLR)."},{"key":"e_1_3_2_46_2","first-page":"4944","article-title":"Efficient Neural Network Robustness Certification with General Activation Functions.","author":"Zhang Huan","year":"2018","unstructured":"Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. 2018. Efficient Neural Network Robustness Certification with General Activation Functions. In NeurIPS , Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicol\u00f3 Cesa-Bianchi, and Roman Garnett (Eds.). 4944-4953.","journal-title":"In NeurIPS"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729255","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:05:47Z","timestamp":1784196347000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729255"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":45,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729255"],"URL":"https:\/\/doi.org\/10.1145\/3729255","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-14","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}