{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:12:35Z","timestamp":1784837555605,"version":"3.55.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T00:00:00Z","timestamp":1766102400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Commun. ACM"],"published-print":{"date-parts":[[2026,1]]},"abstract":"<jats:p>In certifiable machine learning, AI systems produce not only results but also verifiable certificates that the results can be trusted.<\/jats:p>","DOI":"10.1145\/3737447","type":"journal-article","created":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T22:03:02Z","timestamp":1766095382000},"page":"66-75","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Certificates in AI: Learn but Verify"],"prefix":"10.1145","volume":"69","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"first","affiliation":[{"name":"Stanford University, Stanford, California, United States"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2985-7724","authenticated-orcid":false,"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[{"name":"ISTA, Klosterneuburg, Lower Austria, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6190-8707","authenticated-orcid":false,"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[{"name":"University of California Berkeley, Berkeley, California, United States"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,12,19]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3447928.3456646"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3183713.3196891"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3355089.3356549"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-45329-8_17"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.52202\/079017-1310"},{"key":"e_1_3_1_7_2","unstructured":"Bhatia S. Qiu J. Seshia S.A. and Cheung A. Can LLMs perform verified lifting of code? Technical Report UCB\/EECS-2024-11 University of California Berkeley (Mar. 2024)."},{"key":"e_1_3_1_8_2","first-page":"3240","volume-title":"Proceedings of the 33rd Intern. Conf. on Neural Information Processing Systems.","author":"Chang Y-C.","year":"2019","unstructured":"Chang, Y-C., Roohi, N., and Gao, S. Neural Lyapunov control. In Proceedings of the 33rd Intern. Conf. on Neural Information Processing Systems.\u00a0Curran Associates\u00a0(2019), 3240\u20133249."},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30823-9_1"},{"key":"e_1_3_1_10_2","doi-asserted-by":"crossref","unstructured":"Cheung A. Solar-Lezama A. and Madden S. Optimizing database-backed applications with query synthesis. In Proceedings of the Conf. on Programming Language Design and Implementation.\u00a0ACM (2013) 3\u201314.","DOI":"10.1145\/2491956.2462180"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_3_1_12_2","doi-asserted-by":"crossref","unstructured":"Cotroneo D. Improta C. Liguori P. and Natella R. Vulnerabilities in AI code generators: Exploring targeted data poisoning attacks. In\u00a0Proceedings of the 32nd IEEE\/ACM Intern. Conf. on Program Comprehension. ACM (2023).","DOI":"10.1145\/3643916.3644416"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2022.3232542"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3561048"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-017-0294-5"},{"key":"e_1_3_1_16_2","first-page":"13021","volume-title":"Proceedings of the 33rd Intern. Conf. on Neural Information Processing Systems.","author":"Jothimurugan K.","year":"2019","unstructured":"Jothimurugan, K., Alur, R., and Bastani, O. A composable specification language for reinforcement learning tasks. In Proceedings of the 33rd Intern. Conf. on Neural Information Processing Systems.\u00a0Curran Associates\u00a0(2019), 13021\u201313030."},{"key":"e_1_3_1_17_2","doi-asserted-by":"crossref","unstructured":"Lattuada A. et al. Verus: Verifying Rust programs using linear ghost types.\u00a0Proceedings ACM Program. Lang. 7 OOPSLA1\u00a0(Apr. 2023).","DOI":"10.1145\/3586037"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v36i7.20695"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1126\/science.abq1158"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1561\/2400000035"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3624007.3624053"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2021\/366"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/357084.357090"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3527315"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v36i11.21499"},{"key":"e_1_3_1_27_2","unstructured":"Mukherjee P. and Delaware B. Towards automated verification of LLM-synthesized C programs.\u00a0arXiv:2410.14835\u00a0(2024)."},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v39i26.34966"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2007.902736"},{"key":"e_1_3_1_31_2","first-page":"2205","volume-title":"USENIX Security Symp.","author":"Sandoval G.","year":"2023","unstructured":"Sandoval, G. et al. Lost at C: A user study on the security implications of large language model code assistants. In USENIX Security Symp.\u00a0USENIX Association\u00a0(2023), 2205\u20132222."},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2015.2471838"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2018.8556946"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65112-0_7"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-88494-9_19"},{"key":"e_1_3_1_37_2","first-page":"153","volume-title":"Proceedings of the Conf. on Formal Methods in Computer-Aided Design.","author":"Torfah H.","year":"2021","unstructured":"Torfah, H. et al. Synthesizing Pareto-optimal interpretations for black-box models. In Proceedings of the Conf. on Formal Methods in Computer-Aided Design.\u00a0IEEE\u00a0(2021), 153\u2013162."},{"key":"e_1_3_1_38_2","first-page":"11926","volume-title":"Proceedings of the Conf. on Artificial Intelligence.","author":"\u017dikeli\u0107 \u0110.","year":"2023","unstructured":"\u017dikeli\u0107, \u0110., Lechner, M., Henzinger, T.A., and Chatterjee, K. Learning control policies for stochastic systems with reach-avoid guarantees. In Proceedings of the Conf. on Artificial Intelligence.\u00a0AAAI Press\u00a0(2023), 11926\u201311935."},{"key":"e_1_3_1_39_2","volume-title":"Proceedings of the Conf. on Neural Information Processing Systems","author":"\u017dikeli\u0107 \u0110.","year":"2023","unstructured":"\u017dikeli\u0107, \u0110. et al. Compositional policy learning in stochastic control systems with formal guarantees. In Proceedings of the Conf. on Neural Information Processing Systems. Curran Associates\u00a0(2023)."},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65630-9_13"},{"key":"e_1_3_1_41_2","first-page":"22247","volume-title":"Proceedings of the Conf. on Neural Information Processing Systems.","author":"Wu M.","year":"2023","unstructured":"Wu, M., Wu, H., and Barrett, C. VeriX: Towards verified explainability of deep neural networks. In Proceedings of the Conf. on Neural Information Processing Systems.\u00a0Curran Associates\u00a0(2023), 22247\u201322268."}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3737447","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T21:20:18Z","timestamp":1766179218000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3737447"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,12,19]]},"references-count":40,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,1]]}},"alternative-id":["10.1145\/3737447"],"URL":"https:\/\/doi.org\/10.1145\/3737447","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,12,19]]},"assertion":[{"value":"2024-10-07","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-12-19","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}