Avaljot Singh

Room 4107

Thomas M Siebel Center

201 Goodwin Avenue

Urbana,

Illinois, 61801

United States

I am a PhD student in the Computer Science Department at University of Illinois, Urbana-Champaign. I am advised by Prof. Gagandeep Singh and Prof. Charith Mendis. My current research is focused on making Neural Networks trustworthy by making it easy to verify properties like robustness using formal methods. We are currently building ConstraintFlow, a DSL for defining Neural Network analysis algorithms.

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 Rahul Sharma at MSR India and Prof. Nate Foster at Cornell University during my research internships.

Resume

Selected Publications

2024

ProveSound

Automated Verification of Soundness of DNN Certifiers

Avaljot Singh, Yasmin Sarita, Charith Mendis, and 1 more author

In submission, 2024
Syndicate

Syndicate: Synergistic Synthesis of Ranking Function and Invariants for Termination Analysis

Yasmin Sarita, Avaljot Singh, Shaurya Gomber, and 2 more authors

Arxiv, 2024
ConstraintFlow

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

Avaljot Singh, Yasmin Sarita, Charith Mendis, and 1 more author

In Static Analysis, 2024
ProFIt

Interpreting Robustness Proofs of Deep Neural Networks

Debangshu Banerjee, Avaljot Singh, and Gagandeep Singh

In The Twelfth International Conference on Learning Representations (ICLR), 2024

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.

Current Projects

ConstraintFlow

We develop a ConstraintFlow, a declarative DSL for specifying Abstract Interpretation-based DNN certifiers. It provides a lightweight automatic verification, which can be used to ensure the over-approximation-based soundness of DNN certifiers. We are also building a compiler that can generate an optimized executabels that can run on different hardwares.

Learn More

Termination Analysis of Programs

We develop Syndicate, a novel framework for proving termination of programs by synergistically generating ranking functions and invariants.

Learn More

Automated Theorem Proving

Using Large Language Models to automatically prove theorems.