Research perspective

I study how AI agents can solve challenging programming and mathematical problems, with a focus on learning from reliable feedback. My work brings together model training and test-time search: training develops reusable reasoning strategies, while search lets agents explore, check, and refine solutions to harder tasks.

Testing, symbolic solvers, and proof assistants provide complementary feedback in this process. I use them to build training signals, guide search, and evaluate solutions against explicit requirements. I am particularly interested in bringing these ideas to real-world software, where generating plausible code is only the beginning: the code must also satisfy its specification.

Selected projects

Code-Verification Agents. We combine SFT/RL training with hierarchical proof search to build code-verification agents, from Goedel-Code-Prover to an internal 200B-parameter model. Paper ↗ · Code ↗

Verified Kernel Optimization. We build an agent-driven framework for optimizing real-world LLM pre-training kernels, combining a testing harness with Lean 4 proof generation to verify correctness. Website ↗ · Code ↗

Verified Code Generation for Real-World Systems. We introduce Vero, a benchmark of 103 Lean 4 tasks derived from eBPF, LLVM, and seL4, to evaluate agents’ ability to generate code and prove it meets new specifications. Paper ↗ · Code ↗

Search-Based Formal Reasoning. We combine LLM-guided tree search with symbolic reasoning and proof-assistant feedback to tackle Olympiad inequalities and operating-system verification. NeqLIPS Paper ↗ · Code ↗ · seL4 Paper ↗ · Code ↗