projects
L3 Lab research areas and projects. Click a project for related publications.
AI and Formal Methods
We develop AI systems that use formal methods to advance mathematics and software, along with tools that make machine-checked reasoning broadly useful.
AI for Formal Mathematics
We aim to build AI systems that can understand, create, and verify mathematics in collaboration with people and proof assistants.
See more…AI for Verified Software
We aim to build AI systems that produce software with machine-checkable guarantees and make formal verification a routine part of software development.
See more…AI Tools for Formal Verification
We build AI-powered tools that make formal verification more accessible, efficient, and useful to mathematicians and programmers.
See more…Reasoning and Agents
We build models and agents that reason, act through computers, and improve through interaction and feedback.
Computer-Use Agents
We aim to build general-purpose agents that can reliably carry out any task achievable through a computer interface.
See more…Reasoning Models
We aim to make reasoning models more capable, controllable, and efficient, including through inference-time scaling and efficient inference.
See more…Continually Improving AI
We aim to build AI systems that learn from feedback, experience, and their own failures to become more capable over time.
See more…Foundations of Language Models
We study the principles and algorithms underlying how language models learn, generate, and generalize.
Learning and Optimization
We study how objectives, data, and optimization shape what language models learn and how effectively they generalize.
See more…Inference and Generation
We develop algorithms that make language-model inference and generation more capable, efficient, and reliable.
See more…Evaluation and Generalization
We develop rigorous ways to evaluate language models and understand when, how, and why they generalize.
See more…