{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T14:27:09Z","timestamp":1766068029092,"version":"3.41.0"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"8","license":[{"start":{"date-parts":[[2024,11,30]],"date-time":"2024-11-30T00:00:00Z","timestamp":1732924800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2024,11,30]]},"abstract":"<jats:p>Uninterpreted predicate solving is a fundamental problem in formal verification, including loop invariant and constrained horn clauses predicate solving. Existing approaches have been mostly in symbolic ways. While achieving sustainable progress, they still suffer from inefficiency and seem unable to leverage the ever-increasing computility, such as GPU. Recently, neural relaxation has been proposed to tackle this problem. They treat the uninterpreted predicate-solving task as an optimization problem by relaxing the discrete search process into a learning process of neural networks. However, two bottlenecks keep them from being valid. First, relaxed neural networks cannot match the original semantics of predicates rigorously; second, the neural networks are difficult to train to reach global optimization. Therefore, this article presents a novel discrete neural architecture with the Abstract Gradient Decent (AGD) algorithm to directly solve uninterpreted predicates in the discrete hypothesis space. The abstract gradient is for discrete neurons whose calculation rules are designed in an abstract domain. Our approach conforms to the original semantics of predicates, and the proposed AGD algorithm can achieve global optimization satisfactorily. We implement the tool Dasp in the Boxes abstract domain to solve uninterpreted predicates in the QF-NIA SMT theory. In the experiments, Dasp has outperformed seven state-of-the-art tools across three predicate synthesis tasks.<\/jats:p>","DOI":"10.1145\/3675394","type":"journal-article","created":{"date-parts":[[2024,7,2]],"date-time":"2024-07-02T15:25:10Z","timestamp":1719933910000},"page":"1-47","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Neural Solving Uninterpreted Predicates with Abstract Gradient Descent"],"prefix":"10.1145","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8647-4949","authenticated-orcid":false,"given":"Shiwen","family":"Yu","sequence":"first","affiliation":[{"name":"State Key Laboratory of Complex and Critical Software Environment, College of Computer Science and Technology, National University of Defense Technology, Changsha, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-3896-4971","authenticated-orcid":false,"given":"Zengyu","family":"Liu","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Complex and Critical Software Environment, College of Computer Science and Technology, National University of Defense Technology, Changsha, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7780-2330","authenticated-orcid":false,"given":"Ting","family":"Wang","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Complex and Critical Software Environment, College of Computer Science and Technology, National University of Defense Technology, Changsha, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0637-8744","authenticated-orcid":false,"given":"Ji","family":"Wang","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Complex and Critical Software Environment, College of Computer Science and Technology, National University of Defense Technology, Changsha, China"}]}],"member":"320","published-online":{"date-parts":[[2024,12,3]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_3_3_2_2","DOI":"10.1007\/978-3-030-99524-9_24"},{"unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2016. The Satisfiability Modulo Theories Library (SMT-LIB). Retrieved from www.SMT-LIB.org.","key":"e_1_3_3_3_2"},{"doi-asserted-by":"publisher","key":"e_1_3_3_4_2","DOI":"10.3233\/FAIA201017"},{"doi-asserted-by":"publisher","key":"e_1_3_3_5_2","DOI":"10.1561\/2500000002"},{"doi-asserted-by":"publisher","key":"e_1_3_3_6_2","DOI":"10.1007\/978-3-031-13185-1_14"},{"doi-asserted-by":"publisher","key":"e_1_3_3_7_2","DOI":"10.1145\/1811212.1811216"},{"doi-asserted-by":"publisher","key":"e_1_3_3_8_2","DOI":"10.1145\/3597495"},{"doi-asserted-by":"publisher","key":"e_1_3_3_9_2","DOI":"10.1561\/2500000049"},{"key":"e_1_3_3_10_2","first-page":"101","volume-title":"Static Analysis.","author":"Chen Liqian","year":"2014","unstructured":"Liqian Chen, Jiangchao Liu, Antoine Min\u00e9, Deepak Kapur, and Ji Wang. 2014. An Abstract Domain to Infer Octagonal Constraints with Absolute Value. In Static Analysis. Markus M\u00fcller-Olm and Helmut Seidl (Eds.), Springer International Publishing, Cham, 101\u2013117."},{"doi-asserted-by":"publisher","key":"e_1_3_3_11_2","DOI":"10.1007\/978-3-319-21690-4_44"},{"doi-asserted-by":"publisher","key":"e_1_3_3_12_2","DOI":"10.2307\/2271310"},{"doi-asserted-by":"publisher","key":"e_1_3_3_13_2","DOI":"10.1145\/234528.234740"},{"doi-asserted-by":"publisher","key":"e_1_3_3_14_2","DOI":"10.1145\/512950.512973"},{"doi-asserted-by":"publisher","key":"e_1_3_3_15_2","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_3_16_2","first-page":"11123","volume-title":"Proceedings of the Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021 (NeurIPS\u201921)","author":"Cui Guofeng","year":"2021","unstructured":"Guofeng Cui and He Zhu. 2021. Differentiable Synthesis of Program Architectures. In Proceedings of the Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021 (NeurIPS\u201921). Marc\u2019Aurelio Ranzato, Alina Beygelzimer, Yann N. Dauphin, Percy Liang, and Jennifer Wortman Vaughan (Eds.), 11123\u201311135. Retrieved from https:\/\/proceedings.neurips.cc\/paper\/2021\/hash\/5c5a93a042235058b1ef7b0ac1e11b67-Abstract.html"},{"issue":"4","key":"e_1_3_3_17_2","first-page":"611","article-title":"Neural-Symbolic Computing: An Effective Methodology for Principled Integration of Machine Learning and Reasoning","volume":"6","author":"Garcez Artur S. d\u2019Avila","year":"2019","unstructured":"Artur S. d\u2019Avila Garcez, Marco Gori, Lu\u00eds C. Lamb, Luciano Serafini, Michael Spranger, and Son N. Tran. 2019. Neural-Symbolic Computing: An Effective Methodology for Principled Integration of Machine Learning and Reasoning. FLAP 6, 4 (2019), 611\u2013632. Retrieved from https:\/\/collegepublications.co.uk\/ifcolog\/?00033","journal-title":"FLAP"},{"doi-asserted-by":"publisher","key":"e_1_3_3_18_2","DOI":"10.1145\/2509136.2509511"},{"doi-asserted-by":"publisher","key":"e_1_3_3_19_2","DOI":"10.5555\/113902"},{"key":"e_1_3_3_20_2","first-page":"1931","volume-title":"Proceedings of the 36th International Conference on Machine Learning (ICML \u201919)","volume":"97","author":"Fischer Marc","year":"2019","unstructured":"Marc Fischer, Mislav Balunovic, Dana Drachsler-Cohen, Timon Gehr, Ce Zhang, and Martin T. Vechev. 2019. DL2: Training and Querying Neural Networks with Logic. In Proceedings of the 36th International Conference on Machine Learning (ICML \u201919), Vol. 97. Kamalika Chaudhuri and Ruslan Salakhutdinov (Eds.), PMLR, 1931\u20131941. DOI: http:\/\/proceedings.mlr.press\/v97\/fischer19a.html"},{"doi-asserted-by":"publisher","key":"e_1_3_3_21_2","DOI":"10.1007\/978-3-319-08867-9_5"},{"doi-asserted-by":"publisher","key":"e_1_3_3_22_2","DOI":"10.1145\/2837614.2837664"},{"key":"e_1_3_3_23_2","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/978-3-031-13185-1_2","volume-title":"Computer Aided Verification","author":"Gurfinkel Arie","year":"2022","unstructured":"Arie Gurfinkel. 2022. Program Verification with Constrained Horn Clauses (Invited Paper). In Computer Aided Verification. Sharon Shoham and Yakir Vizel (Eds.), Springer International Publishing, Cham, 19\u201329."},{"doi-asserted-by":"publisher","key":"e_1_3_3_24_2","DOI":"10.1007\/978-3-642-15769-1_18"},{"doi-asserted-by":"publisher","key":"e_1_3_3_25_2","DOI":"10.1007\/978-3-319-21690-4_20"},{"doi-asserted-by":"publisher","key":"e_1_3_3_26_2","DOI":"10.1007\/978-94-011-5300-3"},{"doi-asserted-by":"publisher","key":"e_1_3_3_27_2","DOI":"10.1145\/363235.363259"},{"doi-asserted-by":"publisher","key":"e_1_3_3_28_2","DOI":"10.23919\/FMCAD.2018.8603013"},{"doi-asserted-by":"publisher","key":"e_1_3_3_29_2","DOI":"10.2307\/2268661"},{"doi-asserted-by":"publisher","key":"e_1_3_3_30_2","DOI":"10.1145\/3385412.3386027"},{"doi-asserted-by":"publisher","key":"e_1_3_3_31_2","DOI":"10.1007\/978-3-030-53291-8_7"},{"doi-asserted-by":"publisher","key":"e_1_3_3_32_2","DOI":"10.1145\/3428257"},{"key":"e_1_3_3_33_2","volume-title":"Proceedings of the 11th International Conference on Learning Representations","author":"Li Zenan","year":"2023","unstructured":"Zenan Li, Zehua Liu, Yuan Yao, Jingwei Xu, Taolue Chen, Xiaoxing Ma, and Jian Lu. 2023. Learning with Logical Constraints but Without Shortcut Satisfaction. In Proceedings of the 11th International Conference on Learning Representations. Retrieved from https:\/\/openreview.net\/forum?id=M2unceRvqhh"},{"doi-asserted-by":"publisher","key":"e_1_3_3_34_2","DOI":"10.2140\/pjm.1959.9.129"},{"doi-asserted-by":"publisher","key":"e_1_3_3_35_2","DOI":"10.1007\/s10990-006-8609-1"},{"doi-asserted-by":"publisher","key":"e_1_3_3_36_2","DOI":"10.1016\/j.scico.2013.09.014"},{"key":"e_1_3_3_37_2","first-page":"6938","volume-title":"Proceedings of the 37th International Conference on Machine Learning (ICML \u201920)","volume":"119","author":"Minervini Pasquale","year":"2020","unstructured":"Pasquale Minervini, Sebastian Riedel, Pontus Stenetorp, Edward Grefenstette, and Tim Rockt\u00e4schel. 2020. Learning Reasoning Strategies in End-to-End Differentiable Proving. In Proceedings of the 37th International Conference on Machine Learning (ICML \u201920), Vol. 119. PMLR, 6938\u20136949. Retrieved from http:\/\/proceedings.mlr.press\/v119\/minervini20a.html"},{"key":"e_1_3_3_38_2","first-page":"12157","volume-title":"Proceedings of the Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019 (NeurIPS \u201919)","author":"Nandwani Yatin","year":"2019","unstructured":"Yatin Nandwani, Abhishek Pathak, Mausam, and Parag Singla. 2019. A Primal Dual Formulation for Deep Learning with Constraints. In Proceedings of the Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019 (NeurIPS \u201919). Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d\u2019Alch\u00e9-Buc, Emily B. Fox, and Roman Garnett (Eds.), 12157\u201312168. Retrieved from https:\/\/proceedings.neurips.cc\/paper\/2019\/hash\/cf708fc1decf0337aded484f8f4519ae-Abstract.html"},{"doi-asserted-by":"publisher","key":"e_1_3_3_39_2","DOI":"10.1145\/3106237.3106281"},{"doi-asserted-by":"publisher","key":"e_1_3_3_40_2","DOI":"10.1007\/978-3-031-27481-7_6"},{"doi-asserted-by":"publisher","key":"e_1_3_3_41_2","DOI":"10.1145\/3540250.3549166"},{"doi-asserted-by":"publisher","key":"e_1_3_3_42_2","DOI":"10.1145\/3540250.3549166"},{"doi-asserted-by":"publisher","key":"e_1_3_3_43_2","DOI":"10.1007\/978-3-540-27864-1_21"},{"key":"e_1_3_3_44_2","volume-title":"Proceedings of the 8th International Conference on Learning Representations (ICLR \u201920)","author":"Ryan Gabriel","year":"2020","unstructured":"Gabriel Ryan, Justin Wong, Jianan Yao, Ronghui Gu, and Suman Jana. 2020. CLN2INV: Learning Loop Invariants with Continuous Logic Networks. In Proceedings of the 8th International Conference on Learning Representations (ICLR \u201920). OpenReview.net. Retrieved from https:\/\/openreview.net\/forum?id=HJlfuTEtvB"},{"key":"e_1_3_3_45_2","first-page":"111","volume-title":"Proceedings of the International Workshop on Verification, Model Checking, and Abstract Interpretation","author":"Sankaranarayanan Sriram","year":"2006","unstructured":"Sriram Sankaranarayanan, Michael A. Col\u00f3n, Henny Sipma, and Zohar Manna. 2006. Efficient Strongly Relational Polyhedral Analysis. In Proceedings of the International Workshop on Verification, Model Checking, and Abstract Interpretation. Springer, 111\u2013125."},{"key":"e_1_3_3_46_2","volume-title":"Proceedings of the 7th International Conference on Learning Representations (ICLR \u201919)","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 7th International Conference on Learning Representations (ICLR \u201919). OpenReview.net. Retrieved from https:\/\/openreview.net\/forum?id=HJMC_iA5tm"},{"key":"e_1_3_3_47_2","first-page":"7762","volume-title":"Proceedings of the Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018 (NeurIP \u201918)","author":"Si Xujie","year":"2018","unstructured":"Xujie Si, Hanjun Dai, Mukund Raghothaman, Mayur Naik, and Le Song. 2018. Learning Loop Invariants for Program Verification. In Proceedings of the Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018 (NeurIP \u201918). Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicolo Cesa-Bianchi, and Roman Garnett (Eds.), 7762\u20137773. Retrieved from https:\/\/proceedings.neurips.cc\/paper\/2018\/hash\/65b1e92c585fd4c2159d5f33b5030ff2-Abstract.html"},{"doi-asserted-by":"publisher","key":"e_1_3_3_48_2","DOI":"10.1145\/3385412.3385986"},{"doi-asserted-by":"publisher","key":"e_1_3_3_49_2","DOI":"10.1109\/TR.2019.2925037"},{"doi-asserted-by":"publisher","key":"e_1_3_3_50_2","DOI":"10.1145\/3597926.3598047"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3675394","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3675394","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:04:23Z","timestamp":1750291463000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3675394"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,30]]},"references-count":49,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2024,11,30]]}},"alternative-id":["10.1145\/3675394"],"URL":"https:\/\/doi.org\/10.1145\/3675394","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"type":"print","value":"1049-331X"},{"type":"electronic","value":"1557-7392"}],"subject":[],"published":{"date-parts":[[2024,11,30]]},"assertion":[{"value":"2023-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-06-19","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-12-03","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}