8 papers
SAIL: Sound Abstract Interpreters with LLMs
Qiuhan Gu, Avaljot Singh, Gagandeep Singh
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…
Lumos: Let there be Language Model System Certification
Isha Chaudhary, Vedaant Jain, Prineet Parhar +4
We introduce the first principled framework, Lumos, for specifying and formally certifying Language Model System (LMS) behaviors. Lumos is an imperative probabilistic programming D…
RuleFlow : Generating Reusable Program Optimizations with LLMs
Avaljot Singh, Dushyant Bharadwaj, Stefanos Baziotis +2
Optimizing Pandas programs is a challenging problem. Existing systems and compiler-based approaches offer reliability but are either heavyweight or support only a limited set of op…
AgentRx: Diagnosing AI Agent Failures from Execution Trajectories
Shraddha Barke, Arnav Goyal, Alind Khare +3
AI agents often fail in ways that are difficult to localize because executions are probabilistic, long-horizon, multi-agent, and mediated by noisy tool outputs. We address this gap…
A Tensor-Based Compiler and a Runtime for Neuron-Level DNN Certifier Specifications
Avaljot Singh, Yamin Chandini Sarita, Aditya Mishra +3
The uninterpretability of DNNs has led to the adoption of abstract interpretation-based certification as a practical means to establish trust in real-world systems that rely on DNN…
Efficient Ranking Function-Based Termination Analysis with Bi-Directional Feedback
Yasmin Sarita, Avaljot Singh, Shaurya Gomber +2
Synthesizing ranking functions is a common technique for proving the termination of loops. A ranking function must be bounded and decrease by a specified amount with each iteration…