|
Zachary Burton |
|
I am a machine learning engineer at Meta working on Facebook Reels ranking. I graduated from MIT with an SB in Mathematics.
My research interests span reinforcement learning, formal reasoning, and AI-guided proof. I've built training environments for RLHF (PIEFACE), studied where RL breaks on symbolic tasks (blog), and explored structured prompting for neural theorem provers (arXiv).
I was born in NYC and raised in the UK. Outside of work, I play goalkeeper in a Sunday football league. Feel free to reach out if you want to chat!
|
Structured Hints for Sample-Efficient Lean Theorem Proving
Preprint, 2026 arXiv Testing whether neural theorem provers benefit from lightweight structural guidance. Achieves 43% relative improvement on miniF2F with a simple prompt schedule. |
|
|
When Does Tabular RL Actually Break?
Blog Post, 2025 post A systematic study of representation bottlenecks in symbolic algebra, testing where RL breaks on high school math. |
|
Collision Thresholds on Lattices
Preprint arXiv An expository derivation using Poissonization and Laplace asymptotics to analyze random walks on lattices. |
|
PIEFACE
website A full-stack platform for crowdsourcing human feedback on mathematical reasoning traces, with a Flask backend, SQL storage, trace parser, and distributed PPO training loop. |
|
zOS
github Local LLM self-training loop with step-by-step feedback, written with Rust & Tauri. |
|
Formal Complexity Science
github Autoformalization of classical NP-completeness reductions in Lean 4, built on Mathlib and CSLib. Formalizes Karp reductions (SAT ≤ 3SAT ≤ 3-COLORING, with more planned) as machine-checked proofs. |
|
|
LLM Political Persuasion?
paper 17.279 (Political Misinformation in the Age of Social Media) Final Paper - independent empirical study (n=174, randomized) on AI disclosure effects on belief formation in political conspiracy-framing content. |
|
|
Scribe AI
devpost Autocomplete for math handwriting. |
