Research
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.