Faculty Profile: Prof. Sean Welleck — CMU LTI (L3 Lab)
Faculty Profile: Prof. Sean Welleck — CMU LTI (L3 Lab)
Position: Assistant Professor Institution: Carnegie Mellon University, Language Technologies Institute Lab: L3 Lab (Learning, Language, Logic) — https://cmu-l3.github.io/ Website: https://wellecks.github.io/ Report date: 2026-06-12
Research Focus
LLM reasoning, formal verification, mathematical AI, code generation with proofs, foundations of generative models. Core: developing learning, inference, and evaluation algorithms for LLMs in mathematical reasoning and code.
Academic Profile
- PhD: NYU
- Core researcher, NSF Institute for Computer-Aided Reasoning in Mathematics
- ICLR 2026 paper on premise selection for Lean theorem prover
- Recruiting PhD students Fall 2026 (AI + formal methods, AI agents, foundations of generative models)
Key Publications
| Paper | Venue | Focus |
|---|---|---|
| AlphaVerus | 2025 | Bootstrapping formally verified code generation |
| L1: Controlling Reasoning Length | 2025 | Controllable chain-of-thought reasoning length |
| Diffusion language models with latent tokens | 2025 | Alternative generation paradigms |
| nanoGPT / lm-evaluation-harness contributions | — | Infrastructure for LLM evaluation |
Fit with Weijia Zhang
| Dimension | Assessment |
|---|---|
| LLM reasoning | ✅ Core focus |
| Formal verification + code | ✅ AlphaVerus |
| AI agents | ✅ Stated recruiting interest: “AI agents” |
| Mathematical AI | ✅ Strong |
| RL post-training | ⚠️ Adjacent via reasoning training |
| GUI / VLM agents | ❌ Not his focus |
| RAG / retrieval | ❌ Not primary |
Verdict
P2 套磁（如果你对 reasoning + formal verification 方向感兴趣）。 Recruiting Fall 2026. If Weijia wants to add formal reasoning/verification angle to agent work (e.g., verifiable agent plans), good match. Less relevant if staying purely on GUI/NLP agents.