Bio

Brando Miranda is a Ph.D. student in Artificial Intelligence / Machine Learning (AI/ML) at Stanford University under the supervision of Professor Sanmi Koyejo in the Stanford Trustworthy AI Research (STAIR) group. Previously, he was a graduate researcher at the University of Illinois Urbana-Champaign and held research appointments at the Massachusetts Institute of Technology (MIT) — including a Research Assistantship in MIT’s Center for Brains, Minds and Machines (CBMM). He earned his Master of Engineering in Electrical Engineering and Computer Science at MIT, conducting deep-learning-theory research under Professor Tomaso Poggio — who also supervised DeepMind co-founder Demis Hassabis during his post-doctoral fellowship.

Miranda’s research centers on AI for formal mathematics — Lean 4 theorem proving, autoformalization, and end-to-end formal verification of software and mathematics — alongside contamination-resistant evaluation of LLM mathematical reasoning and data-centric machine learning for foundation and frontier models, with broader interest in alternative architectures (e.g. energy-based models) toward Artificial General Intelligence (AGI). He is the co-founder and president of Stanford AI for Lean, a research community advancing AI for Lean theorem proving and formalizing mathematics. His work has earned the inaugural Veritas Scholar offer from Math Inc. (offered, declined), the NeurIPS Outstanding Main Track Paper Award (top 0.4%, 2 papers selected), the International Journal of Automation & Computing “Most Cited Paper” Certificate, two Honorable Mentions from the Ford Foundation Fellowship, the Saburo Muroga Computer Science Excellence Fellowship, the Stanford School of Engineering Fellowship, and selection as an EDGE Scholar at Stanford.

Miranda is more than a researcher—he is an innovator, communicator, and deeply passionate about the future of AI. As a Machine Learning Research Scientist Consultant at the venture-backed AI startup Morph Labs, he made key contributions to the Morph Prover model and helped launch Moogle.ai, the first search engine for verified code in Lean. He later applied the same expertise as an AI consultant to Wise Agents—featured in Forbes Mexico — a Stanford spin-out leveraging AI agents to transform sales performance.

Shorter Bio

Brando Miranda is a Ph.D. student in Artificial Intelligence / Machine Learning at Stanford University, advised by Prof. Sanmi Koyejo in the Trustworthy AI Research (STAIR) group. His work targets AI for formal mathematics (Lean 4 theorem proving, autoformalization, end-to-end formal verification of software and mathematics), contamination-resistant evaluation of LLM math reasoning, and data-centric techniques for foundation/frontier models toward AGI. He is the co-founder and president of Stanford AI for Lean, a research community advancing AI for Lean theorem proving and formalizing mathematics. Miranda received the NeurIPS Outstanding Paper Award (top 0.4%) and other honors for his research. In industry, he served as Machine-Learning Research Scientist Consultant at venture-backed Morph Labs, helping build the Morph Prover v0-7B and launch Moogle.ai, the first search engine for verified code in Lean. He later brought the same expertise to Wise Agents, a Stanford spin-out that uses AI agents to transform sales performance.

Selected Publications [Full List]

Selected publications are listed reverse-chronologically; see Google Scholar for the full list and citation metrics.

VeriBench: End-to-End Formal Verification Benchmark for AI Coding Agents in Lean 4 (2026) Brando Miranda, Srivatsava Daruru, Ethan S. Hersch, Zhanke Zhou, Allen Nie, Daneshvar Amrollahi, Leni Aniva, Iddah Mlauzi, et al. [Preprint] [2nd Workshop on AI for Math at International Conference on Machine Learning (ICML) 2025]

CoDaPO: Confidence and Difficulty-Adaptive Policy Optimization for LLM Reasoning (2026) Zhanke Zhou, Xiangyu Lu, Chentao Cao, Brando Miranda, Tongliang Liu, Bo Han, Sanmi Koyejo. [International Conference on Machine Learning (ICML) Main Track 2026] [International Conference on Learning Representations (ICLR) Workshop on Lifelong Agents 2026] [2nd Workshop on AI for Math at International Conference on Machine Learning (ICML) 2025]

Pretraining Scaling Laws for Generative Evaluations of Language Models (2026) Rylan Schaeffer, Noam Levi, Brando Miranda, Sanmi Koyejo. [International Conference on Learning Representations (ICLR) Main Track 2026] [arXiv]

Rethinking LLM Judges: Chain-of-Thought and Multi-Step Pipelines for Math Grading (2026) Eric Chen, Aryan Gulati, Brando Miranda, Zeyu Tang, Sanmi Koyejo. [International Conference on Learning Representations (ICLR) Workshop on Logical Reasoning of Large Language Models 2026]

AI Coding Benchmarks Need Proofs, Not Just Tests (2026) Danesh Amrollahi, M. Karimi, Brando Miranda, Leni Aniva, Chuyue Sun, Clark Barrett, Sanmi Koyejo. [Preprint]

VeriBench-FTP: A Formal Theorem Proving Benchmark in Lean 4 for Code Verification (2025) Slim Barkallah, Srivatsava Daruru, Brando Miranda, Leni Aniva, Allen Nie, Sanmi Koyejo. [Neural Information Processing Systems (NeurIPS) Mathematical Reasoning and AI Workshop 2025]

Why Has Predicting Downstream Capabilities of Frontier AI Models with Scale Remained Elusive? (2025) Rylan Schaeffer, Hailey Schoelkopf, Brando Miranda, Gabriel Mukobi, Varun Madan, Adam Ibrahim, Herbie Bradley, Stella Biderman, Sanmi Koyejo. [International Conference on Machine Learning (ICML) 2025] [ICML Outstanding Paper Trustworthy Multi-modal Foundation Models and AI Agents (TiFA) Workshop 2024 award] [arxiv]

Putnam-AXIOM: A Functional & Static Benchmark for Measuring Higher Level Mathematical Reasoning in LLMs (2025) Brando Miranda*, Aryan Gulati*, Eric Chen*, Emily Xia*, Kai Fronsdal*, Bruno de Moraes Dumont, Sanmi Koyejo. (*equal contribution) [International Conference on Machine Learning (ICML) Main Track 2025] [Neural Information Processing Systems (NeurIPS) Mathematics and AI (MATH-AI) Workshop 2024] [arXiv]

Pantograph: A machine-to-machine interaction interface for advanced theorem proving, high level reasoning, and data extraction in Lean 4 (2025) Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett, Sanmi Koyejo. [International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2025]

Causally Quantifying the Effect of Test Set Contamination on Generative Benchmarks (2025) Rylan Schaeffer, Brando Miranda, Joshua Kazdan, Ken Liu, Ahmed M. Ahmed, Niloofar Mireshghallah, Sanmi Koyejo. [Neural Information Processing Systems (NeurIPS) Workshop on Evaluating the Evolving LLM Lifecycle: Benchmarks, Emergent Abilities, and Scaling 2025] [NeurIPS] [arXiv]

Position: Machine Learning Conferences Should Establish a “Refutations and Critiques” Track (2025) Rylan Schaeffer, J. Kazdan, Y. Denisov-Blanch, Brando Miranda, M. Gerstgrasser, et al. [Advances in Neural Information Processing Systems 38 (NeurIPS) Position Paper Track Oral 2025] [OpenReview] [arXiv]

Lean-ing on Quality: How High-Quality Data Beats Diverse Multilingual Data in Autoformalization (2025) W. Chan, M. Souliman, J. Nordhagen, Brando Miranda, Elyas Obbad, Sanmi Koyejo. [arXiv]

Failures to Find Transferable Image Jailbreaks Between Vision-Language Models (2024) Rylan Schaeffer, Dan Valentine, Luke Bailey, James Chua, Cristobal Eyzaguirre, Zane Durante, Joe Benton, Brando Miranda, Henry Sleight, Tony Tong Wang, John Hughes, Rajashree Agrawal, Mrinank Sharma, Scott Emmons, Sanmi Koyejo, Ethan Perez. [International Conference on Learning Representations (ICLR) 2024] [Neural Information Processing Systems (NeurIPS) Red Teaming GenAI Workshop 2024]

Does Maximizing Neural Regression Scores Teach Us About The Brain? (2024) Rylan Schaeffer, M. Khona, S. Chandra, M. Ostrow, Brando Miranda, Sanmi Koyejo. [Neural Information Processing Systems (NeurIPS) Workshop on Unifying Representations in Neural Models (UniReps), 2nd Edition 2024]

Quantifying the Importance of Data Alignment in Downstream Model Performance (2024) K. Chawla, A. Sahai, M. DePavia, S. Sundar, Brando Miranda. [International Conference on Learning Representations (ICLR) Workshop on Data-Centric Machine Learning Research (DMLR) 2024]

An Evaluation Benchmark for Autoformalization in Lean4 (2024) Aryan Gulati, D. Ladsaria, S. Mishra, J. Sidhu, Brando Miranda. [International Conference on Learning Representations (ICLR) Tiny Papers Track, Second Edition 2024]

ZIP-FIT: Embedding-Free Data Selection via Compression-Based Alignment (2024) Elyas Obbad, Iddah Mlauzi, Brando Miranda, Rylan Schaeffer, K. Obbad, S. Bedi, Sanmi Koyejo. [arXiv]

Morph Prover v0 7b: The 1st Frontier Model for the Lean 4 Formal Verification Programming Language (2024) [blog] [Hugging Face Model Card]

Are Emergent Abilities of Large Language Models a Mirage? (2023) Rylan Schaeffer, Brando Miranda, Sanmi Koyejo. [Neural Information Processing Systems (NeurIPS) Outstanding Main Track Paper Award 2023 & NeurIPS Oral] [OpenReview] [arXiv]

Is Pre-training Truly Better Than Meta-Learning? (2023) Brando Miranda, Patrick Yu, Saumya Goyal, Yu-Xiong Wang, Sanmi Koyejo. [International Conference on Machine Learning (ICML) Data-Centric Machine Learning Workshop 2023] [Poster] [arXiv]

Beyond Scale: the Diversity Coefficient as a Data Quality Metric Demonstrates LLMs are Pre-trained on Formally Diverse Data (2023) Brando Miranda*, Alycia Lee*, Patrick Yu, and Oluwasanmi Koyejo. [International Conference on Machine Learning (ICML) Data-Centric Machine Learning Workshop 2023 & ICML Challenges in Deployable Generative AI Workshop 2023] [Poster] [arXiv] [Code]

The Curse of Low Task Diversity: On the Failure of Transfer Learning to Outperform MAML and Their Empirical Equivalence (2022) Brando Miranda, Patrick Yu, Yu-Xiong Wang, Oluwasanmi Koyejo. [Neural Information Processing Systems (NeurIPS) Meta-Learning Workshop 2022] [OpenReview] [arXiv] [Slides] [Poster] [5 minute video]

Does MAML Only Work via Feature Re-use? A Data Set Centric Perspective (2021) Brando Miranda, Yu-Xiong Wang, Oluwasanmi Koyejo. [Best research project award for graduate course CS 598 “Learning to Learn” by professor Y. Wang UIUC (December 2020)] [arXiv] [5 minute video]

Weight and Batch Normalization implement Classical Generalization Bounds (2019) Tomaso Poggio, Andrzej Banburski, Qianli Liao, Brando Miranda, Lorenzo Rosasco, Jack Hidary. [International Conference on Machine Learning (ICML) Workshop 2019] [PDF]

High-performance and scalable on-chip digital Fourier transform spectroscopy (2018) Derek M Kita, Brando Miranda, David Favela, David Bono, Jérôme Michon, Hongtao Lin, Tian Gu, Juejun Hu. [Nature Communications 2018]

Why and when can deep-but not shallow-networks avoid the curse of dimensionality: a review (2017) Tomaso Poggio, Hrushikesh Mhaskar, Lorenzo Rosasco, Brando Miranda, Qianli Liao. [International Journal of Automation and Computing 2017, Most Cited Paper Certificate awarded by International Journal of Automation & Computing (IJAC)] [Award]

Talks

Applications of Trustworthy Machine Reasoning with AI Coding Agents — AAAI 2026 Tutorial “Trustworthy Machine Reasoning with Foundation Models” (Part IV, 50 min). Co-presented with B. Han, Z. Zhou, C. Cao, P. Lu, S. Koyejo. Singapore, January 20, 2026.
Emergent Abilities in Large Language Models: Mirage or an Elusive Predictive Frontier? — Hong Kong Baptist University, Department of Computer Science Seminar. Hong Kong, January 19, 2026.
Applications of Trustworthy Machine Reasoning with AI Coding Agents — Hong Kong Baptist University, Department of Computer Science Seminar, invited. Hong Kong, January 2026.
VeriBench: End-to-End Formal Verification Benchmark for AI Code Generation in Lean 4 — Lawrence Livermore National Laboratory Reading Group, invited. July 31, 2025.
Intro to Lean 4, VeriBench, and Trustworthy Testing with Theorems — Prof. Azalia Mirhoseini’s Lab Meeting, Stanford, invited. 2025.
Are Emergent Abilities of Large Language Models a Mirage? — Why Has Predicting Downstream Capabilities Remained Elusive? — Lawrence Livermore National Laboratory, invited talk. 2025.
Are Emergent Abilities of Large Language Models a Mirage? — Stanford IEEE Invited Talk, slides. Stanford, CA, 2023.
Emergent Abilities of Large Language Models — Amazon Research, invited talk. 2023.
The Curse of Low Task Diversity: On the Failure of Transfer Learning to Outperform MAML and Their Empirical Equivalence — NeurIPS Meta-Learning Workshop, Contributed Talk, slides. New Orleans, LA, December 2022.

Media Coverage

Below are selected links showcasing media coverage of selected work:

Hacker News / Y Combinator (January 2025): The Putnam-AXIOM benchmark for higher-level LLM mathematical reasoning was posted on Hacker News, Y Combinator’s influential tech-news front page.

Aran Komatsuzaki / @arankomatsuzaki on X (June 2024): Shared the Why Has Predicting Downstream Capabilities of Frontier AI Models with Scale Remained Elusive? paper to his AI-research audience — an AI-research commentator with early work on GPT-J, LAION, scaling, and MoE.

AIhub (April 2024): Interview with Brando Miranda on the NeurIPS Outstanding Paper Award-winning emergent-abilities paper.

American Scientist (March-April 2024): “Is There an AI Metrics Mirage?”

White House Economic Report of the President (March 2024): Miranda et al.’s work was cited in the 2024 Economic Report of the President. Direct quote: “The Report presents an overview of the nation’s economic progress and makes the case for the Biden-Harris Administration’s economic policy priorities.” [Report] [Screenshot]

Andrew Ng (March 2024): Endorsed the emergent-abilities paper as evidence that Artificial General Intelligence (AGI) won’t come discontinuously, but instead, will come smoothly and predictably

Quanta Magazine (February 2024): “How Quickly Do Large Language Models Learn Unexpected Skills? - A new study suggests that so-called emergent abilities actually develop gradually and predictably, depending on how you measure them.”

Stanford AI Lab Blog (ICML 2023): The Beyond Scale and Is Pre-training Truly Better Than Meta-Learning? papers were featured in the Stanford AI Lab blog roundup of ICML 2023.

AK / @_akhaliq on X (June 2023): AK shared the Beyond Scale data-diversity paper to his AI-research audience — the influential AI-research-paper aggregator (Gradio founder; now at HuggingFace), 68.9K views.

The New York Times (June 2023): “Silicon Valley Confronts the Idea That the ‘Singularity’ Is Here”

The Register (May 2023): “LLM emergent behavior written off as ‘a mirage’ by study”

Y Combinator News (May 2023): “Are emergent abilities of large language models a mirage?”

Stanford’s Institute for Human-Centered Artificial Intelligence (HAI) (May 2023): “AI’s Ostensible Emergent Abilities Are a Mirage”

Forbes (May 2023): “AI ‘Emergent Abilities’ Are A Mirage, Says AI Researcher”

Vice / Motherboard (May 2023): “Scary ‘Emergent’ AI Abilities Are Just a ‘Mirage’ Produced by Researchers, Stanford Study Says”

This work was also covered by: Medium, Hacker News, NeurIPS blog, Reddit, and more, courtesy of Google search.

Awards

Inaugural Veritas Scholar, Math Inc. (offered, declined; 2026) — selected for the inaugural Veritas Scholar offer, recognizing frontier work in AI-assisted formalization and verified mathematics.
ICML 2026 Silver Reviewer (May 2026) — top reviewer recognition signed by the ICML 2026 Program Chairs.
Oral Recommendation (Top 1), 2nd AI for Math Workshop @ ICML 2025 — for VeriBench: End-to-End Formal Verification Benchmark for AI Code Generation in Lean 4 (Miranda et al.); reviewer recommendation “Accept (Oral, Top 1)”.
Pear AI Researchers Circle (July 2025) — selective AI-researcher network convened by Pear VC; invited following the final round (R3) of the Pear AI Researcher Grant program.
ICML Workshop on Trustworthy Multi-modal Foundation Models and AI Agents (TiFA) — Outstanding Paper Award (July 2024) — for “Why Has Predicting Downstream Capabilities of Frontier AI Models with Scale Remained Elusive?” (Schaeffer, Schoelkopf, Miranda, et al.).
Neural Information Processing Systems (NeurIPS) Outstanding Main Track Paper Award (December 2023) — top 0.4% of NeurIPS submissions; only 2 main-track papers selected. For “Are Emergent Abilities of Large Language Models a Mirage?” (Schaeffer, Miranda, Koyejo).
EDGE Scholar, Stanford University (September 2022) — Stanford fellowship supporting first-generation / low-income PhD scholars.
Stanford School of Engineering Fellowship (September 2022) — multi-year departmental fellowship for incoming engineering PhDs.
Honorable Mention, Ford Foundation Predoctoral Fellowship (2020, 2021) — national fellowship recognizing PhD applicants with potential to diversify the U.S. professoriate.
Best Research Project Award, UIUC graduate course CS 598 “Learning to Learn” (December 2020) — course-level award for the top research project.
HSF Scholar, Hispanic Scholarship Fund (2020) — competitive national merit fellowship for Hispanic graduate students.
Computer Science Excellence Saburo Muroga Endowed Fellow, UIUC (2019-2020) — top departmental fellowship for incoming CS PhDs.
Most Cited Paper Certificate, International Journal of Automation & Computing (IJAC, December 2019) — for “Why and when can deep- but not shallow-networks avoid the curse of dimensionality: a review”.
Sloan Scholar, Alfred P. Sloan Foundation Minority Ph.D. (MPHD) Program (2018-2019) — national fellowship for underrepresented STEM PhD students.
Grainger Engineering SURGE Fellowship, UIUC (2018-2019) — multi-year college-level fellowship for diverse engineering PhDs.
MIT Mitchell B. Kaufman Memorial Scholarship (2012-2013, 2013-2014) — MIT undergraduate scholarship support.
MIT Eugene and Margaret McDermott Scholarship (2012-2013, 2013-2014) — MIT undergraduate scholarship support.
Chopper Trading, LLC, Best Strategy Report Award, MIT BattleCode AI competition (2013) — top finisher among ~300 teams.
Greengates Scholarship (30% 2007, 50% 2008, 100% 2009, 100% 2010) — merit scholarship that increased to full-tuition support.
High Achievement Prize Award, Greengates School (2007, 2008, 2009, 2010) — equivalent to Valedictorian.
Best All-Round Student Award, Greengates School (2010) — school-wide award recognizing the top all-around student.
Achievement Prize Award, Greengates School (2006) — school recognition for academic achievement.
Certificate for Progress Award, Greengates School (2005) — school recognition for academic progress.

Research Artifacts & Systems

VeriBench: end-to-end Lean 4 benchmark for evaluating AI-generated code with formal verification proofs.
VeriBench-FTP: formal theorem-proving benchmark in Lean 4 for code verification.
Putnam-AXIOM: functional and static benchmark for higher-level LLM mathematical reasoning.
Putnam-AXIOM-Grading: human-graded 1,000-solution benchmark for Putnam-style partial-credit mathematical evaluation.
Pantograph: machine-to-machine interface for Lean 4 theorem proving, reasoning, and data extraction.
Morph Prover v0 7B and Moogle.ai: Lean 4 proof model and search engine for verified Lean code developed with Morph Labs.
AlphaApollo: agentic reasoning framework for tool-integrated reasoning, agentic post-training, and self-evolving verification workflows. [arXiv]
AlphaDiana: harness-aware evaluation system for open agents on verifiable reasoning tasks with trajectory logging.
ultimate-utils: reusable ML and research-engineering utility library for experiment workflows.

Selected Writing

Metallica Goes Jazz: A 2010 High School Arrangement, Reanimated by AI — May 2026.
Embrace AI or Be Left Behind — By People, Not Machines — April 2026.
Asking the Right Question: Formal Methods as Scalable Oversight — April 2026.
What I Learned Building a Correctness-Gated Multi-Agent Workflow for Research — April 2026.

Selected service and mentoring writing is available in the blog archive, including posts on research community, graduate-school statements, mindfulness, and team-building.