Publications

2026

1. Preprint

   Lumos: Let there be Language Model System Certification

   Isha Chaudhary, Vedaant Jain, Avaljot Singh, Kavya Sachdeva, Sayan Ranu, and Gagandeep Singh

   arXiv preprint, 2026

   Under review

   arXiv
2. Preprint

   A Tensor-Based Compiler and a Runtime for Neuron-Level DNN Certifier Specifications

   Avaljot Singh, Yasmin Sarita, Aditya Mishra, Ishaan Goyal, Gagandeep Singh, and Charith Mendis

   arXiv preprint, 2026

   Neuton. Under review

   arXiv
3. Under Review

   Scaling Deterministic LLM Verification to Prompt Spaces

   Nalin Wadhwa, Brian Kim, David Shu Cheng, Isha Chaudhary, Avaljot Singh, and Gagandeep Singh

   2026

   Under review
4. EMNLP

   AgentRx: Diagnosing AI Agent Failures from Execution Trajectories

   Shraddha Barke, Arnav Goyal, Alind Khare, Avaljot Singh, Suman Nath, and Chetan Bansal

   In Conference on Empirical Methods in Natural Language Processing (EMNLP), 2026

   arXiv
5. COLM

   Learning Reusable Program Transformations via LLM-Guided Rule Synthesis

   Avaljot Singh, Dushyant Bharadwaj, Stefanos Baziotis, Kaushik Varadharajan, and Charith Mendis

   In Conference on Language Modeling (COLM), 2026

   RuleFlow. * Equal contribution by Avaljot Singh and Dushyant Bharadwaj

   arXiv Code
6. PLDI

   SAIL: Sound Abstract Interpreters with LLMs

   Qiuhan Gu, Avaljot Singh, and Gagandeep Singh

   In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2026

   arXiv Code
7. ESOP

   Efficient Ranking Function-Based Termination Analysis via Bidirectional Decompositional Search

   Yasmin Sarita, Avaljot Singh, Shaurya Gomber, Gagandeep Singh, and Mahesh Viswanathan

   In European Symposium on Programming (ESOP), 2026

   Syndicate

   arXiv HTML
8. ICLR-W

   Unified Operational Formalism for LLM-based Theorem-proving Systems

   Avaljot Singh, Shaurya Gomber, Yasmin Sarita, Jose Meseguer, and Gagandeep Singh

   In VerifAI Workshop at the International Conference on Learning Representations (ICLR), 2026

   Maestro. * Equal contribution by Avaljot Singh and Shaurya Gomber

   HTML PDF
9. IJCNN

   Adaptive Quantization of CNNs for Spectrogram-Based Foreground Activity Classification

   Ashitabh Misra, Madhav Agrawal, Tomoyoshi Kimura, Jinyang Li, Avaljot Singh, Arham Jain, and Tarek Abdelzaher

   In International Joint Conference on Neural Networks (IJCNN), 2026

2025

1. OOPSLA

   Automated Verification of Soundness of DNN Certifiers

   Avaljot Singh, Yasmin Sarita, Charith Mendis, and Gagandeep Singh

   Proceedings of the ACM on Programming Languages (OOPSLA), 2025

   ProveSound

   arXiv HTML Code
2. FnTPL

   Safety and Trust in Artificial Intelligence with Abstract Interpretation

   Gagandeep Singh, Jacob Laurel, Sasa Misailovic, Debangshu Banerjee, Avaljot Singh, Changming Xu, Shubham Ugare, and Huan Zhang

   Foundations and Trends in Programming Languages, 2025

   HTML

2024

1. SAS

   ConstraintFlow: A DSL for Specification and Verification of Neural Network Analyses

   Avaljot Singh, Yasmin Sarita, Charith Mendis, and Gagandeep Singh

   In International Static Analysis Symposium (SAS), 2024

   ConstraintFlow. Bronze Medal, ACM SRC at PLDI 2024

   arXiv HTML Code Poster
2. ICLR

   Interpreting Robustness Proofs of Deep Neural Networks

   Debangshu Banerjee, Avaljot Singh, and Gagandeep Singh

   In International Conference on Learning Representations (ICLR), 2024

   ProFIt. Outstanding Paper Award, WFVML at ICML 2023

   Abs HTML PDF

   In recent years numerous methods have been developed to formally verify the robustness of deep neural networks (DNNs). Though the proposed techniques are effective in providing mathematical guarantees about the DNNs’ behavior, it is not clear whether the proofs generated by these methods are human understandable. In this paper, we bridge this gap by developing new concepts, algorithms, and representations to generate human understandable insights into the internal workings of DNN robustness proofs. Leveraging the proposed method, we show that the robustness proofs of standard DNNs rely more on spurious input features as compared to the proofs of DNNs trained to be robust. Robustness proofs of the provably robust DNNs filter out a larger number of spurious input features as compared to adversarially trained DNNs, sometimes even leading to the pruning of semantically meaningful input features. The proofs for the DNNs combining adversarial and provably robust training tend to achieve the middle ground.