Architecting LLM-driven agent systems for mobility modeling and behavioral inference in the SERMoS Lab.

• Built a LangGraph-based multi-agent system (Planner, Coder, Critic) to automate analysis of large-scale mobile location data.
• Integrated cAST (Chunking via Abstract Syntax Trees) to retrieve and apply complex codebase documentation for transportation agencies.
• Developed the SAPA framework to synthesize psychometric variables from survey data, improving PR-AUC for ridesourcing mode choice prediction by 75.9%.
• Co-developed the GHOST Python package for bias-mitigated home detection, reducing spatial error to 1.84 meters on the Boston Walks dataset.
• Leading a household travel simulation where LLM agents negotiate shared resources via a structured conversation protocol.

Investigated multi-agent LLM architectures for the Chicago Transit Authority (CTA).

• Designed a Spatial-RAG pipeline blending dense retrieval with sparse spatial lookup (GTFS/GIS geometry).
• Enabled agents to reason about delay propagation, rerouting, and simulate station-level dispatchers.
• Collaborated with transit operations researchers on deploying LLM agents for policy-driven scenarios.

Led research on formal methods and AI-driven feedback loops for mathematical proof automation and verification.

• Designed the FORMAL system, combining retrieval-augmented thinking with agentic reasoning to translate natural language mathematics into Lean 4 code.
• Achieved 92% syntactic correctness and 83% semantic accuracy on the Lean-Workbook dataset using local LLMs.
• Built dynamic vector stores for theorem statements and tactic examples, enabling efficient proof search and verification.