{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:08:23Z","timestamp":1750219703247,"version":"3.41.0"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2024,3,18]],"date-time":"2024-03-18T00:00:00Z","timestamp":1710720000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"National Science Foundation","award":["#2002405 and #2139781"],"award-info":[{"award-number":["#2002405 and #2139781"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2024,3,31]]},"abstract":"<jats:p>Constraints solvers play a significant role in the analysis, synthesis, and formal verification of complex cyber-physical systems. In this article, we study the problem of designing a scalable constraints solver for an important class of constraints named polynomial constraint inequalities (also known as nonlinear real arithmetic theory). In this article, we introduce a solver named PolyARBerNN that uses convex polynomials as abstractions for highly nonlinears polynomials. Such abstractions were previously shown to be powerful to prune the search space and restrict the usage of sound and complete solvers to small search spaces. Compared with the previous efforts on using convex abstractions, PolyARBerNN provides three main contributions namely (i) a neural network guided abstraction refinement procedure that helps selecting the right abstraction out of a set of pre-defined abstractions, (ii) a Bernstein polynomial-based search space pruning mechanism that can be used to compute tight estimates of the polynomial maximum and minimum values which can be used as an additional abstraction of the polynomials, and (iii) an optimizer that transforms polynomial objective functions into polynomial constraints (on the gradient of the objective function) whose solutions are guaranteed to be close to the global optima. These enhancements together allowed the PolyARBerNN solver to solve complex instances and scales more favorably compared to the state-of-the-art nonlinear real arithmetic solvers while maintaining the soundness and completeness of the resulting solver. In particular, our test benches show that PolyARBerNN achieved 100X speedup compared with Z3 8.9, Yices 2.6, and PVS (a solver that uses Bernstein expansion to solve multivariate polynomial constraints) on a variety of standard test benches. Finally, we implemented an optimizer called PolyAROpt that uses PolyARBerNN to solve constrained polynomial optimization problems. Numerical results show that PolyAROpt is able to solve high-dimensional and high order polynomial optimization problems with higher speed compared to the built-in optimizer in the Z3 8.9 solver.<\/jats:p>","DOI":"10.1145\/3632970","type":"journal-article","created":{"date-parts":[[2024,1,24]],"date-time":"2024-01-24T12:16:46Z","timestamp":1706098606000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["PolyARBerNN: A Neural Network Guided Solver and Optimizer for Bounded Polynomial Inequalities"],"prefix":"10.1145","volume":"23","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4600-0909","authenticated-orcid":false,"given":"Wael","family":"Fatnassi","sequence":"first","affiliation":[{"name":"University of California, Irvine, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8224-8477","authenticated-orcid":false,"given":"Yasser","family":"Shoukry","sequence":"additional","affiliation":[{"name":"University of California, Irvine, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,3,18]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3178126.3178133"},{"key":"e_1_3_2_3_2","unstructured":"A. Papachristodoulou J. Anderson G. Valmorbida S. Prajna P. Seiler P. Parrilo M. Peet and J. Jagt. 2021. SOSTOOLS version 4.00 sum of squares optimization toolbox for MATLAB. ArXivorg (2021). https:\/\/par.nsf.gov\/biblio\/10353822"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3178126.3178147"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3302504.3311792"},{"key":"e_1_3_2_6_2","unstructured":"Irwan Bello Hieu Pham Quoc V. Le Mohammad Norouzi and Samy Bengio. 2017. Neural combinatorial optimization with reinforcement learning. arXiv:1611.09940. Retrieved from https:\/\/arxiv.org\/abs\/1611.09940"},{"key":"e_1_3_2_7_2","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/978-3-642-33386-6_12","volume-title":"Proceedings of the International Symposium on Automated Technology for Verification and Analysis","author":"Sassi Mohamed Amin Ben","year":"2012","unstructured":"Mohamed Amin Ben Sassi, Romain Testylier, Thao Dang, and Antoine Girard. 2012. Reachability analysis of polynomial systems using linear programming relaxations. In Proceedings of the International Symposium on Automated Technology for Verification and Analysis. Springer, 137\u2013151."},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3178126.3178137"},{"key":"e_1_3_2_9_2","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/978-3-642-28891-3_9","volume-title":"Proceedings of the NASA Formal Methods Symposium","author":"Brisebarre Nicolas","year":"2012","unstructured":"Nicolas Brisebarre, Mioara Jolde\u015f, \u00c9rik Martin-Dorel, Micaela Mayero, Jean-Michel Muller, Ioana Pa\u015fca, Laurence Rideau, and Laurent Th\u00e9ry. 2012. Rigorous polynomial approximation using Taylor models in Coq. In Proceedings of the NASA Formal Methods Symposium. Springer, 85\u201399."},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.2001.0463"},{"key":"e_1_3_2_11_2","volume-title":"Reachability Analysis of Non-Linear Hybrid Systems Using Taylor Models","author":"Chen Xin","year":"2015","unstructured":"Xin Chen. 2015. Reachability Analysis of Non-Linear Hybrid Systems Using Taylor Models. Ph. D. Dissertation. Fachgruppe Informatik, RWTH Aachen University."},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_18"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-07407-4_17"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_15_2","first-page":"990","volume-title":"Proceedings of the International Conference on Machine Learning","author":"Devlin Jacob","year":"2017","unstructured":"Jacob Devlin, Jonathan Uesato, Surya Bhupatiraju, Rishabh Singh, Abdel-rahman Mohamed, and Pushmeet Kohli. 2017. Robustfill: Neural program learning under noisy I\/O. In Proceedings of the International Conference on Machine Learning. PMLR, 990\u2013998."},{"key":"e_1_3_2_16_2","first-page":"29","volume-title":"Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control","author":"Dreossi Tommaso","year":"2017","unstructured":"Tommaso Dreossi. 2017. Sapo: Reachability computation and parameter synthesis of polynomial dynamical systems. In Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control. 29\u201334."},{"key":"e_1_3_2_17_2","doi-asserted-by":"crossref","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Proceedings of the International Conference on Computer Aided Verification","author":"Dutertre Bruno","year":"2014","unstructured":"Bruno Dutertre. 2014. Yices 2.2. In Proceedings of the International Conference on Computer Aided Verification. Springer, 737\u2013744."},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3302504.3311807"},{"key":"e_1_3_2_19_2","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/978-3-319-45641-6_12","volume-title":"Proceedings of the International Workshop on Computer Algebra in Scientific Computing","author":"England Matthew","year":"2016","unstructured":"Matthew England and James H. Davenport. 2016. The complexity of cylindrical algebraic decomposition with respect to polynomial degree. In Proceedings of the International Workshop on Computer Algebra in Scientific Computing. Springer, 172\u2013192."},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-8396(87)90012-4"},{"key":"e_1_3_2_21_2","first-page":"1","volume-title":"Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control","author":"Ferlez James","year":"2020","unstructured":"James Ferlez and Yasser Shoukry. 2020. AReN: Assured ReLU NN architecture for model predictive control of LTI systems. In Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control. 1\u201311."},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0006-3495(61)86902-6"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1080\/00207170600726592"},{"key":"e_1_3_2_24_2","first-page":"37","volume-title":"Proceedings of the International Symposium on Interval Mathematics","author":"Garloff J\u00fcrgen","year":"1985","unstructured":"J\u00fcrgen Garloff. 1985. Convergent bounds for the range of multivariate polynomials. In Proceedings of the International Symposium on Interval Mathematics. Springer, 37\u201356."},{"key":"e_1_3_2_25_2","first-page":"135","volume-title":"Frontiers in Global Optimization. Nonconvex Optimization and Its Applications","author":"Garloff J\u00fcrgen","year":"2004","unstructured":"J\u00fcrgen Garloff and Andrew P. Smith. 2004. An improved method for the computation of affine lower bound functions for polynomials. In Frontiers in Global Optimization. Nonconvex Optimization and Its Applications. Springer, 135\u2013144."},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.5555\/3454287.3455683"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02591962"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/96877.96943"},{"key":"e_1_3_2_29_2","first-page":"2235","article-title":"Deepmath-deep sequence models for premise selection","author":"Irving Geoffrey","year":"2016","unstructured":"Geoffrey Irving, Christian Szegedy, Alexander A. Alemi, Niklas E\u00e9n, Fran\u00e7ois Chollet, and Josef Urban. 2016. Deepmath-deep sequence models for premise selection. In Proceedings of the 30th Conference on Neural Information Processing Systems. 2235\u20132243.","journal-title":"Proceedings of the 30th Conference on Neural Information Processing Systems"},{"key":"e_1_3_2_30_2","unstructured":"Cezary Kaliszyk Fran\u00e7ois Chollet and Christian Szegedy. 2017. Holstep: A machine learning dataset for higher-order logic theorem proving. International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=ryuxYmvel"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3365365.3382194"},{"key":"e_1_3_2_32_2","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1007\/978-3-642-35289-8_3","volume-title":"Neural Networks: Tricks of the Trade","author":"LeCun Yann A.","year":"2012","unstructured":"Yann A. LeCun, L\u00e9on Bottou, Genevieve B. Orr, and Klaus-Robert M\u00fcller. 2012. Efficient backprop. In Neural Networks: Tricks of the Trade. Lecture Notes in Computer Science Springer, 9\u201348."},{"key":"e_1_3_2_33_2","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/978-3-030-58768-0_17","volume-title":"Proceedings of the International Conference on Software Engineering and Formal Methods","author":"Lestingi Livia","year":"2020","unstructured":"Livia Lestingi, Mehrnoosh Askarpour, Marcello M. Bersani, and Matteo Rossi. 2020. Formal verification of human-robot interaction in healthcare scenarios. In Proceedings of the International Conference on Software Engineering and Formal Methods. Springer, 303\u2013324."},{"key":"e_1_3_2_34_2","volume-title":"Dagstuhl Seminar Proceedings","author":"Mahboubi Assia","year":"2006","unstructured":"Assia Mahboubi. 2006. Programming and certifying a CAD algorithm in the Coq system. In Dagstuhl Seminar Proceedings, Thierry Coquand, Henri Lombardi, and Marie-Fran\u00e7oise Roy (Eds.). Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik."},{"key":"e_1_3_2_35_2","unstructured":"Cplex IBM ILOG. 2009. V12. 1: User\u2019s Manual for CPLEX. International Business Machines Corporation 46 53 (2009) 157."},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3302504.3311801"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-9459-1_12"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2008.04.016"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9256-3"},{"key":"e_1_3_2_40_2","volume-title":"Proceedings of the International Colloquium on Theoretical Aspects of Computing (ICTAC 2015)","author":"Munoz Cesar A.","year":"2015","unstructured":"Cesar A. Munoz. 2015. Formal methods in air traffic management: The case of unmanned aircraft systems. In Proceedings of the International Colloquium on Theoretical Aspects of Computing (ICTAC 2015)."},{"key":"e_1_3_2_41_2","first-page":"209","article-title":"Formal verification of conflict detection algorithms for arbitrary trajectories.","volume":"17","author":"Narkawicz Anthony","year":"2012","unstructured":"Anthony Narkawicz and C\u00e9sar A. Munoz. 2012. Formal verification of conflict detection algorithms for arbitrary trajectories. Reliable Computing 17 (2012), 209\u2013237.","journal-title":"Reliable Computing"},{"key":"e_1_3_2_42_2","first-page":"53","volume-title":"Proceedings of the International Workshop on Formal Approaches to Agent-Based Systems","author":"Nelson Stacy D.","year":"2002","unstructured":"Stacy D. Nelson and Charles Pecheur. 2002. Formal verification for a next-generation space shuttle. In Proceedings of the International Workshop on Formal Approaches to Agent-Based Systems. Springer, 53\u201367."},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3365365.3382204"},{"issue":"1","key":"e_1_3_2_44_2","first-page":"40","article-title":"A matrix method for efficient computation of Bernstein coefficients.","volume":"17","author":"Ray Shashwati","year":"2012","unstructured":"Shashwati Ray and P. S. V. Nataraj. 2012. A matrix method for efficient computation of Bernstein coefficients. Reliable Computing 17, 1 (2012), 40\u201371.","journal-title":"Reliable Computing"},{"key":"e_1_3_2_45_2","first-page":"1","volume-title":"Proceedings of the 2018 IEEE International Symposium on Circuits and Systems (ISCAS)","author":"Roy Debayan","year":"2018","unstructured":"Debayan Roy, Michael Balszun, Thomas Heurung, and Samarjit Chakraborty. 2018. Multi-domain coupling for automated synthesis of distributed cyber-physical systems. In Proceedings of the 2018 IEEE International Symposium on Circuits and Systems (ISCAS). IEEE, 1\u20135."},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/3365365.3382211"},{"key":"e_1_3_2_47_2","volume-title":"Proceedings of the International Conference on Learning Representations","author":"Selsam Daniel","year":"2019","unstructured":"Daniel Selsam, Matthew Lamm, Benedikt B\u00fcnz, Percy Liang, Leonardo de Moura, and David L. Dill. 2019. Learning a SAT solver from single-bit supervision. In Proceedings of the International Conference on Learning Representations. Retrieved from https:\/\/openreview.net\/forum?id=HJMC_iA5tm"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","unstructured":"Zuowei Shen. 2020. Deep network approximation characterized by number of neurons. Communications in Computational Physics 28 5 (2020) 1768\u20131811. DOI:10.4208\/cicp.OA-2020-0149","DOI":"10.4208\/cicp.OA-2020-0149"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/3078621"},{"issue":"2","key":"e_1_3_2_50_2","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1007\/s10898-007-9195-4","article-title":"Fast construction of constant bound functions for sparse polynomials","volume":"43","author":"Smith Andrew Paul","year":"2009","unstructured":"Andrew Paul Smith. 2009. Fast construction of constant bound functions for sparse polynomials. Journal of Global Optimization 43, 2 (2009), 445\u2013458.","journal-title":"Journal of Global Optimization"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/3302504.3311802"},{"key":"e_1_3_2_52_2","doi-asserted-by":"crossref","unstructured":"Philippe Tr\u00e9buchet Bernard Mourrain and Marta Abril Bucero. 2016. Border basis for polynomial system solving and optimization. Mathematical Software\u2013ICMS 2016: 5th International Conference Berlin Germany July 11-14 2016 Proceedings 5 Springer 212\u2013220.","DOI":"10.1007\/978-3-319-42432-3_27"},{"key":"e_1_3_2_53_2","unstructured":"Lieven Vandenberghe. 2010. The CVXOPT linear and quadratic cone program solvers. Retrieved March 20 2010 from http:\/\/cvxopt.org\/documentation\/coneprog.pdf."},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/3178126.3178148"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/3302504.3311810"},{"key":"e_1_3_2_56_2","first-page":"43","volume-title":"IFAC-PapersOnLine","author":"Shoukry Wael Fatnassi and Yasser","year":"2021","unstructured":"Wael Fatnassi and Yasser Shoukry. 2021. PolyAR: A highly parallelizable solver for polynomial inequality constraints using convex abstraction refinement. IFAC-PapersOnLine 54, 5 (2021), 43\u201348."},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1109\/9.661615"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632970","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632970","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:35:50Z","timestamp":1750178150000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632970"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,3,18]]},"references-count":56,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,3,31]]}},"alternative-id":["10.1145\/3632970"],"URL":"https:\/\/doi.org\/10.1145\/3632970","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2024,3,18]]},"assertion":[{"value":"2023-02-27","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-10-21","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-03-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}