My research focuses on formal methods for reinforcement learning, trustworthy AI, and high-stakes software and cyber-physical systems. I study how learning-enabled and autonomous systems can be designed to operate safely, fairly, and accountably in complex and uncertain environments.
A central goal of my work is to develop intelligent systems whose behavior can be specified, verified, and explained. To this end, I combine formal verification, reinforcement learning, symbolic reasoning, and program analysis.
Foundations and algorithms for reasoning about learning agents beyond finite-state, episodic settings.
I study the integration of formal methods with reinforcement learning to support reliable and structured decision-making in complex environments. My work addresses settings where classical RL abstractions are insufficient, including temporal objectives, recursion, symbolic models, and continuous state spaces.
Combining learning with symbolic reasoning to produce explanations and guarantees.
I develop methods that combine large language models with symbolic tools such as logic, automata, and SMT solvers. The goal is to produce systems that reason in ways that are auditable and grounded, rather than relying only on plausible text generation.
This work includes structured reasoning architectures, proof-guided explanation, and frameworks in which formal methods and learning complement one another.
Auditing and debugging AI-driven software in legal- and social-critical domains.
I study how algorithmic decision-making systems can be tested, audited, and explained when correctness has legal or societal consequences. My work develops formal and data-driven techniques for identifying failures, unfairness, and inconsistencies in software behavior.
Application domains include tax preparation software, juvenile justice, and other public-facing systems where transparency and accountability matter.
Formal guarantees for safety, security, and control under uncertainty.
I develop methods for the analysis and design of safety-critical cyber-physical systems. This work combines control theory, formal verification, and symbolic methods to reason about safety, security, privacy, and resilience in dynamic environments.