Jiayi Wu (jyah-yee/jiā-yì)

Hello:)

Hi! I'm an undergrad studying Mathematics (A.B.) and Computer Science (Sc.B.) at Brown University.

I hope to build the formal and empirical infrastructure for trustworthy machine learning across two complementary dimensions:

AI for mathematics and automated reasoning: Formal theorem proving [1] [2] and program synthesis [3] [4] are fully specified, unambiguous, machine-checkable substrates for studying models' reasoning processes. Concretely, I'm interested in designing model architectures that leverage various learning paradigms (neurosymbolic programming in particular) to enable more robust and interpretable reasoning, in formal theorem proving and beyond.
Principled evaluation, auditing, and guarantees: I'm interested in designing evaluation and auditing approaches that attach formal or statistical evidence to model properties, from specification conformance and robustness [4] [1] to value alignment [5] and supply-chain provenance. These approaches should generalize across systems, development stages, and deployment contexts.

My Work

Below are selected projects and publications; a more comprehensive list is available in my academic CV.

Interoperability for Formal Mathematics: Automating Proof Translation Across Interactive Theorem Provers, Caltech Summer Undergraduate Research Fellowships (SURF) project advised by Anima Anandkumar, in collaboration with Robert Joseph George.
Formalizing and Benchmarking Overton Pluralism in LLMs, MIT summer visiting student project advised by Michiel Bakker, in collaboration with Elinor Poole-Dayan.
Elinor Poole-Dayan, Jiayi Wu, Taylor Sorensen, Jiaxin Pei, Michiel A. Bakker. Benchmarking Overton Pluralism in LLMs. ICLR 2026. Previously in NeurIPS 2025 Workshop on Evaluating the Evolving LLM Lifecycle. [arXiv] [GitHub] [HuggingFace] [Project Page]
Pattern Mining and Automated Tactic Discovery in Formal Theorem Proving, research project advised by Robert Lewis and Stephen Bach, in collaboration with Gavin Zhao, Zekai Li, and Ilija Ivanov.
Motif of Thoughts (MoT): Reusable Abstractions for Compositional Neurosymbolic Reasoning, research project in collaboration with Chance Jiajie Li.
Chance Jiajie Li*, Jiayi Wu*, Zhenze Mo, Ao Qu, Yuhan Tang, Kaiya Ivy Zhao, Yulu Gan, Jie Fan, Jiangbo Yu, Jinhua Zhao, Paul Pu Liang, Luis Alberto Alonso Pastor, Kent Larson. Simulating Society Requires Simulating Thought. NeurIPS 2025 Position Paper Track (5.7%). [arXiv]

Chance Jiajie Li, Zhenze Mo, Yuhan Tang, Ao Qu, Jiayi Wu, Kaiya Ivy Zhao, Yulu Gan, Jie Fan, Jiangbo Yu, Hang Jiang, Paul Pu Liang, Jinhua Zhao, Luis Alberto Alonso Pastor, Kent Larson. HugAgent: Evaluating LLMs in Simulating Individual-Level Human Reasoning on Open-Ended Tasks. NeurIPS 2025 Workshop on Bridging Language, Agent, and World Models for Reasoning and Planning (Spotlight). Also in NeurIPS 2025 Workshop on PersonaLLM (Oral) and NeurIPS 2025 Workshop on Socially Responsible and Trustworthy Foundation Models. [arXiv] [GitHub]
Neurosymbolic Synthesis of Regular Stream Types, Brown University Undergraduate Teaching and Research Awards (UTRA) project advised by Nikos Vasilakis, in collaboration with Lukas Lazarek, Zekai Li, and Evangelos Lamprou.

Misc

I help organize communities at Brown that connect technology with governance and public-interest perspectives. I’m co-president of Brown’s AI and Robotics Ethics Society (AIRES) and co-director of the AI Governance Panel at Brown China Summit 2025. I'm also writing the AI safety, AI governance, and algorithmic fairness primers for Brown's Socially Responsible Computing (SRC) Handbook. More updates are available here!

In my spare time, I enjoy cold brew, taking on plank challenges (≥7min), thinking, and roaming around the neighborhoods and community spaces I'm involved in 🏘️🌳 -- if I'm not in CIT or the Rock's basement stacks^;