Grounded Deduction
Summer Research Fellow · EPFL, Switzerland · May 2026 – Present (onsite May – July 2026; remote after)
Adviser: Prof. Bryan Ford, EPFL
- Developing Grounded Deduction, a formal reasoning framework that admits arbitrary recursive definitions without prior termination proofs, using explicit definedness conditions to reason about potentially nonterminating computations.
- Building on an existing Isabelle/Pure implementation of Grounded Deduction, encoded Basic Grounded Arithmetic’s syntax, semantics, and proof checker and proved its consistency within GD, using step-indexed satisfaction.
- Developing GD2, a usability-focused implementation of Grounded Deduction in Isabelle/Pure, with unified terms and formulas, first-class functions, and a definable fixed-point operator supporting recursive and mutually recursive definitions without new axioms or termination proofs at definition time.
- Adapting and extending proof automation and libraries, with comparative case studies in Isabelle/HOL and Lean 4; developing a hammer that translates GD2 goals to first-order problems and reconstructs external proofs in Isabelle.
- Extended GD’s mechanized metatheory by adding proof-checker rules and proving primitive recursiveness and truth preservation; proved that Propositional Grounded Arithmetic (PGA) contains its own truth predicate.
Paper
Report
Slides
Verification Modulo Tested Library Contracts
Student Researcher · IISc · May 2025 – Apr 2026
Advisers: Prof. D. D’Souza (IISc), Prof. P. Madhusudan (UIUC), Prof. A. Murali (UW-Madison)
- Co-developed VMTLC, a framework that verifies client programs assuming synthesized library contracts, while testing those contracts against the library implementations.
- Co-designed the Learner component within a Teacher-Learner CEGIS loop, developing two distinct LLM-integrated architectures (a pure LLM learner and an LLM-seeded ICE learner) to leverage semantic intuition, synthesizing valid contracts where traditional enumerative baselines could not.
- Independently designed and implemented the LLM pipeline for synthesizing contracts and invariants from logical constraints, including prompt templates, counterexample-driven repair, malformed-output handling, and integration with formal verification and testing; implemented LLM-generated attributes for the hybrid HornICE learner.
- Designed and implemented two mutation templates producing 30 incorrect programs that escaped testing; analyzed when modular and contextual VMTLC rejected or accepted them.
Paper
Code
Causal Discovery in Time Series
Student Researcher · IISc · Aug 2025 – Present
Adviser: Prof. Deepak N. Subramani, Computational and Data Sciences, IISc
- Led the research and designed and implemented Mask2Cause, a Transformer framework for causal discovery through conditional mean and variance prediction using adjacency-constrained attention over inverted variable embeddings.
- Designed a variance-aware prediction objective and the novel Mixed Physics benchmark to study dependencies expressed through conditional mean and variance; developed an information-theoretic analysis motivating the objective.
- Designed controlled experiments investigating information leakage, hidden confounding, changing causal graphs, and separation of mean and variance parents; used the findings to refine architectural claims and characterize limitations.
Paper
Code
Finite Automata in Repeated Games
Student Researcher · IISc · Jan 2026 – Present
- Leading a collaborative investigation of repeated Prisoner’s Dilemma strategies implemented as finite automata, studying how per-state memory costs affect cooperation and equilibrium.
- Derived a tight cost threshold for sustaining eventual mutual cooperation in Nash equilibrium, and bounds on when non-defection outcomes disappear under Nash and semi-perfect equilibrium.
Formalization of Group Theoretic Algorithms
Summer Research Fellow · Krea University, India (Onsite) · May 2025 – July 2025
Advisers: Prof. Rishi Vyas (KREA), Prof. T.V.H Prathamesh (KREA)
- Formalized proofs for decision problems in geometric group theory (including the word, conjugacy, and subgroup membership problems) using the Lean 4 proof assistant.
- Key contributions include formalizing two definitions of the Dehn function and proving their equivalence and verifying the algorithm for the conjugacy problem in free groups.
- The project forms part of a broader research effort on formalizing algorithms in geometric group theory, including the computability of Dehn functions for hyperbolic groups, for which I helped formalize the foundations.
Enhancing Formal Verification with LLMs
Research Intern · University of Virginia, USA (Remote) · Aug 2025 – Oct 2025
Adviser: Prof. Wenxi Wang, The University of Virginia
- Explored techniques for decomposing Z3 proof objects for Verus-generated verification conditions into dependency-preserving proof subtrees, aiming to make solver reasoning easier for LLMs to interpret.
- Assisted with evaluation of LLM-generated verification proofs and literature review; contributions acknowledged in the resulting ICML 2026 paper introducing VCoT-Lift and VCoT-Bench.
