I contribute to StatsMLlib, a project formalizing deep learning theory, high-dimensional statistics, probability theory, and concentration inequalities in Lean 4. I work on this project alongside my research.
The project is maintained by the Lean-MoDS community and is an ongoing effort to make rigorous results in modern statistics and machine learning available in a machine-checked form.
Studying how imperfect verifiers interact with inference-time scaling, and when seemingly unfavorable scaling behavior can be misleading. My work develops theoretical tools for understanding the geometry of verifier–utility mismatch and the statistical cost of reliably auditing scaling decisions.
Studying when verification fails to keep pace with recursively improving policies. I combine theoretical analysis with controlled experiments to understand how optimizer-induced policy shifts interact with imperfect or stale verifiers, and how verification should adapt as the policy evolves.