{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T09:27:08Z","timestamp":1787563628851,"version":"build-2736575974"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"publisher","award":["DP240103068"],"award-info":[{"award-number":["DP240103068"]}],"id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>\n                    Convex hulls are commonly used to tackle the non-linearity of activation functions in the verification of neural networks. Computing the exact convex hull is a costly task though. In this work, we propose a fast and precise approach to over-approximating the convex hull of the ReLU function (referred to as the\n                    <jats:italic toggle=\"yes\">ReLU hull<\/jats:italic>\n                    ), one of the most used activation functions. Our key insight is to formulate a\n                    <jats:italic toggle=\"yes\">convex polytope<\/jats:italic>\n                    that \u201cwraps\u201d the ReLU hull, by reusing the linear pieces of the ReLU function as the lower faces and constructing upper faces that are adjacent to the lower faces. The upper faces can be efficiently constructed based on the edges and vertices of the lower faces, given that an\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mi>n<\/mml:mi>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    -dimensional (or simply\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mi>n<\/mml:mi>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    d hereafter) hyperplane can be determined by an\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mrow>\n                          <mml:mo>(<\/mml:mo>\n                          <mml:mi>n<\/mml:mi>\n                          <mml:mo>-<\/mml:mo>\n                          <mml:mn>1<\/mml:mn>\n                          <mml:mo>)<\/mml:mo>\n                        <\/mml:mrow>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    d hyperplane and a point outside of it. We implement our approach as\n                    <jats:sc>WraLU<\/jats:sc>\n                    , and evaluate its performance in terms of precision, efficiency, constraint complexity, and scalability.\n                    <jats:sc>WraLU<\/jats:sc>\n                    outperforms existing advanced methods by generating fewer constraints to achieve tighter approximation in less time. It exhibits versatility by effectively addressing arbitrary input polytopes and higher-dimensional cases, which are beyond the capabilities of existing methods. We integrate\n                    <jats:sc>WraLU<\/jats:sc>\n                    into PRIMA, a state-of-the-art neural network verifier, and apply it to verify large-scale ReLU-based neural networks. Our experimental results demonstrate that\n                    <jats:sc>WraLU<\/jats:sc>\n                    achieves a high efficiency without compromising precision. It reduces the number of constraints that need to be solved by the linear programming solver by up to half, while delivering comparable or even superior results compared to the state-of-the-art verifiers.\n                  <\/jats:p>","DOI":"10.1145\/3632917","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T15:48:51Z","timestamp":1704469731000},"page":"2260-2287","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["ReLU Hull Approximation"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2392-3751","authenticated-orcid":false,"given":"Zhongkui","family":"Ma","sequence":"first","affiliation":[{"name":"University of Queensland, Brisbane, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1187-7521","authenticated-orcid":false,"given":"Jiaying","family":"Li","sequence":"additional","affiliation":[{"name":"Microsoft, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6390-9890","authenticated-orcid":false,"given":"Guangdong","family":"Bai","sequence":"additional","affiliation":[{"name":"University of Queensland, Brisbane, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","unstructured":"2022. ERAN: ETH Robustness Analyzer for Neural Networks. https:\/\/github.com\/eth-sri\/eran"},{"key":"e_1_3_1_3_1","unstructured":"2023. pycddlib. https:\/\/pypi.org\/project\/pycddlib\/"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17953-3_3"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0893-9659(91)90141-h"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/bf02293050"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/235815.235821"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v34i04.5729"},{"key":"e_1_3_1_9_1","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)."},{"key":"e_1_3_1_10_1","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. 4795\u20134804."},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/321556.321564"},{"key":"e_1_3_1_12_1","unstructured":"Djork-Arn\u00e9 Clevert Thomas Unterthiner and Sepp Hochreiter. 2015. Fast and Accurate Deep Network Learning by Exponential Linear Units (ELUs). arXiv:arXiv:1511.07289"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","unstructured":"Gregory Cohen Saeed Afshar Jonathan Tapson and Andre van Schaik. 2017. EMNIST: Extending MNIST to handwritten letters. (May 2017). https:\/\/doi.org\/10.1109\/ijcnn.2017.7966217 10.1109\/ijcnn.2017.7966217","DOI":"10.1109\/ijcnn.2017.7966217"},{"key":"e_1_3_1_14_1","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. Vol. 2. Springer."},{"key":"e_1_3_1_15_1","unstructured":"Sumanth Dathathri Krishnamurthy Dvijotham Alexey Kurakin Aditi Raghunathan Jonathan Uesato Rudy Bunel Shreya Shankar Jacob Steinhardt Ian J. Goodfellow Percy Liang and Pushmeet Kohli. 2020. Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming. CoRR abs\/2010.11645 (2020)."},{"key":"e_1_3_1_16_1","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."},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/msp.2012.2211477"},{"key":"e_1_3_1_18_1","unstructured":"Krishnamurthy Dvijotham Sven Gowal Robert Stanforth Relja Arandjelovic Brendan O\u2019Donoghue Jonathan Uesato and Pushmeet Kohli. 2018a. Training verified learners with learned verifiers. arXiv:arXiv:1805.10265"},{"key":"e_1_3_1_19_1","first-page":"550","volume-title":"UAI","author":"Dvijotham Krishnamurthy","year":"2018","unstructured":"Krishnamurthy Dvijotham, Robert Stanforth, Sven Gowal, Timothy A. Mann, and Pushmeet Kohli. 2018b. A Dual Approach to Scalable Verification of Deep Networks.. In UAI. AUAI Press, 550\u2013559."},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-61568-9"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"e_1_3_1_22_1","unstructured":"Claudio Ferrari Mark Niklas Muller Nikola Jovanovic and Martin Vechev. 2022. Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound. arXiv:arXiv:2205.00263"},{"key":"e_1_3_1_23_1","unstructured":"Komei Fukuda. 2003. Cddlib reference manual. Report version 093a McGill University Montr\u00e9al Quebec Canada (2003)."},{"key":"e_1_3_1_24_1","first-page":"91","volume-title":"Combinatorics and Computer Science (Lecture Notes in Computer Science, Vol. 1120)","author":"Fukuda Komei","year":"1995","unstructured":"Komei Fukuda and Alain Prodon. 1995. Double Description Method Revisited.. In Combinatorics and Computer Science (Lecture Notes in Computer Science, Vol. 1120). Springer, 91\u2013111."},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00058"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10710-017-9314-z"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/iccv.2019.00494"},{"key":"e_1_3_1_28_1","unstructured":"Gurobi Optimization LLC. 2023. Gurobi Optimizer Reference Manual. https:\/\/www.gurobi.com"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(73)90020-3"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-05148-1_1"},{"key":"e_1_3_1_32_1","first-page":"97","volume-title":"CAV","author":"Katz Guy","year":"2017","unstructured":"Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. 2017. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks.. In CAV, Vol. 10426. Springer, 97\u2013117."},{"key":"e_1_3_1_33_1","first-page":"443","volume-title":"CAV","author":"Guy Katz Derek A.","year":"2019","unstructured":"Guy Katz, Derek A. Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljic, David L. Dill, Mykel J. Kochenderfer, and Clark W. Barrett. 2019. The Marabou Framework for Verification and Analysis of Deep Neural Networks.. In CAV, Vol. 11561. Springer, 443\u2013452."},{"key":"e_1_3_1_34_1","unstructured":"Alex Krizhevsky Geoffrey Hinton et al. 2009. Learning multiple layers of features from tiny images. (2009)."},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.726791"},{"key":"e_1_3_1_36_1","first-page":"3","volume-title":"Proc. icml","author":"Maas Andrew L.","year":"2013","unstructured":"Andrew L. Maas, Awni Y. Hannun, and Andrew Y. Ng. 2013. Rectifier nonlinearities improve neural network acoustic models. In Proc. icml, Vol. 30. Atlanta, GA, 3."},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1112\/S0025579300002850"},{"key":"e_1_3_1_38_1","unstructured":"Mark Huasong Meng Guangdong Bai Sin Gee Teo Zhe Hou Yan Xiao Yun Lin and Jin Song Dong. 2022. Adversarial robustness of deep neural networks: A survey from a formal verification perspective. IEEE Transactions on Dependable and Secure Computing (2022)."},{"key":"e_1_3_1_39_1","first-page":"3575","volume-title":"ICML (Proceedings of Machine Learning Research, Vol. 80)","author":"Mirman Matthew","year":"2018","unstructured":"Matthew Mirman, Timon Gehr, and Martin T. Vechev. 2018. Differentiable Abstract Interpretation for Provably Robust Neural Networks.. In ICML (Proceedings of Machine Learning Research, Vol. 80). PMLR, 3575\u20133583."},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1515\/9781400881970-004"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498704"},{"key":"e_1_3_1_42_1","unstructured":"Aditi Raghunathan Jacob Steinhardt and Percy Liang. 2018. Semidefinite relaxations for certifying robustness to adversarial examples.. In NeurIPS. 10900\u201310910."},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","unstructured":"Wenjie Ruan Xiaowei Huang and Marta Kwiatkowska. 2018. Reachability Analysis of Deep Neural Networks with Provable Guarantees.. In IJCAI. ijcai.org 2651\u20132659. https:\/\/doi.org\/10.24963\/ijcai.2018\/368 10.24963\/ijcai.2018\/368","DOI":"10.24963\/ijcai.2018\/368"},{"key":"e_1_3_1_44_1","unstructured":"Gagandeep Singh Rupanshu Ganvir Markus P\u00fcschel and Martin T. Vechev. 2019a. Beyond the Single Neuron Convex Barrier for Neural Network Certification.. In NeurIPS. 15072\u201315083."},{"key":"e_1_3_1_45_1","unstructured":"Gagandeep Singh Timon Gehr Matthew Mirman Markus P\u00fcschel and Martin T. Vechev. 2018. Fast and Effective Robustness Certification.. In NeurIPS. 10825\u201310836."},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290354"},{"key":"e_1_3_1_47_1","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)."},{"key":"e_1_3_1_48_1","first-page":"21675","article-title":"The convex relaxation barrier, revisited: Tightened single-neuron relaxations for neural network verification","volume":"33","author":"Tjandraatmadja Christian","year":"2020","unstructured":"Christian Tjandraatmadja, Ross Anderson, Joey Huchette, Will Ma, Krunal Kishor Patel, and Juan Pablo Vielma. 2020. The convex relaxation barrier, revisited: Tightened single-neuron relaxations for neural network verification. Advances in Neural Information Processing Systems 33 (2020), 21675\u201321686.","journal-title":"Advances in Neural Information Processing Systems"},{"key":"e_1_3_1_49_1","unstructured":"Vincent Tjeng Kai Y. Xiao and Russ Tedrake. 2019. Evaluating Robustness of Neural Networks with Mixed Integer Programming.. In ICLR (Poster). OpenReview.net."},{"key":"e_1_3_1_50_1","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\u201329921.","journal-title":"Advances in Neural Information Processing Systems"},{"key":"e_1_3_1_51_1","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). PMLR 5273\u20135282."},{"key":"e_1_3_1_52_1","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). PMLR 5283\u20135292."},{"key":"e_1_3_1_53_1","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_1_54_1","unstructured":"Han Xiao Kashif Rasul and Roland Vollgraf. 2017. Fashion-MNIST: a Novel Image Dataset for Benchmarking Machine Learning Algorithms. arXiv:arXiv:1708.07747"},{"key":"e_1_3_1_55_1","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)."},{"key":"e_1_3_1_56_1","unstructured":"Huan Zhang Shiqi Wang Kaidi Xu Linyi Li Bo Li Suman Jana Cho-Jui Hsieh and J. Zico Kolter. 2022. General Cutting Planes for Bound-Propagation-Based Neural Network Verification. arXiv:arXiv:2208.05740"},{"key":"e_1_3_1_57_1","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. 4944\u20134953."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632917","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632917","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T16:06:45Z","timestamp":1751645205000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632917"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":56,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632917"],"URL":"https:\/\/doi.org\/10.1145\/3632917","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}