Pith. sign in

REVIEW 3 major objections 5 minor 69 references

This paper claims that cost-guided LLM iterations can synthesize globally sound abstract transformers for neural-network verification, including novel ones that were previously missing from the literature.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-03 21:43 UTC pith:6RVE3BLZ

load-bearing objection Solid framework, unverified headline: the SMT-verified piecewise-linear transformers and the cost-guided loop are real contributions, but the claimed sound GELU/ELU/Sigmoid transformers rest on missing manual proofs. the 3 major comments →

arxiv 2511.13663 v2 pith:6RVE3BLZ submitted 2025-11-17 cs.PL cs.LG

SAIL: Sound Abstract Interpreters with LLMs

Qiuhan Gu , Avaljot Singh , Gagandeep Singh This is my paper
classification cs.PL cs.LG MSC 68Q6068T07
keywords abstract interpretationabstract transformer synthesisLLM program synthesisneural network verificationsoundnesscost-guided refinementDeepPoly domaincounterexample-guided synthesis
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Writing a sound abstract transformer—the component that lets a verifier over-approximate a neural-network operator—is a slow expert task. The paper argues that a large language model can do it, provided the search is turned into an optimization problem with a quantitative measure of unsoundness. Candidates are generated, statically checked, and submitted to an SMT-based soundness verifier; when verification fails, a cost function scores how far the candidate is from sound and the counterexamples feed the next round. The paper claims this loop converges to a globally sound transformer and demonstrates results matching handcrafted transformers, plus new sound transformers for activations like GELU and Sigmoid that had none. A sympathetic reader would take the contribution as a step toward automating the construction of provably sound analyzers.

Core claim

LLM candidates, filtered by validation and scored by a soundness-deviation cost function, can be refined into transformers that are sound for all abstract inputs, not just sampled ones. Synthesis is formalized as constrained optimization over an infinite search space, with a cost aggregating distances of concrete outputs from abstract constraints. The cost is zero exactly at soundness, so search becomes guided descent; a convergence theorem says that refinements lowering cost by a fixed positive margin reach a sound transformer in finitely many steps. Evaluation matches handcrafted precision and yields previously missing sound transformers for HardSigmoid, GELU, ELU, and Sigmoid, with the la

What carries the argument

The load-bearing object is the soundness-deviation cost function Δ_S(F#): for a candidate transformer F#, it aggregates, over violating abstract elements and points in their concretizations, the distance between the concrete output of the operator and the candidate's abstract output constraints (scalar or affine bounds). It is zero if and only if the transformer is globally sound. Around it, the framework builds an iterative loop: generate candidates with an LLM, validate syntax and semantics (repairing errors), run an SMT-based soundness checker, score unsound candidates, and feed the best one plus counterexamples into the next prompt. The cost function turns an infinite, pass/fail search i

Load-bearing premise

For the novel nonlinear activations GELU, ELU, and Sigmoid, the paper's claim of global soundness rests on the authors' manual verification rather than the automated solver, because the underlying SMT solver cannot reason about those functions; if any of those manual proofs is wrong, the headline result fails for those operators.

What would settle it

For one of the manually verified transformers (e.g., GELU in the mixed case l<0<u), run an independent solver capable of nonlinear real arithmetic, or a randomized search over abstract elements and concretizations, to look for an abstract element whose concrete output falls outside the claimed bounds; any such violation would disprove global soundness. Conversely, a machine-checked proof for the same transformers would settle the claim positively.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

  • If cost-guided refinement converges as claimed, building a new verifier component reduces to prompting an LLM and supplying operator and domain descriptions, removing the need for hand-derived transformers.
  • Networks using activations that previously had no sound transformer—HardSigmoid, GELU, ELU, Sigmoid—can now be certified with DeepPoly-style bounds, as long as the manual certificates for the nonlinear cases hold.
  • The convergence bound (at most ⌈L(F#_0)/λ⌉ refinement steps) gives a predictable budget for synthesis, though it depends on the LLM actually proposing λ-improving refinements.
  • The same optimization recipe can be applied in other abstract domains (the paper demonstrates DeepZ and Interval too), suggesting a general route to automating abstract interpretation.
  • Precision results matching handcrafted transformers indicate no precision loss from automation in the operators that have existing transformers.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The manual soundness check for GELU, ELU, and Sigmoid is a gap between the paper's headline and its automation claim: until a solver that handles transcendental functions is integrated, those certificates depend on human proof rather than the pipeline. A testable extension is to plug in a solver supporting nonlinear real arithmetic and replay the same candidate search to obtain machine-checked cer
  • The cost function is essentially a quantitative refinement metric; the same idea could drive synthesis of sound invariants or program analyzers beyond neural networks, where soundness is also a universal condition over an infinite state space.
  • Since stronger LLMs needed less feedback, the framework's practical guarantee currently inherits the model's ceiling; pairing this cost-guided loop with a search over both candidates and cost-margin thresholds might make weaker models converge more reliably.
  • The returned best-unsound fallback when no sound candidate is found leaves the verifier user with an explicit warning; a natural product-level extension is to output the residual cost so the user can judge how dangerously unsound the fallback is.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper presents SAIL, an LLM-driven framework for synthesizing abstract transformers for neural-network verification, expressed in the ConstraintFlow DSL. The synthesis task is formalized as a constrained optimization problem with a soundness-deviation cost L(F#); candidates are statically validated, repaired by a second LLM, checked with the ProveSound/Z3 verifier, and refined through counterexample-guided feedback. The evaluation covers several activations and abstract domains, and the paper claims both to match handcrafted transformers where they exist and to synthesize new globally sound transformers for HardSigmoid, GELU, ELU, and Sigmoid. It also claims a finite-step convergence guarantee for the refinement process.

Significance. If fully substantiated, the contribution would be significant: it would automate a tedious expert task, produce new DeepPoly transformers for operators lacking them, and demonstrate that LLM search coupled with external verification can generate non-trivial sound code. The piecewise-linear results are supported by an external SMT-based verifier, which is a genuine strength of the work. However, the paper's headline nonlinear results rest on omitted manual proofs, and the convergence theorem is conditional on an assumption not established for the implemented system. As it stands, the strongest claims outrun the evidence; the value of the framework will be realized only if the missing certificates and proofs are supplied.

major comments (3)
  1. [§5 Experimental Setup; Figs. 8–9, 11; Abstract and §1] The paper's central claim—globally sound DeepPoly transformers for GELU, ELU, and Sigmoid—is not supported by the included artifact. §5 states that ConstraintFlow cannot verify these functions with Z3 and that soundness was 'manually verified', but no manual proof, proof script, or final DSL code is provided. The proof obligations are nontrivial: Fig. 8c asserts a secant line is a global upper bound for GELU on [l,u] and y=0.5x is a global lower bound; similar claims appear for ELU (Fig. 9c) and Sigmoid (Fig. 11c). Because ProveSound cannot handle these operators, the headline novelty rests on an omitted human case analysis. Without machine-checkable certificates or complete proofs, the claim that SAIL synthesizes globally sound transformers for these operators is not established.
  2. [§4.4 Theorem 4.1; Algorithm 1] Theorem 4.1 is conditional, not a convergence guarantee for the implemented system. It assumes every refinement R satisfies L(R(F#)) < L(F#) − λ, but Algorithm 1 only updates the best candidate when the stochastic LLM happens to produce such a refinement; existence is not ensured. If the retry budget is exhausted, Algorithm 1 returns the best unsound fallback. The claim in §1 (Challenge 3) that the process 'guarantees convergence to a globally sound transformer' is therefore not established. The theorem should be stated as conditional, and the implemented system described as best-effort search with fallback.
  3. [§4.3 and §4.5, Eq. (6)] The practical cost function is a finite-sample relaxation. The ideal Δ_S is defined over infinite sets A* and γ(z), and §4.3 claims L=0 iff F# is sound. The implementation in §4.5 replaces this with maximization over a finite sample (Eq. (6)), so cost zero can occur for an unsound candidate. This is acceptable for piecewise-linear operators only because ProveSound supplies an independent global check. For GELU, ELU, and Sigmoid, where that check is absent, the sampled cost cannot certify global soundness. This limitation should be stated explicitly.
minor comments (5)
  1. [§4.3; Fig. 6] Unresolved editorial notes remain in the manuscript, e.g., '[Note: use another letter instead of S, refer to fig 5]', '[Note: don’t use phi]', and 'Fig. 6. [Note: remove precision, bkg]'. These should be removed.
  2. [Title/Abstract] The arXiv title is 'SAIL: Sound Abstract Interpreters with LLMs', but the body title is 'Cost-Driven Synthesis of Sound Abstract Interpreters', and the acronym SAIL is never defined or used in the body.
  3. [§4.4] The proof of Theorem 4.1 refers to 'requirement (R3)' but only R1 and R2 are listed; the improvement rule is Eq. (5), not R3.
  4. [Tables 1–3] The 'Handcrafted' column uses '✗' without a legend. Define it in each caption.
  5. [§1; Appendix A] Typos: 'seperate' in §1 and 'funstions' in the Appendix A prompt.

Circularity Check

1 steps flagged

Convergence guarantee is enforced by the algorithm's own acceptance test; GELU/ELU/Sigmoid soundness is manually asserted rather than certified.

specific steps
  1. self definitional [§4.4 Theorem 4.1; Algorithm 1, line 18]
    "Theorem 4.1. Assume each refinement step R satisfies the rule L(R(F♯)) < L(F♯) − λ ... the refinement process reaches L(F♯_T)=0 in at most T ≤ ⌈L(F♯_0)/λ⌉ successful refinement steps. [Algorithm 1:] if score < best_score − λ then best_score ← score; best_code ← d"

    The theorem's key hypothesis is exactly the algorithm's update condition: Algorithm 1 only records a new best when score < best_score − λ. Thus the monotone decrease and the finite bound ⌈L(F♯_0)/λ⌉ are properties of the acceptance predicate, not discovered properties of the LLM search. The substantive question—whether the stochastic generator can produce candidates satisfying the inequality—is assumed, never proved. The claimed 'theoretical convergence to a globally sound transformer' therefore reduces to the definition of a 'successful refinement' and cannot support the stated guarantee.

full rationale

Most of the pipeline is not circular: for piecewise-linear operators such as HardSigmoid, HardTanh, and ReLU6, soundness is checked by the external SMT-based ProveSound tool, and the cost function is a reformulation of the soundness condition rather than a fitted quantity. The self-citations to ConstraintFlow, ProveSound, and the compiler backend are tool reuse, not a load-bearing self-citation chain. The principal circular aspect is Theorem 4.1: Algorithm 1 implements the theorem's progress assumption as its acceptance test, so the 'guarantee' that cost reaches zero in finitely many steps is a tautology of the selection rule. Separately, §5 contains a support gap—not itself circularity—when it states: 'Since ConstraintFlow cannot directly verify nonlinear activation functions Gelu, Elu, and Sigmoid due to relying on Z3 as the underlying SMT solver, we manually verify the soundness and provide counterexamples for these.' No manual proof is supplied, so the headline claim of globally sound novel transformers for these functions rests on unshown human case analysis. I also note the Appendix A prompt includes HardSigmoid-specific helper functions (slope, f1, f2), which weakens the 'from scratch' narrative but is answer leakage rather than a formal circular derivation. Overall, the central empirical soundness evidence for SMT-verifiable operators is independent, but the convergence contribution is circular by construction, giving a partial circularity score of 6.

Axiom & Free-Parameter Ledger

6 free parameters · 6 axioms · 0 invented entities

The paper's real contribution is the synthesis loop, not new mathematical objects. The free parameters are the manually chosen cost machinery (λ, weights, sampling, aggregation) and the prompt-specific helper functions that seed the search. The axioms show the two load-bearing assumptions: the existence of an LLM refinement that decreases the cost, and the correctness of manual nonlinear soundness proofs. No new physical or mathematical entity is invented.

free parameters (6)
  • Minimum progress threshold λ = 0.0001
    Used in Eq. 5 and Theorem 4.1 for termination; chosen by implementation, not derived.
  • Weight function φ(f, x_i) = softplus(||∇f||)
    Hand-designed to emphasize points near nonlinear boundaries; normalized weights affect cost; alternative choices change refinement.
  • Sampling set γ_sample(z)
    Cost estimates violations only on sampled concretizations; size and distribution not specified, so global cost guarantee is approximate.
  • Retry budgets R and repair trials
    Algorithm 1 uses a maximum retries R; no value given; termination/success depends on it.
  • HardSigmoid-specific prompt helpers (slope, intercept)
    Appendix A prompt pre-defines slope and intercept functions for HardSigmoid, injecting operator-specific knowledge into the "from scratch" synthesis.
  • Aggregation operator (max)
    Cost uses max among sampled violations; mean or other operators would produce different guidance.
axioms (6)
  • standard math Soundness of an abstract transformer is ∀z, F(γ(z)) ⊆ γ(F#(z))
    Background definition of abstract interpretation (§2.1, §4.1).
  • domain assumption Operator is single-assignment: only one neuron updated at a time
    Used to simplify cost decomposition in Eq. 4; true for activations but not for general program operators.
  • standard math Fourier–Motzkin elimination can rewrite relational constraints into per-variable constraints
    Invoked in §4.2 for shape-aware deviation; assumes linear real arithmetic/polyhedral structure.
  • ad hoc to paper A refinement operator R satisfying L(R(F#)) < L(F#) − λ exists and is produced by the LLM
    Theorem 4.1 requires this condition; the paper does not prove the stochastic LLM can generate such a candidate, so convergence is conditional.
  • ad hoc to paper Manual soundness proofs for GELU/ELU/Sigmoid are correct and global
    §5 says Z3 cannot verify nonlinear activations, so soundness is manually verified; no proof script or formal artifact is provided.
  • domain assumption Cost values are finite and non-negative
    R1/R2 in §4.4; finite-sample approximation may violate the exact bound if sampled values are unbounded.

pith-pipeline@v1.3.0-alltime-deepseek · 33700 in / 12675 out tokens · 125419 ms · 2026-08-03T21:43:54.111063+00:00 · methodology

0 comments
read the original 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.

Figures

Figures reproduced from arXiv: 2511.13663 by Avaljot Singh, Gagandeep Singh, Qiuhan Gu.

Figure 1
Figure 1. Figure 1: The overview of our framework. Given a prompt [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Definition and visualization of the HardSigmoid activation. HardSigmoid linearly approximates the [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Correct polyhedra bounds for HardSigmoid [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figure 5
Figure 5. Figure 5: Search trajectory of abstract transformers from an unsound starting point into the Fig5Search trajectory of abstract transform itional generation [PITH_FULL_IMAGE:figures/full_fig_p013_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Synthesis performance of different LLMs on HardSigmoid operators in the DeepPoly domain. [PITH_FULL_IMAGE:figures/full_fig_p017_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Performance of GPT-5 generating DeepPoly [PITH_FULL_IMAGE:figures/full_fig_p017_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: DeepPoly Transformer for GeLU. The transformer considers three cases: (a) for 𝑙 < 𝑢 < 0, lower bound and upper bound are 𝑦 = 0.5𝑥 and 𝑦 = 0 respectively; (b) for 0 < 𝑙 < 𝑢, lower bound and upper bound are 𝑦 = 0.5𝑥 and 𝑦 = 𝑥 respectively; (c) for the mixed case (𝑙 < 0 < 𝑢), the upper bound is the secant line connecting (𝑙, GeLU(𝑙)) and (𝑢, GeLU(𝑢)), while the lower bound remains 𝑦 = 0.5𝑥. Since GeLU(𝑥) is m… view at source ↗
Figure 9
Figure 9. Figure 9: DeepPoly Transformer for ELU. The transformer is divided into three cases: (1) for 𝑙 < 𝑢 < 0, the lower and upper bounds are 𝑦 = −1 and the secant line connecting (𝑙, ELU(𝑙)) and (𝑢, ELU(𝑢)), respectively; (2) for 0 < 𝑙 < 𝑢, the lower and upper bounds are 𝑦 = 𝑥 and the same secant line; (3) for the mixed case (𝑙 < 0 < 𝑢), the upper bound is again the secant through (𝑙, ELU(𝑙)) and (𝑢, ELU(𝑢)), while the lo… view at source ↗
Figure 10
Figure 10. Figure 10: Examples of transformer candidates generated by our framework. ( [PITH_FULL_IMAGE:figures/full_fig_p030_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: visualizes the generated transformer for sigmoid activation. x 0.0 0.2 0.4 0.6 0.8 1.0 y u 0 Sigmoid(x) Lower Upper (a) 𝑙 < 𝑢 < 0. x 0.0 0.2 0.4 0.6 0.8 1.0 y 0 u Sigmoid(x) Lower Upper (b) 0 < 𝑙 < 𝑢. x 0.0 0.2 0.4 0.6 0.8 1.0 y 0 u Sigmoid(x) Lower Upper (c) 𝑙 < 0 < 𝑢 [PITH_FULL_IMAGE:figures/full_fig_p034_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: With cost-function guidance. The model converges to sound transformers within a few refinement [PITH_FULL_IMAGE:figures/full_fig_p034_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: Without cost-function guidance but with repair module. The model is able to produce syntactically [PITH_FULL_IMAGE:figures/full_fig_p035_13.png] view at source ↗
Figure 14
Figure 14. Figure 14: Without repair module and cost-function guidance. The model often produces syntactically invalid [PITH_FULL_IMAGE:figures/full_fig_p035_14.png] view at source ↗
Figure 15
Figure 15. Figure 15: Quantitative results of GPT-5 generating transformers under the DeepPoly domain. [PITH_FULL_IMAGE:figures/full_fig_p035_15.png] view at source ↗
Figure 16
Figure 16. Figure 16: Quantitative results of Llama4-Maverick generating transformers under the DeepPoly domain. [PITH_FULL_IMAGE:figures/full_fig_p036_16.png] view at source ↗
Figure 17
Figure 17. Figure 17: Quantitative results of Claude-Opus–4 generating transformers under the DeepPoly domain. [PITH_FULL_IMAGE:figures/full_fig_p036_17.png] view at source ↗
Figure 18
Figure 18. Figure 18: Quantitative results of GPT-5 generating transformers under the DeepZ domain. [PITH_FULL_IMAGE:figures/full_fig_p036_18.png] view at source ↗
Figure 19
Figure 19. Figure 19: Quantitative results of Claude-Opus-4 generating transformers under the DeepZ domain. [PITH_FULL_IMAGE:figures/full_fig_p037_19.png] view at source ↗
Figure 20
Figure 20. Figure 20: Quantitative results of GPT5 generating transformers under the Interval domain. [PITH_FULL_IMAGE:figures/full_fig_p037_20.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

69 extracted references · 2 canonical work pages

  1. [1]

    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. In2013 Formal Methods in Computer-Aided Design. 1–8. https://doi.org/10.1109/FMCAD.2013.6679385

    arXiv 2013

  2. [2]

    Rajeev Alur, Arjun Radhakrishna, and Abhishek Udupa. 2017. Scaling enumerative program synthesis via divide and conquer. InInternational conference on tools and algorithms for the construction and analysis of systems. Springer, 319–336

    2017

  3. [3]

    Jacob Austin, Augustus Odena, Maxwell Nye, Maarten Bosma, Henryk Michalewski, David Dohan, Ellen Jiang, Carrie Cai, Michael Terry, Quoc Le, et al. 2021. Program synthesis with large language models.arXiv preprint arXiv:2108.07732(2021)

    Pith/arXiv arXiv 2021

  4. [4]

    2002.Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software

    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. Springer-Verlag, Berlin, Heidelberg, 85–108

    2002

  5. [5]

    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, and Lenore D. Zuck (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 37–51

    2008

  6. [6]

    Johnson, and Haoze Wu

    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. arXiv:2412.19985 [cs.LG] https: //arxiv.org/abs/2412.19985

    Pith/arXiv arXiv 2024

  7. [7]

    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), 33 pages. https://doi.org/10.1145/3704905

    doi:10.1145/3704905 2025

  8. [8]

    Jose Cambronero, Hongyu Li, Seohyun Kim, Koushik Sen, and Satish Chandra. 2019. When Deep Learning Met Code Search. arXiv:1905.03813 [cs.SE] https://arxiv.org/abs/1905.03813

    Pith/arXiv arXiv 2019

  9. [9]

    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), 31 pages. https://doi.org/10.1145/3498721

    doi:10.1145/3498721 2022

  10. [10]

    Abstractinterpretation:aunifiedlatticemodelforstaticanalysisofprogramsby construction or approximation of fixpoints

    PatrickCousotandRadhiaCousot.1977. Abstractinterpretation:aunifiedlatticemodelforstaticanalysisofprogramsby construction or approximation of fixpoints. InProceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages(Los Angeles, California)(POPL ’77). Association for Computing Machinery, New York, NY, USA, 238–252. https://doi...

    arXiv 1977

  11. [11]

    Patrick Cousot and Radhia Cousot. 1979. Systematic design of program analysis frameworks. InProceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages(San Antonio, Texas)(POPL ’79). Association for Computing Machinery, New York, NY, USA, 269–282. https://doi.org/10.1145/567752.567778

    arXiv 1979

  12. [12]

    Patrick Cousot, Radhia Cousot, Jerôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival

  13. [13]

    1973.Fourier-Motzkin elimination and its dual

    George B Dantzig. 1973.Fourier-Motzkin elimination and its dual. Technical Report

    1973

  14. [14]

    DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning

    DeepSeek-AI, Daya Guo, et al.2025. DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning. arXiv:2501.12948 [cs.CL] https://arxiv.org/abs/2501.12948

    Pith/arXiv arXiv 2025

  15. [15]

    Li Deng. 2012. The MNIST Database of Handwritten Digit Images for Machine Learning Research [Best of the Web]. IEEE Signal Processing Magazine6 (2012), 141–142. https://doi.org/10.1109/MSP.2012.2211477

    arXiv 2012

  16. [16]

    Alessandra Di Pierro and Herbert Wiklicky. 2000. Measuring the precision of abstract interpretations. InInternational Workshop on Logic-Based Program Synthesis and Transformation. Springer, 147–164

    2000

  17. [17]

    Pranav Garg, Daniel Neider, Parthasarathy Madhusudan, and Dan Roth. 2016. Learning invariants using decision trees and implication counterexamples.ACM Sigplan Notices1 (2016), 499–512

    2016

  18. [18]

    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. In2018 IEEE Symposium on Security and Privacy (SP). 3–18. https://doi.org/10.1109/SP.2018.00058

    arXiv 2018

  19. [19]

    Roberto Giacobazzi, Francesco Ranzato, and Francesca Scozzari. 2000. Making abstract interpretations complete.J. ACM47, 2 (March 2000), 361–416. https://doi.org/10.1145/333979.333989

    arXiv 2000

  20. [20]

    Shaurya Gomber, Debangshu Banerjee, and Gagandeep Singh. 2025. Universal Synthesis of Differentiably Tunable Numerical Abstract Transformers.arXiv preprint arXiv:2507.11827(2025)

    Pith/arXiv arXiv 2025

  21. [21]

    SvenGowal,KrishnamurthyDvijotham,RobertStanforth,RudyBunel,ChongliQin,JonathanUesato,ReljaArandjelovic, Timothy Mann, and Pushmeet Kohli. 2018. On the effectiveness of interval bound propagation for training verifiably robust models.arXiv preprint arXiv:1810.12715(2018). Cost-Driven Synthesis of Sound Abstract Interpreters 23

    Pith/arXiv arXiv 2018

  22. [22]

    Arya Grayeli, Atharva Sehgal, Omar Costilla-Reyes, Miles Cranmer, and Swarat Chaudhuri. 2024. Symbolic Regression with a Learned Concept Library. arXiv:2409.09359 [cs.LG] https://arxiv.org/abs/2409.09359

    Pith/arXiv arXiv 2024

  23. [23]

    Sumit Gulwani, Oleksandr Polozov, Rishabh Singh, et al. 2017. Program synthesis.Foundations and Trends®in Programming Languages4, 1-2 (2017), 1–119

    2017

  24. [24]

    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. https://doi.org/10.1109/ ICSE.2017.54

    2017

  25. [25]

    Naman Jain, Skanda Vaidyanath, Arun Iyer, Nagarajan Natarajan, Suresh Parthasarathy, Sriram Rajamani, and Rahul Sharma. 2022. Jigsaw: Large language models meet program synthesis. InProceedings of the 44th International Conference on Software Engineering. 1219–1231

    2022

  26. [26]

    Julien Julien Bertrane, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, and Xavier Rival. 2011. Static analysis by abstract interpretation of embedded critical software.SIGSOFT Softw. Eng. Notes1 (Jan. 2011), 1–8. https://doi.org/10.1145/1921532.1921553

    arXiv 2011

  27. [27]

    Synthesizingabstract transformers.Proc.ACMProgram.Lang.OOPSLA2,Article171(Oct.2022),29pages

    PankajKumarKalita,SujitKumarMuduli,LorisD’Antoni,ThomasReps,andSubhajitRoy.2022. Synthesizingabstract transformers.Proc.ACMProgram.Lang.OOPSLA2,Article171(Oct.2022),29pages. https://doi.org/10.1145/3563334

    doi:10.1145/3563334 2022

  28. [28]

    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)

    2025

  29. [29]

    2009.The CIFAR-10 and CIFAR-100 datasets

    Alex Krizhevsky and Geoffrey Hinton. 2009.The CIFAR-10 and CIFAR-100 datasets. https://www.cs.toronto.edu/ ~kriz/cifar.html Accessed: 2025-11-07

    2009

  30. [30]

    Joel Lehman, Jonathan Gordon, Shawn Jain, Kamal Ndousse, Cathy Yeh, and Kenneth O. Stanley. 2022. Evolution through Large Models. arXiv:2206.08896 [cs.NE] https://arxiv.org/abs/2206.08896

    Pith/arXiv arXiv 2022

  31. [31]

    Maikel Leon. 2025. GPT-5 and open-weight large language models: Advances in reasoning, transparency, and control. Information Systems(2025), 102620

    2025

  32. [32]

    Yujia Li, David Choi, Junyoung Chung, Nate Kushman, Julian Schrittwieser, Rémi Leblond, Tom Eccles, James Keeling, Felix Gimeno, Agustin Dal Lago, et al. 2022. Competition-level code generation with alphacode.Science378, 6624 (2022), 1092–1097

    2022

  33. [33]

    Sirui Lu and Rastislav Bodík. 2023. Grisette: Symbolic Compilation as a Functional Programming Library.Proc. ACM Program. Lang.7, POPL, Article 16 (Jan. 2023), 33 pages. https://doi.org/10.1145/3571209

    doi:10.1145/3571209 2023

  34. [34]

    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. arXiv:2303.17651 [cs.CL] https://arxiv.or...

    Pith/arXiv arXiv 2023

  35. [35]

    Antoine Miné. 2006. Symbolic methods to enhance the precision of numerical abstract domains. InInternational Workshop on Verification, Model Checking, and Abstract Interpretation. Springer, 348–363

    2006

  36. [36]

    Antoine Miné. 2017. Static Analysis of Embedded Real-Time Concurrent Software with Dynamic Priorities.Electronic Notes in Theoretical Computer Science331 (2017), 3–39. https://doi.org/10.1016/j.entcs.2017.02.002 Proceedings of the Sixth Workshop on Numerical and Symbolic Abstract Domains (NSAD 2016)

    work page doi:10.1016/j.entcs.2017.02.002 2017

  37. [37]

    Matthew Mirman, Timon Gehr, and Martin T. Vechev. 2018. Differentiable Abstract Interpretation for Provably Robust NeuralNetworks.InInternationalConferenceonMachineLearning. https://api.semanticscholar.org/CorpusID:51872670

    2018

  38. [38]

    Codegen: An open large language model for code with multi-turn program synthesis.arXiv preprint arXiv:2203.13474 (2022)

    ErikNijkamp,BoPang,HiroakiHayashi,LifuTu,HuanWang,YingboZhou,SilvioSavarese,andCaimingXiong.2022. Codegen: An open large language model for code with multi-turn program synthesis.arXiv preprint arXiv:2203.13474 (2022)

    Pith/arXiv arXiv 2022

  39. [39]

    Alexander Novikov, Ngân V˜u, Marvin Eisenberger, Emilien Dupont, Po-Sen Huang, Adam Zsolt Wagner, Sergey Shirobokov, Borislav Kozlovskii, Francisco J. R. Ruiz, Abbas Mehrabian, M. Pawan Kumar, Abigail See, Swarat Chaudhuri, George Holland, Alex Davies, Sebastian Nowozin, Pushmeet Kohli, and Matej Balog. 2025. AlphaEvolve: A coding agent for scientific and...

    Pith/arXiv arXiv 2025

  40. [41]

    Brandon Paulsen and Chao Wang. 2022. LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions. arXiv:2201.13351 [cs.LG] https://arxiv.org/abs/2201.13351

    Pith/arXiv arXiv 2022

  41. [42]

    Stanislas Polu and Ilya Sutskever. 2020. Generative Language Modeling for Automated Theorem Proving. arXiv:2009.03393 [cs.LG] https://arxiv.org/abs/2009.03393

    Pith/arXiv arXiv 2020

  42. [43]

    Thomas Reps and Aditya Thakur. 2016. Automating Abstract Interpretation. InProceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 9583(St. Petersburg, FL, USA) (VMCAI 2016). Springer-Verlag, Berlin, Heidelberg, 3–40. https://doi.org/10.1007/978-3-662-49122-5_1 24 Qiuhan Gu, Avaljot Singh, and...

    doi:10.1007/978-3-662-49122-5_1 2016

  43. [44]

    Pawan Kumar, Emilien Dupont, Francisco J

    Bernardino Romera-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M. Pawan Kumar, Emilien Dupont, Francisco J. R. Ruiz, Jordan S. Ellenberg, Pengming Wang, Omar Fawzi, Pushmeet Kohli, and Alhussein Fawzi

  44. [45]

    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. arXiv:2404.18400 [cs.LG] https://arxiv.org/abs/2404.18400

    Pith/arXiv arXiv 2025

  45. [46]

    Avaljot Singh, Yasmin Sarita, Charith Mendis, and Gagandeep Singh. 2024. ConstraintFlow: A Declarative DSL for Easy Development of DNN Certifiers. Springer-Verlag, Berlin, Heidelberg, 407–424. https://doi.org/10.1007/978-3- 031-74776-2_16

    doi:10.1007/978-3- 2024

  46. [47]

    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), 29 pages. https://doi.org/10.1145/3720509

    work page doi:10.1145/3720509 2025

  47. [48]

    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. arXiv:2507.20055 [cs.CL] https://arxiv.org/abs/2507.20055

    Pith/arXiv arXiv 2025

  48. [49]

    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

    2025

  49. [50]

    Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin Vechev. 2018. Fast and effective robustness certification. InProceedings of the 32nd International Conference on Neural Information Processing Systems (Montréal, Canada)(NIPS’18). Curran Associates Inc., Red Hook, NY, USA, 10825–10836

    2018

  50. [51]

    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), 30 pages. https://doi.org/10.1145/3290354

    doi:10.1145/3290354 2019

  51. [52]

    Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin T. Vechev. 2018. Boosting Robustness Certification of Neural Networks. InInternational Conference on Learning Representations. https://api.semanticscholar.org/CorpusID: 196059499

    2018

  52. [53]

    Gagandeep Singh, Jacob Laurel, Sasa Misailovic, Debangshu Banerjee, Avaljot Singh, Changming Xu, Shubham Ugare, and Huan Zhang. 2025. Safety and Trust in Artificial Intelligence with Abstract Interpretation.Found. Trends Program. Lang.3–4 (June 2025), 250–408. https://doi.org/10.1561/2500000062

    doi:10.1561/2500000062 2025

  53. [54]

    Gagandeep Singh, Markus Püschel, and Martin Vechev. 2017. Fast polyhedra abstract domain. InProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. 46–59

    2017

  54. [55]

    Armando Solar-Lezama. 2009. The sketching approach to program synthesis. InAsian symposium on programming languages and systems. Springer, 4–13

    2009

  55. [56]

    Armando Solar-Lezama. 2013. Program sketching.Int. J. Softw. Tools Technol. Transf.5–6 (Oct. 2013), 475–495. https://doi.org/10.1007/s10009-012-0249-7

    doi:10.1007/s10009-012-0249-7 2013

  56. [57]

    Benno Stein, Bor-Yuh Evan Chang, and Manu Sridharan. 2021. Demanded abstract interpretation. InProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (Virtual, Canada)(PLDI 2021). Association for Computing Machinery, New York, NY, USA, 282–295. https: //doi.org/10.1145/3453483.3454044

    arXiv 2021

  57. [58]

    Gemini Team, Rohan Anil, et al . 2025. Gemini: A Family of Highly Capable Multimodal Models. arXiv:2312.11805 [cs.CL] https://arxiv.org/abs/2312.11805

    Pith/arXiv arXiv 2025

  58. [59]

    Yu, and Guandong Xu

    Wenhua Wang, Yuqun Zhang, Yulei Sui, Yao Wan, Zhou Zhao, Jian Wu, Philip S. Yu, and Guandong Xu. 2022. Reinforcement-Learning-Guided Source Code Summarization Using Hierarchical Attention.IEEE Transactions on Software Engineering48, 1 (2022), 102–119. https://doi.org/10.1109/TSE.2020.2979701

    arXiv 2022

  59. [60]

    Yixuan Wang, Chao Huang, Zhaoran Wang, Zhilu Wang, and Qi Zhu. 2021. Verification in the Loop: Correct-by- Construction Control Learning with Reach-avoid Guarantees. arXiv:2106.03245 [eess.SY] https://arxiv.org/abs/2106. 03245

    Pith/arXiv arXiv 2021

  60. [61]

    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. InProceedings of the 1st ACM SIGPLAN International Workshop on Language Models and Programming Languages(Singapore, Singapore)(LMPL ’25). Association for Computing Machinery, New York, NY, U...

    arXiv 2025

  61. [62]

    Ziwei Xu, Sanjay Jain, and Mohan Kankanhalli. 2025. Hallucination is Inevitable: An Innate Limitation of Large Language Models. arXiv:2401.11817 [cs.CL] https://arxiv.org/abs/2401.11817

    Pith/arXiv arXiv 2025

  62. [63]

    Shunyu Yao, Jeffrey Zhao, Dian Yu, Nan Du, Izhak Shafran, Karthik Narasimhan, and Yuan Cao. 2023. ReAct: Synergizing Reasoning and Acting in Language Models. arXiv:2210.03629 [cs.CL] https://arxiv.org/abs/2210.03629

    Pith/arXiv arXiv 2023

  63. [64]

    Huan Zhang, Hongge Chen, Chaowei Xiao, Sven Gowal, Robert Stanforth, Bo Li, Duane Boning, and Cho-Jui Hsieh

  64. [69]

    Unsound transformer

    / 6, 13(prev+ 3) / 6) 14: (0, 1, (prev+ 3) / (prev[u] + 3), (prev-prev[l]) / (3 -prev[l]))))); 15} Listing 2. Unsound transformer. Counterexample: Prev = 3/2, Prev_l = -4, Prev_u = 2, Prev_L = 3/2, Prev_U = 3/2, Curr = 3/4. Based on the transformer, we get Curr_l = 0, Curr_u = 5/6, Curr_L = 3/4, Curr_U = -5/18, which is a wrong approximation. 1transformer...

  65. [161]

    Invalid transformer (Syntax error

    : Cost-Driven Synthesis of Sound Abstract Interpreters 29 17((prev[u]) <= ((1 - attr[beta]) / attr[alpha])) ? 18(0, 19(attr[alpha] *prev[u] + attr[beta]), 200, 21(attr[alpha] *prev- (attr[alpha] *prev[l]))) : 22(0, 1, 0, 1); 23} Listing 1. Invalid transformer (Syntax error. Undefined variable: attr, alpha, beta) 1transformerdeeppoly { 2HardSigmoid -> (pre...

  66. [181]

    Sound transformer Fig

    : 19(prev[u] <= 3) ? 20(0, 21(prev[u] / 6) + 0.5, 220, 30 Qiuhan Gu, Avaljot Singh, and Gagandeep Singh 23(((((prev[u] / 6) + 0.5) / (prev[u] -prev[l])) *prev) 24- ((((prev[u] / 6) + 0.5) / (prev[u] -prev[l])) *prev[l]))) : 25(0, 1, 0, 1); 26} Listing 3. Sound transformer Fig. 10. Examples of transformer candidates generated by our framework. (1) contains...

    2062

  67. [2005]

    https://doi.org/10.1007/978-3-540-31987-0_3

    TheASTREÉanalyzer.InProceedingsofthe14thEuropeanConferenceonProgrammingLanguagesandSystems (Edinburgh,UK)(ESOP’05).Springer-Verlag,Berlin,Heidelberg,21–30. https://doi.org/10.1007/978-3-540-31987-0_3

    doi:10.1007/978-3-540-31987-0_3

  68. [2019]

    "" ### Example: Affine operator Input: Generate the transformer for ‘affine‘ operator Output:

    Towards Stable and Efficient Training of Verifiably Robust Neural Networks. arXiv:1906.06316 [cs.LG] Cost-Driven Synthesis of Sound Abstract Interpreters 25 https://arxiv.org/abs/1906.06316 26 Qiuhan Gu, Avaljot Singh, and Gagandeep Singh A Prompt Templates In this section, we show the prompt used for transformer generation and transformer repair in our f...

    Pith/arXiv arXiv 1906

  69. [2024]

    https://doi.org/10.1038/s41586-023-06924-6

    Mathematical discoveries from program search with large language models.Nat.7995 (January 2024), 468–475. https://doi.org/10.1038/s41586-023-06924-6

    doi:10.1038/s41586-023-06924-6 2024