Kaiyu Yang 杨凯峪

I lead a research team at Apodex working on large language models for mathematics and verification. AI systems generate code and proofs faster than anyone can check them, and as generation gets cheaper, verification becomes the bottleneck. We work on closing that gap: models and systems that verify AI outputs cheaply and reliably, so the human review needed to trust them keeps shrinking.

Mathematics is where this is furthest along, because correctness there can be checked automatically. The same principle applies wherever outputs can be assessed automatically, including AI's own training pipelines, from the correctness of GPU kernels to the quality of training data.

What we work on

• Mathematics. No one stage of training creates mathematical ability, so we work on all of them: pre-training data that aims to capture all the math on the web, synthetic mid-training data distilled from research papers, and post-training pushing toward research-level mathematics.
• Verification. We build verifiers that help agents complete long-horizon tasks: the longer the task, the more errors compound, and the more a cheap, reliable check is worth. Frontier LLMs broaden what can be verified to include outputs that had no dependable check before.

Background

I have worked on machine learning for formal mathematics since my PhD at Princeton. Before Apodex, I was a research scientist at Meta FAIR and a postdoctoral fellow at Caltech. Full background and publications →

Selected earlier work

• NeurIPS 2023 LeanDojo: Theorem Proving with Retrieval-Augmented Language Models The first open-source infrastructure for theorem proving with LLMs in Lean; used by projects at Meta, ByteDance, and DeepSeek.
• COLM 2025 · ICLR 2026 Goedel-Prover and Goedel-Prover-V2 Theorem provers that set the state of the art among open models at release, outperforming provers 20× their size.
• ICLR 2026 Verina: Benchmarking Verifiable Code Generation Benchmark for generating code together with machine-checkable proofs of correctness; early adopters include AWS and Harmonic.
• ICML 2019 Learning to Prove Theorems via Interacting with Proof Assistants Introduced CoqGym; among the first to apply neural networks to proof assistants, groundwork for today's LLM-based provers.
• ICML 2024 Autoformalizing Euclidean Geometry Enabled the first faithful formalization of Euclid's Elements, Book I, in a modern proof assistant; uncovered mistakes in Euclid's original proofs.