Student or educator? Sign up with your school email and get 6 months of Pro free.
CoChat
Sign Up
Cited by 0

The DOI matches its Crossref record; 3 of the 3 references it cites were found in a registry or an index.

SAIL: Sound Abstract Interpreters with LLMs

Gu, Qiuhan, Singh, Avaljot, Singh, Gagandeep·2026·Proceedings of the ACM on Programming Languages
DOI 10.1145/3808308

Published version of a preprint

Open this paper in CoChat — free account

Abstract

How to construct globally sound abstract interpreters to safely approximate program behaviors remains a bottleneck in abstract interpretation. In this paper, we show the potential of using state-of-the-art LLMs to automate this tedious process. Focusing on the neural network verification area, we synthesize non-trivial sound abstract transformers across diverse abstract domains using LLMs to search within infinite space from scratch. We formalize the synthesis task as a constrained optimization problem, for which we design a novel mathematically grounded cost function that measures the degree of unsoundness of each generated candidate transformer, while enforcing hard syntactic and semantic validity constraints. Building on this formulation, we introduce Sail , a novel unified framework that combines model generation, syntactic and semantic validation, and cost-function-based refinement to synthesize globally sound abstract transformers. Evaluation results show that Sail not only matches the performance of manually designed transformers, but also is able to synthesize sound and high-precision transformers that do not exist in the literature for complex non-linear operators.

Overview

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

Crossref · 10.1145/3808308

Cites

3 of 3 references verified0 citation errors · 0 not checkable

Statistics

Verification

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Citations

Cites

Research works printed but not linked: 72

  1. Martín Abadi Paul Barham Jianmin Chen Zhifeng Chen Andy Davis Jeffrey Dean Matthieu Devin Sanjay Ghemawat Geoffrey Irving Michael Isard Manjunath Kudlur Josh Levenberg Rajat Monga Sherry Moore Derek G. Murray Benoit Steiner Paul Tucker Vijay Vasudevan Pete Warden Martin Wicke Yuan Yu and Xiaoqiang Zheng . 2016. TensorFlow: A system for large-scale machine learning. https://arxiv.org/abs/1605.08695 · arXiv
  2. Rajeev Alur Rastislav Bodik Garvit Juniwal Milo M. K. Martin Mukund Raghothaman Sanjit A. Seshia Rishabh Singh Armando Solar-Lezama Emina Torlak and Abhishek Udupa . 2013. Syntax-guided synthesis. In 2013 Formal Methods in Computer-Aided Design. 1–8. doi:10.1109/FMCAD.2013.6679385 · DOI · Paper page
  3. Rajeev Alur Arjun Radhakrishna and Abhishek Udupa . 2017. Scaling enumerative program synthesis via divide and conquer. In International conference on tools and algorithms for the construction and analysis of systems. 319–336. · DOI
  4. Jacob Austin Augustus Odena Maxwell Nye Maarten Bosma Henryk Michalewski David Dohan Ellen Jiang Carrie Cai Michael Terry Quoc Le and . 2021. Program Synthesis with Large Language Models. https://arxiv.org/abs/2108.07732 · arXiv
  5. Clark Barrett Swarat Chaudhuri Fabrizio Montesi Jim Grundy Pushmeet Kohli Leonardo de Moura Alexandre Rademaker and Sorrachai Yingchareonthawornchai . 2026. CSLib: The Lean Computer Science Library. https://arxiv.org/abs/2602.04846 · arXiv
  6. Atilim Gunes Baydin Barak A. Pearlmutter Alexey Andreyevich Radul and Jeffrey Mark Siskind . 2018. Automatic differentiation in machine learning: a survey. https://arxiv.org/abs/1502.05767 · arXiv
  7. Bruno Blanchet Patrick Cousot Radhia Cousot Jérôme Feret Laurent Mauborgne Antoine Miné David Monniaux and Xavier Rival . 2002. Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. 85-108. · DOI · Paper page
  8. Olivier Bouissou and Matthieu Martel . 2008. Abstract Interpretation of the Physical Inputs of Embedded Programs. In Verification Model Checking and Abstract Interpretation Francesco Logozzo Doron A. Peled Lenore D. Zuck (Eds.). 37–51. · DOI
  9. Christopher Brix Stanley Bak Taylor T. Johnson and Haoze Wu . 2024. The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results. https://arxiv.org/abs/2412.19985 · arXiv
  10. Yufan Cai Zhe Hou David Sanan Xiaokun Luan Yun Lin Jun Sun and Jin Song Dong . 2025. Automated Program Refinement: Guide and Verify Code Large Language Model with Refinement Calculus. Proc. ACM Program. Lang. POPL Article 69 (Jan. 2025). doi:10.1145/3704905 · DOI
  11. Jose Cambronero Hongyu Li Seohyun Kim Koushik Sen and Satish Chandra . 2019. When Deep Learning Met Code Search. https://arxiv.org/abs/1905.03813 · arXiv
  12. Marco Campion Mila Dalla Preda and Roberto Giacobazzi . 2022. Partial (In)Completeness in abstract interpretation: limiting the imprecision in program analysis. Proc. ACM Program. Lang. POPL Article 59 (Jan. 2022). doi:10.1145/3498721 · DOI
  13. 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 (POPL '77). 238–252. doi:10.1145/512950.512973 · DOI · Paper page
  14. Patrick Cousot and Radhia Cousot . 1979. Systematic design of program analysis frameworks. In Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL '79). 269–282. doi:10.1145/567752.567778 · DOI · Paper page
  15. Patrick Cousot Radhia Cousot Jerôme Feret Laurent Mauborgne Antoine Miné David Monniaux and Xavier Rival . 2005. The ASTREÉ analyzer. In Proceedings of the 14th European Conference on Programming Languages and Systems (ESOP'05). 21–30. doi:10.1007/978-3-540-31987-0_3 · DOI · Paper page
  16. George B Dantzig . 1973. Fourier-Motzkin elimination and its dual. Technical Report. · DOI
  17. DeepSeek-AI Daya Guo . 2025. DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning. https://arxiv.org/abs/2501.12948 · arXiv
  18. 10.1109/MSP.2012.2211477 · DOI · Paper page
  19. Alessandra Di Pierro and Herbert Wiklicky . 2000. Measuring the precision of abstract interpretations. In International Workshop on Logic-Based Program Synthesis and Transformation. 147–164. · DOI
  20. 10.1145/2914770.2837664 · DOI
  21. Timon Gehr Matthew Mirman Dana Drachsler-Cohen Petar Tsankov Swarat Chaudhuri and Martin Vechev . 2018. AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation. In 2018 IEEE Symposium on Security and Privacy (SP). 3–18. doi:10.1109/SP.2018.00058 · DOI
  22. Robert Joseph George Jennifer Cruden Xiangru Zhong Huan Zhang and Anima Anandkumar . 2026. TorchLean: Formalizing Neural Networks in Lean. https://arxiv.org/abs/2602.22631 · arXiv
  23. 10.1145/333979.333989 · DOI
  24. Shaurya Gomber Debangshu Banerjee and Gagandeep Singh . 2025. Universal Synthesis of Differentiably Tunable Numerical Abstract Transformers. https://arxiv.org/abs/2507.11827 · arXiv
  25. Sven Gowal Krishnamurthy Dvijotham Robert Stanforth Rudy Bunel Chongli Qin Jonathan Uesato Relja Arandjelovic Timothy Mann and Pushmeet Kohli . 2019. On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models. https://arxiv.org/abs/1810.12715 · arXiv
  26. Arya Grayeli Atharva Sehgal Omar Costilla-Reyes Miles Cranmer and Swarat Chaudhuri . 2024. Symbolic Regression with a Learned Concept Library. https://arxiv.org/abs/2409.09359 · DOI
  27. 10.1561/2500000010 · DOI · Paper page
  28. Kihong Heo Hakjoo Oh and Kwangkeun Yi . 2017. Machine-Learning-Guided Selectively Unsound Static Analysis. In 2017 IEEE/ACM 39th International Conference on Software Engineering (ICSE). 519–529. doi:10.1109/ICSE.2017.54 · DOI
  29. Naman Jain Skanda Vaidyanath Arun Iyer Nagarajan Natarajan Suresh Parthasarathy Sriram Rajamani and Rahul Sharma . 2022. Jigsaw: Large language models meet program synthesis. In Proceedings of the 44th International Conference on Software Engineering. 1219–1231. · DOI
  30. Jacques-Henri Jourdan Vincent Laporte Sandrine Blazy Xavier Leroy and David Pichardie . 2015. A Formally-Verified C Static Analyzer. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '15). 247–259.doi:10.1145/2676726.2676966 · DOI
  31. 10.1145/1921532.1921553 · DOI
  32. 10.1145/3563334 · DOI
  33. Pankaj Kumar Kalita Thomas Reps and Subhajit Roy . 2025. Automated Abstract Transformer Synthesis for Reduced Product Domains. ACM Transactions on Software Engineering and Methodology (2025).
  34. Jacob Laurel Rem Yang Shubham Ugare Robert Nagel Gagandeep Singh and Sasa Misailovic . 2022. A general construction for abstract interpretation of higher-order automatic differentiation. Proc. ACM Program. Lang. 6 OOPSLA2 Article 161 (Oct. 2022). doi:10.1145/3563324 · DOI
  35. Maikel Leon . 2025. GPT-5 and open-weight large language models: Advances in reasoning transparency and control. Information Systems (2025) 102620. · DOI
  36. Tzu-Mao Li Michaël Gharbi Andrew Adams Frédo Durand and Jonathan Ragan-Kelley . 2018. Differentiable programming for image processing and deep learning in halide. ACM Trans. Graph. 37 4 Article 139 (July 2018). doi:10.1145/3197517.3201383 · DOI
  37. 10.1126/science.abq1158 · DOI · Paper page
  38. Changliu Liu Tomer Arnon Christopher Lazarus Christopher Strong Clark Barrett and Mykel J. Kochenderfer . 2020. Algorithms for Verifying Deep Neural Networks. https://arxiv.org/abs/1903.06758 · DOI
  39. 10.1145/3571209 · DOI
  40. Aman Madaan Niket Tandon Prakhar Gupta Skyler Hallinan Luyu Gao Sarah Wiegreffe Uri Alon Nouha Dziri Shrimai Prabhumoye Yiming Yang Shashank Gupta Bodhisattwa Prasad Majumder Katherine Hermann Sean Welleck Amir Yazdanbakhsh and Peter Clark . 2023. Self-Refine: Iterative Refinement with Self-Feedback. https://arxiv.org/abs/2303.17651 · DOI · Paper page
  41. Antoine Miné . 2006. Symbolic methods to enhance the precision of numerical abstract domains. In International Workshop on Verification Model Checking and Abstract Interpretation. 348–363. · DOI
  42. 10.1016/j.entcs.2017.02.002 · DOI
  43. Matthew Mirman Timon Gehr and Martin T. Vechev . 2018. Differentiable Abstract Interpretation for Provably Robust Neural Networks. In International Conference on Machine Learning. https://api.semanticscholar.org/CorpusID:51872670
  44. Erik Nijkamp Bo Pang Hiroaki Hayashi Lifu Tu Huan Wang Yingbo Zhou Silvio Savarese and Caiming Xiong . 2023. CodeGen: An Open Large Language Model for Code with Multi-Turn Program Synthesis. https://arxiv.org/abs/2203.13474 · arXiv
  45. 10.1007/978-3-031-13185-1_8 · DOI
  46. Brandon Paulsen and Chao Wang . 2022. LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions. https://arxiv.org/abs/2201.13351 · DOI
  47. Stanislas Polu and Ilya Sutskever . 2020. Generative Language Modeling for Automated Theorem Proving. https://arxiv.org/abs/2009.03393 · arXiv
  48. Thomas Reps and Aditya Thakur . 2016. Automating Abstract Interpretation. In Proceedings of the 17th International Conference on Verification Model Checking and Abstract Interpretation - Volume 9583 (VMCAI 2016). 3–40. doi:10.1007/978-3-662-49122-5_1 · DOI
  49. 10.1038/s41586-023-06924-6 · DOI · Paper page
  50. Parshin Shojaee Kazem Meidani Shashank Gupta Amir Barati Farimani and Chandan K Reddy . 2025. LLM-SR: Scientific Equation Discovery via Programming with Large Language Models. https://arxiv.org/abs/2404.18400 · arXiv
  51. Avaljot Singh Yasmin Sarita Charith Mendis and Gagandeep Singh . 2024. ConstraintFlow: A Declarative DSL for Easy Development of DNN Certifiers. 407-424. doi:10.1007/978-3-031-74776-2_16 · DOI
  52. Avaljot Singh Yasmin Chandini Sarita Charith Mendis and Gagandeep Singh . 2025. Automated Verification of Soundness of DNN Certifiers. Proc. ACM Program. Lang. OOPSLA1 Article 144 (April 2025). doi:10.1145/3720509 · DOI
  53. Avaljot Singh Yamin Chandini Sarita Aditya Mishra Ishaan Goyal Gagandeep Singh and Charith Mendis . 2025. A Tensor-Based Compiler and a Runtime for Neuron-Level DNN Certifier Specifications. https://arxiv.org/abs/2507.20055 · arXiv
  54. Gagandeep Singh and Deepika Chawla . 2025. Position: Formal Methods are the Principled Foundation of Safe AI. In ICML Workshop on Technical AI Governance (TAIG). https://openreview.net/forum?id=7V5CDSsjB7
  55. Gagandeep Singh Timon Gehr Matthew Mirman Markus Püschel and Martin Vechev . 2018. Fast and effective robustness certification. In Proceedings of the 32nd International Conference on Neural Information Processing Systems (NIPS'18). 10825–10836.
  56. Gagandeep Singh Timon Gehr Markus Püschel and Martin Vechev . 2019. An abstract domain for certifying neural networks. Proc. ACM Program. Lang. POPL Article 41 (Jan. 2019). doi:10.1145/3290354 · DOI
  57. Gagandeep Singh Timon Gehr Markus Püschel and Martin T. Vechev . 2018. Boosting Robustness Certification of Neural Networks. In International Conference on Learning Representations. https://api.semanticscholar.org/CorpusID:196059499
  58. 10.1561/2500000062 · DOI
  59. Gagandeep Singh Markus Püschel and Martin Vechev . 2017. Fast polyhedra abstract domain. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. 46–59. · DOI
  60. Armando Solar-Lezama . 2009. The sketching approach to program synthesis. In Asian symposium on programming languages and systems. 4–13. · DOI
  61. Armando Solar-Lezama . 2013. Program sketching. Int. 7. Softw. Tools Technol. Transf. 5-6 (Oct. 2013) 475-495. doi:10.1007/s10009-012-0249-7 · DOI
  62. Benno Stein Bor-Yuh Evan Chang and Manu Sridharan . 2021. Demanded abstract interpretation. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2021). 282–295. doi:10.1145/3453483.3454044 · DOI
  63. Gemini Team Rohan Anil and . 2025. Gemini: A Family of Highly Capable Multimodal Models. https://arxiv.org/abs/2312.11805 · arXiv
  64. Andrea Walther . 2009. Getting Started with ADOL-C. In Combinatorial Scientific Computing (Dagstuhl Seminar Proceedings (DagSemProc) Vol. 9061) 1–10. doi:10.4230/DagSemProc.09061.10 · DOI
  65. 10.1109/TSE.2020.2979701 · DOI
  66. Yixuan Wang Chao Huang Zhaoran Wang Zhilu Wang and Qi Zhu . 2021. Verification in the Loop: Correct-byConstruction Control Learning with Reach-avoid Guarantees. https://arxiv.org/abs/2106.03245 · arXiv
  67. Guannan Wei Zhuo Zhang and Caterina Urban . 2025. Hallucination-Resilient LLM-Driven Sound and Tunable Static Analysis: A Case of Higher-Order Control-Flow Analysis. In Proceedings of the 1st ACM SIGPLAN International Workshop on Language Models and Programming Languages (LMPL '25). 6–11. doi:10.1145/3759425.3763378 · DOI
  68. 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. https://arxiv.org/abs/2011.13824 · arXiv
  69. Ziwei Xu Sanjay Jain and Mohan Kankanhalli . 2025. Hallucination is Inevitable: An Innate Limitation of Large Language Models. https://arxiv.org/abs/2401.11817 · arXiv
  70. Chenxi Yang and Swarat Chaudhuri . 2022. Safe Neurosymbolic Learning with Differentiable Symbolic Execution. https://arxiv.org/abs/2203.07671 · arXiv
  71. Huan Zhang Hongge Chen Chaowei Xiao Sven Gowal Robert Stanforth Bo Li Duane Boning and Cho-Jui Hsieh . 2019. Towards Stable and Efficient Training of Verifiably Robust Neural Networks. https://arxiv.org/abs/1906.06316 · arXiv
  72. Huan Zhang Tsui-Wei Weng Pin-Yu Chen Cho-Jui Hsieh and Luca Daniel . 2018. Efficient Neural Network Robustness Certification with General Activation Functions. https://arxiv.org/abs/1811.00866 · arXiv

Metadata

Authors
Gu, Q., Singh, A., & Singh, G.
Venue
Proceedings of the ACM on Programming Languages
Publisher
Association for Computing Machinery (ACM)
Published
2026-06-08
Volume
10
Issue
PLDI
Pages
1534-1559
ISSN
2475-1421
DOI
10.1145/3808308
Cited by
0
References
3
Language
en
Licence
creativecommons.org/licenses/by-nc-nd/4.0/legalcode (vor)

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review

Data sources

Bibliographic data: Semantic Scholar, OpenAlex, Crossref.

Contains information from the Semantic Scholar Academic Graph Datasets, made available under the ODC Attribution License (ODC-BY 1.0).

Semantic Scholar’s data is described in: Kinney, R., et al. (2023). The Semantic Scholar Open Data Platform. arXiv:2301.10140.