{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:09Z","timestamp":1780994709044,"version":"3.54.1"},"reference-count":41,"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\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-1910769, CCF-1917852"],"award-info":[{"award-number":["CCF-1910769, CCF-1917852"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000183","name":"Army Research Office","doi-asserted-by":"publisher","award":["W911NF-20-1-0080"],"award-info":[{"award-number":["W911NF-20-1-0080"]}],"id":[{"id":"10.13039\/100000183","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100008536","name":"Amazon Web Services","doi-asserted-by":"publisher","award":["ASSET Gift for Research in Trustworthy AI"],"award-info":[{"award-number":["ASSET Gift for Research in Trustworthy AI"]}],"id":[{"id":"10.13039\/100008536","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            We consider the problem of synthesizing programs with numerical constants that optimize a quantitative objective, such as accuracy, over a set of input-output examples. We propose a general framework for optimal synthesis of such programs in a given domain specific language (DSL), with provable optimality guarantees. Our framework enumerates programs in a general search graph, where nodes represent subsets of concrete programs. To improve scalability, it uses\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mrow>\n                  <mml:msup>\n                    <mml:mi>A<\/mml:mi>\n                    <mml:mo>*<\/mml:mo>\n                  <\/mml:msup>\n                <\/mml:mrow>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            search in conjunction with a search heuristic based on abstract interpretation; intuitively, this heuristic establishes upper bounds on the value of subtrees in the search graph, enabling the synthesizer to identify and prune subtrees that are provably suboptimal. In addition, we propose a natural strategy for constructing abstract transformers for monotonic semantics, which is a common property for components in DSLs for data classification. Finally, we implement our approach in the context of two such existing DSLs, demonstrating that our algorithm is more scalable than existing optimal synthesizers.\n          <\/jats:p>","DOI":"10.1145\/3632858","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"457-481","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Optimal Program Synthesis via Abstract Interpretation"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-7469-8974","authenticated-orcid":false,"given":"Stephen","family":"Mell","sequence":"first","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3516-1512","authenticated-orcid":false,"given":"Steve","family":"Zdancewic","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9990-7566","authenticated-orcid":false,"given":"Osbert","family":"Bastani","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","first-page":"6172","volume":"33","author":"Anderson Greg","year":"2020","unstructured":"Greg Anderson , Abhinav Verma , Isil Dillig , and Swarat Chaudhuri . 2020. Neurosymbolic reinforcement learning with formally verified exploration. Advances in neural information processing systems 33 (2020), 6172\u20136183.","journal-title":"Advances in neural information processing systems"},{"key":"e_1_3_1_3_1","first-page":"177","volume":"8","author":"Bansal Sorav","year":"2008","unstructured":"Sorav Bansal and Alex Aiken . 2008. Binary Translation Using Peephole Superoptimizers.. In OSDI, Vol. 8. 177\u2013192.","journal-title":"OSDI"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","unstructured":"Favyen Bastani Songtao He Arjun Balasingam Karthik Gopalakrishnan Mohammad Alizadeh Hari Balakrishnan Michael Cafarella Tim Kraska and Sam Madden . 2020. MIRIS: Fast Object Track Queries in Video. In Proceedings of the 2020 ACM SIGMOD International Conference on Management of Data. 1907\u20131921. https:\/\/doi.org\/10.1145\/3318464.3389692 10.1145\/3318464.3389692","DOI":"10.1145\/3318464.3389692"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","unstructured":"Favyen Bastani Songtao He Ziwen Jiang Osbert Bastani and Sam Madden . 2021. SkyQuery: an aerial drone video sensing platform. In Proceedings of the 2021 ACM SIGPLAN International Symposium on New Ideas New Paradigms and Reflections on Programming and Software. 56\u201367. https:\/\/doi.org\/10.1145\/3486607.3486750 10.1145\/3486607.3486750","DOI":"10.1145\/3486607.3486750"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","unstructured":"James Bornholt Emina Torlak Dan Grossman and Luis Ceze . 2016. Optimizing synthesis with metasketches. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 775\u2013788. https:\/\/doi.org\/10.1145\/2837614.2837666 10.1145\/2837614.2837666","DOI":"10.1145\/2837614.2837666"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","unstructured":"Xavier P. Burgos-Artizzu Piotr Doll\u00e1r Dayu Lin David J. Anderson and Pietro Perona . 2012. Social behavior recognition in continuous video. In 2012 IEEE Conference on Computer Vision and Pattern Recognition. 1322\u20131329. https:\/\/doi.org\/10.1109\/CVPR.2012.6247817 10.1109\/CVPR.2012.6247817","DOI":"10.1109\/CVPR.2012.6247817"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_20"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000049"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","unstructured":"Qiaochu Chen Arko Banerjee \u00c7a\u011fatay Demiralp Greg Durrett and Isil Dillig . 2023. Data Extraction via Semantic Regular Expression Synthesis. In OOPSLA. https:\/\/doi.org\/10.1145\/3622863 10.1145\/3622863","DOI":"10.1145\/3622863"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","unstructured":"Qiaochu Chen Aaron Lamoreaux Xinyu Wang Greg Durrett Osbert Bastani and Isil Dillig . 2021. Web question answering with neurosymbolic program synthesis. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 328\u2013343. https:\/\/doi.org\/10.1145\/3453483.3454047 10.1145\/3453483.3454047","DOI":"10.1145\/3453483.3454047"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","unstructured":"Patrick Cousot and Radhia Cousot . 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. 238\u2013252. https:\/\/doi.org\/10.1145\/512950.512973 10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_32"},{"key":"e_1_3_1_15_1","unstructured":"Alexander L Gaunt Marc Brockschmidt Rishabh Singh Nate Kushman Pushmeet Kohli Jonathan Taylor and Daniel Tarlow . 2016. Terpret: A probabilistic programming language for program induction. arXiv preprint arXiv:1608.04428 (2016)."},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1609\/icaps.v22i1.13505"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","unstructured":"Sumit Gulwani Susmit Jha Ashish Tiwari and Ramarathnam Venkatesan . 2011. Synthesis of Loop-Free Programs. In PLDI\u201911 June 4-8 2011 San Jose California USA (pldi\u201911 june 4\u20138 2011 san jose california usa ed.). https:\/\/doi.org\/10.1145\/1993498.1993506 10.1145\/1993498.1993506","DOI":"10.1145\/1993498.1993506"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591285"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1613\/jair.1144"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1613\/jair.855"},{"key":"e_1_3_1_21_1","first-page":"13597","volume":"33","author":"Inala Jeevana Priya","year":"2020","unstructured":"Jeevana Priya Inala , Yichen Yang , James Paulos , Yewen Pu , Osbert Bastani , Vijay Kumar , Martin Rinard , and Armando Solar-Lezama . 2020. Neurosymbolic transformers for multi-agent communication. Advances in Neural Information Processing Systems 33 (2020), 13597\u201313608.","journal-title":"Advances in Neural Information Processing Systems"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/3897.001.0001"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_3_1_24_1","first-page":"222","volume-title":"ICAPS","author":"Marthi Bhaskara","year":"2008","unstructured":"Bhaskara Marthi , Stuart Russell , and Jason Andrew Wolfe . 2008. Angelic Hierarchical Planning: Optimal and Online Algorithms.. In ICAPS. Citeseer, 222\u2013231."},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/36177.36194"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","unstructured":"Stephen Mell . 2023. Artifact for Optimal Program Synthesis via Abstract Interpretation. https:\/\/doi.org\/10.5281\/zenodo.10146270 10.5281\/zenodo.10146270","DOI":"10.5281\/zenodo.10146270"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37706-8_23"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428245"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","unstructured":"Phitchaya Mangpo Phothilimthana Aditya Thakur Rastislav Bodik and Dinakar Dhurjati . 2016. Scaling up superoptimization. In Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems. 297\u2013310. https:\/\/doi.org\/10.1145\/2872362.2872387 10.1145\/2872362.2872387","DOI":"10.1145\/2872362.2872387"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","unstructured":"Raimondas Sasnauskas Yang Chen Peter Collingbourne Jeroen Ketema Gratian Lup Jubi Taneja and John Regehr . 2017. Souper: A synthesizing superoptimizer. arXiv preprint arXiv:1711.04422 (2017). https:\/\/doi.org\/10.48550\/arXiv.1711.04422 10.48550\/arXiv.1711.04422","DOI":"10.48550\/arXiv.1711.04422"},{"key":"e_1_3_1_31_1","first-page":"4940","volume":"33","author":"Shah Ameesh","year":"2020","unstructured":"Ameesh Shah , Eric Zhan , Jennifer Sun , Abhinav Verma , Yisong Yue , and Swarat Chaudhuri . 2020. Learning differentiable programs with admissible neural heuristics. Advances in neural information processing systems 33 (2020), 4940\u20134952.","journal-title":"Advances in neural information processing systems"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2980983.2908102"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66706-5_18"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","unstructured":"Jennifer J. Sun Brian Geuther Vivek Kumar Alice Robie Catherine Schretter Keith Sheppard Dipam Chakraborty Kristin Branson and Ann Kennedy . 2022. The MABe22 Benchmarks for Representation Learning of Multi-Agent Behavior. https:\/\/doi.org\/10.22002\/D1.20186 10.22002\/D1.20186","DOI":"10.22002\/D1.20186"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","unstructured":"Jennifer J Sun Tomomi Karigo Dipam Chakraborty Sharada P Mohanty Benjamin Wild Quan Sun Chen Chen David J Anderson Pietro Perona Yisong Yue and Ann Kennedy . 2021. The Multi-Agent Behavior Dataset: Mouse Dyadic Social Interactions. arXiv preprint arXiv:2104.02710 (2021). https:\/\/doi.org\/10.48550\/arXiv.2104.02710 10.48550\/arXiv.2104.02710","DOI":"10.48550\/arXiv.2104.02710"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","unstructured":"Bochen Tan and Jason Cong . 2020. Optimal layout synthesis for quantum computing. In Proceedings of the 39th International Conference on Computer-Aided Design. 1\u20139. https:\/\/doi.org\/10.1145\/3400302.3415620 10.1145\/3400302.3415620","DOI":"10.1145\/3400302.3415620"},{"key":"e_1_3_1_38_1","volume":"31","author":"Valkov Lazar","year":"2018","unstructured":"Lazar Valkov , Dipak Chaudhari , Akash Srivastava , Charles Sutton , and Swarat Chaudhuri . 2018. Houdini: Lifelong learning as program synthesis. Advances in neural information processing systems 31 (2018).","journal-title":"Advances in neural information processing systems"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2018\/674"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158151"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","unstructured":"Xi Ye Qiaochu Chen Isil Dillig and Greg Durrett . 2021. Optimal Neural Program Synthesis from Multimodal Specifications. In Findings of the Association for Computational Linguistics: EMNLP 2021. 1691\u20131704. https:\/\/doi.org\/10.18653\/v1\/2021.findings-emnlp.146 10.18653\/v1\/2021.findings-emnlp.146","DOI":"10.18653\/v1\/2021.findings-emnlp.146"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","unstructured":"Tan Zhi-Xuan Joshua B. Tenenbaum and Vikash K. Mansinghka . 2022. Abstract Interpretation for Generalized Heuristic Search in Model-Based Planning. https:\/\/doi.org\/10.48550\/arXiv.2208.02938 10.48550\/arXiv.2208.02938 arXiv:2208.02938 [cs.AI].","DOI":"10.48550\/arXiv.2208.02938"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632858","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632858","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632858","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:03:43Z","timestamp":1751659423000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632858"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":41,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632858"],"URL":"https:\/\/doi.org\/10.1145\/3632858","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"}}]}}