Conferences
-
Evolving Abstract Transformers for Gradient-Guided, Adaptable Abstract InterpretationPLDI 2026 (to appear)
Current numerical abstract interpretation relies on fixed, hand-crafted, instruction-specific transformers tailored to each domain, giving rise to three significant limitations. First, extensibility is limited because transformers cannot be reused across domains and new transformers need to be designed for each new domain or operator. Second, precise compositional reasoning over instruction sequences is difficult as transformers are defined only at the instruction level. Third, all downstream tasks are forced to use the same fixed transformer, irrespective of their precision, efficiency, or task-specific requirements. To address these limitations, we propose the Evolving Abstract Transformer, a general transformer that replaces the fixed single-output design of traditional transformers with an adaptable search over a parametric space of sound outputs. This is achieved through two underlying algorithms we develop. First, the Universal Parametric Output Space Encoder (UPOSE) constructs a compact parametric space of sound outputs for any polyhedral numerical domain and any operator in the Quadratic-Bounded Guarded Operators (QGO) class which includes both individual instructions and structured sequences. Next, the Adaptive Gradient Guidance (AGG) algorithm leverages the differentiable structure of the space generated by UPOSE and uses gradient-based updates to efficiently search it according to downstream analysis objectives and available runtime, continually evolving the output as more time is provided. We implement these ideas in the AbsEvolve framework and evaluate their effectiveness across three numerical abstract domains: Zones, Octagons, and Polyhedra. Our results demonstrate that the evolving transformer works across domains and handles diverse instructions and sequences, allowing efficient adaptability in the precision–efficiency tradeoff by adjusting the number of gradient steps in the search, while also reaching the most precise invariants up to 3.2× faster than existing baselines.
@misc{ustad_arxiv, title={Universal Synthesis of Differentiably Tunable Numerical Abstract Transformers}, author={Shaurya Gomber and Debangshu Banerjee and Gagandeep Singh}, year={2025}, eprint={2507.11827}, archivePrefix={arXiv}, primaryClass={cs.PL}, note={\url{https://arxiv.org/abs/2507.11827}}, } -
Efficient Ranking Function-Based Termination Analysis via Bidirectional Decompositional SearchESOP 2026 (to appear)
Synthesizing ranking functions is a common technique for proving the termination of loops in programs. A ranking function must be bounded and decrease by a specified amount with each iteration for all reachable program states. Since the set of reachable states is unknown, loop invariants are used to overapproximate it, requiring the joint synthesis of ranking functions and invariants to prove the ranking functions valid. Existing approaches either synthesize them independently, encode them into a single monolithic query, or connect them through ad hoc, one-way information flow, leading to inefficient exploration of large search spaces. We present Syndicate, a termination analysis framework based on the novel concept of Bidirectional Decompositional Search (BDS). BDS keeps ranking-function and invariant synthesis decomposed but ensures that they co-evolve through continuous bi-directional feedback. This mutual guidance enables efficient exploration and significantly increases the number of programs proven to terminate while reducing runtime compared to baselines without such feedback. Depending on the templates used, Syndicate is both relatively complete and efficient, outperforming existing techniques that achieve at most one of these guarantees. Despite its simplicity, Syndicate matches or surpasses state-of-the-art tools in termination proofs and runtime, demonstrating the effectiveness of bi-directional reasoning in termination analysis.
@misc{ syndicate_arxiv, title={Efficient Ranking Function-Based Termination Analysis with Bi-Directional Feedback}, author={Yasmin Sarita and Avaljot Singh and Shaurya Gomber and Gagandeep Singh and Mahesh Vishwanathan}, year={2024}, eprint={2404.05951}, archivePrefix={arXiv}, primaryClass={cs.LO}, url={https://arxiv.org/abs/2404.05951}, }
Workshops
-
Unified Operational Formalism for LLM-based Theorem-proving SystemsVerifAI @ ICLR 2026 (to appear)
LLM-based theorem provers differ widely in how they organise interaction between language models and interactive theorem provers, ranging from whole-proof generation to tactic-level and multi-stage pipelines. We propose a unified operational framework that makes this interaction structure explicit by modelling proof search as transitions over a joint formal and informal state and by introducing orchestration as a first-class abstraction that controls how tools such as language models, retrieval components, and provers are scheduled and coordinated. Within this framework, existing systems such as Baldur, COPRA, DSP, POETRY, etc, can be expressed uniformly as different orchestration strategies, enabling principled comparison of interaction patterns, rapid prototyping of new strategies, and backend-agnostic evaluation and reuse across provers, libraries, and models.
-
Neural Abstract Interpretation
Abstract interpretation is a widely used method for the formal analysis and verification of programs and neural networks. However, designing efficient abstract transformers for expressive relational domains such as Octagon and Polyhedra is challenging as one needs to carefully balance the fundamental trade-off between the cost, soundness, and precision of the transformer for downstream tasks. Further, scalable implementations involve intricate performance optimizations like Octagon and Polyhedra decomposition. Given the inherent complexity of abstract transformers and the proven capability of neural networks to effectively approximate complex functions, we envision and propose the concept of Neural Abstract Transformers: neural networks that serve as abstract transformers. The proposed Neural Abstract Interpretation (NAI) framework provides supervised and unsupervised methods to learn efficient neural transformers automatically, which reduces development costs. We instantiate the NAI framework for two widely used numerical domains: Interval and Octagon. Evaluations on these domains demonstrate the effectiveness of the NAI framework to learn sound and precise neural transformers. An added advantage of our technique is that neural transformers are differentiable, unlike hand-crafted alternatives. As an example, we showcase how this differentiability allows framing invariant generation as a learning problem, enabling neural transformers to generate valid octagonal invariants for a program.
@inproceedings{gomber2025neural, title={Neural Abstract Interpretation}, author={Shaurya Gomber and Gagandeep Singh}, booktitle={ICLR 2025 Workshop: VerifAI: AI Verification in the Wild}, year={2025}, url={https://openreview.net/forum?id=WTyyhWhp4m} }
Thesis
-
Neural Abstract Interpretation: Leveraging neural networks for automated, efficient and differentiable abstract interpretation🏆 David J. Kuck Outstanding Master’s Thesis Award 2024
@mastersthesis{ nai_gomber_2024, title={Neural abstract interpretation: Leveraging neural networks for automated, efficient and differentiable abstract interpretation}, author={Gomber, Shaurya}, year={2024}, school={University of Illinois at Urbana-Champaign}, url={https://www.ideals.illinois.edu/items/131524} }