Avaljot Singh
PhD candidate at the University of Illinois Urbana-Champaign, working at the intersection of formal methods and artificial intelligence.
I am a PhD student at the University of Illinois Urbana-Champaign, under the guidance of Prof. Gagandeep Singh and Prof. Charith Mendis. Prior to starting my PhD, I graduated with Bachelors and Masters in Computer Science from IIT Delhi in May 2021, where I was advised by Prof. Sanjiva Prasad (Thesis). I have also had the opportunity of working with Shraddha Barke and Suman Nath at MSR Redmond, Rahul Sharma at MSR India and Prof. Nate Foster at Cornell University during my research internships.
My research is centered on a bidirectional interaction between formal methods and artificial intelligence. On one hand, I develop formal and declarative infrastructures for building trustworthy AI systems using formal methods, with a particular focus on specification, soundness verification, and efficient execution of AI analyses and certification procedures. On the other hand, I study how learning and synthesis techniques can be used to automate and improve formal methods themselves, enabling the automatic construction of verification tools, program analyses, and reasoning procedures. Together, these two directions aim to improve the trustworthiness of AI systems and to substantially reduce the human effort required to build and maintain formal verification frameworks.
News
| Aug 20, 2026 | AgentRx — Diagnosing AI Agent Failures from Execution Trajectories — is accepted at EMNLP 2026, from my internship at MSR Redmond. [paper] |
|---|---|
| Jul 10, 2026 | RuleFlow — Learning Reusable Program Transformations via LLM-Guided Rule Synthesis — is accepted at COLM 2026. [paper] [code] |
| Mar 5, 2026 | SAIL — Sound Abstract Interpreters with LLMs — is accepted at PLDI 2026. [paper] [code] |
| Jan 20, 2026 | Maestro — Unified Operational Formalism for LLM-based Theorem-proving Systems — is accepted at the VerifAI workshop at ICLR 2026. [paper] |
| Jan 15, 2026 | Syndicate — Efficient Ranking Function-Based Termination Analysis via Bidirectional Decompositional Search — is accepted at ESOP 2026. [paper] |
Formal Methods for AI
This line of work focuses on building principled and trustworthy AI analysis and certification systems using formal methods. My goal is to make AI analyses and certifiers easier to design, mechanically verifiable for soundness, and efficient to execute, by providing a unified infrastructure that supports specification, formal verification, and compilation of analysis and certification procedures.
ConstraintFlow
ConstraintFlow is a declarative domain-specific language for specifying neural network certifiers and analyses. It provides a compact and modular way to express abstract interpretation-based certifiers, significantly reducing implementation complexity compared to hand-written implementations.
ProveSound
ProveSound automatically verifies the soundness of neural network certifiers written in ConstraintFlow. It checks that a certifier implementation correctly over-approximates the concrete neural network semantics, providing formal guarantees about the correctness of certification algorithms.
Neuton
Neuton is a compiler and execution framework for ConstraintFlow specifications. It translates high-level declarative certifier specifications into efficient executable implementations, bridging the gap between formally specified analyses and practical large-scale neural network verification.
PromptFlow
PromptFlow develops principled methods for KV cache eviction and memory management, tailored to the long-horizon, multi-step execution patterns of LLM-based agentic workflows.
AI for Formal Methods
This line of work focuses on using machine learning and program synthesis techniques to automate and scale formal methods. My goal is to use AI to generate, improve, and adapt formal analysis tools, optimizations, and reasoning procedures, reducing the manual effort required to design, implement, and maintain verification and analysis systems.
Maestro
This project studies the use of AI and large language models to assist and automate theorem proving. The goal is to support formal reasoning by guiding proof search, generating intermediate lemmas, and helping interact with modern theorem provers.