| CARVIEW |
Gabriel Poesia
- PhD in Computer Science at Stanford, advised by Noah Goodman.
- Research Fellow at the Kempner Institute at Harvard
- Incoming (Fall 2026) Assistant Professor of Computer Science and Engineering at the University of Michigan
- I'll be recruiting CS PhD students in the next admissions cycle (Fall 2025)! If you're interested in formal reasoning and AI/ML, consider applying to the UMich CSE PhD program!
I'm interested in building self-improving AI systems that are capable of formal reasoning (e.g., proving mathematical theorems, synthesizing and verifying programs) and open-ended discovery. This requires interfacing ideas from type theory (to define a game of formal theorem proving), reinforcement learning (to become steadily better at this game), language models (to represent policies, value functions, and leverage informal reasoning), program induction (to discover useful symbolic abstractions - lemmas, tactics, or definitions), and the whole toolbox from game-playing AI (e.g., tree search, self-play). Ultimately, I believe formal systems also ought to be useful for human learning if we understand how to pedagogically leverage their feedback on one's reasoning, rather than final answers, and their support for open-ended exploration.
If these topics sound interesting to you, and you're thinking about pursuing a PhD in Computer Science, consider applying to UMich and mentioning my name in your application!
Publications
| COLM 2025 |
From Next-Token to Mathematics: The Learning Dynamics of Mathematical Reasoning in Language Models Shubhra Mishra, Gabriel Poesia and Noah Goodman [Link] |
| OOPSLA 2025 |
Automated Discovery of Tactic Libraries for Interactive Theorem Proving Yutong Xin, Jimmy Xin, Gabriel Poesia, Noah Goodman, Qiaochu Chen and Isil Dillig [arXiv] |
| ICML 2025 Spotlight |
Position: Formal Mathematical Reasoning - A New Frontier in AI Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin E. Lauter, Swarat Chaudhuri and Dawn Song [arXiv] |
| ICLR 2025 |
h4rm3l: A Language for Composable Jailbreak Attack Synthesis Moussa Doumbouya, Ananjan Nandi, Gabriel Poesia, Davide Ghilardi, Anna Goldie, Federico Bianchi, Dan Jurafsky and Christopher D. Manning [Link] [arXiv] [Code] |
| POPL Dafny Workshop 2025 |
dafny-annotator: AI-Assisted Verification of Dafny Programs Gabriel Poesia, Chloe Loughridge and Nada Amin [arXiv] [Code] [Blog post] |
| NeurIPS 2024 Oral |
Learning Formal Mathematics From Intrinsic Motivation Gabriel Poesia, David Broman, Nick Haber and Noah D. Goodman [arXiv] [Code] |
| ICML 2024 |
When do Skills Help Reinforcement Learning? A Theoretical Analysis of Temporal Abstractions Zhening Li, Gabriel Poesia and Armando Solar-Lezama [Link] [arXiv] |
| TMLR 2024 Invited to ICLR |
Certified Deductive Reasoning with Language Models Gabriel Poesia, Kanishk Gandhi*, Eric Zelikman* and Noah D. Goodman [arXiv] |
| ICLR 2024 |
Hypothesis Search: Inductive Reasoning with Language Models Ruocheng* Wang, Eric Zelikman*, Gabriel Poesia, Yewen Pu, Nick Haber and Noah D. Goodman [arXiv] |
| Phil. Trans. of the Royal Society A 2023 |
Peano: Learning Formal Mathematical Reasoning Gabriel Poesia and Noah D. Goodman [arXiv] |
| NeurIPS 2023 Spotlight |
Parsel🐍: Algorithmic Reasoning with Language Models by Composing Decompositions Eric Zelikman, Qian Huang, Gabriel Poesia, Noah D. Goodman and Nick Haber [arXiv] |
| NeurIPS Math-AI 2022 |
Lemma: Bootstrapping High-Level Mathematical Reasoning with Learned Symbolic Abstractions Zhening Li*, Gabriel Poesia*, Omar Costilla-Reyes, Noah Goodman and Armando Solar-Lezama [Link] [arXiv] [PDF] |
| CogSci 2022 |
Left to the Reader: Abstracting Solutions in Mathematical Reasoning Gabriel Poesia and Noah Goodman [PDF] |
| ICLR 2022 |
Synchromesh: Reliable Code Generation from Pre-trained Language Models Gabriel Poesia*, Alex Polozov*, Vu Le, Ashish Tiwari, Gustavo Soares, Chris Meek and Sumit Gulwani [PDF] |
| NeurIPS 2021 |
Contrastive Reinforcement Learning of Symbolic Reasoning Domains Gabriel Poesia, WenXin Dong and Noah Goodman [arXiv] |
| EMNLP 2021 |
Open-domain clarification question generation without question examples Julia White, Gabriel Poesia, Robert Hawkins, Dorsa Sadigh and Noah Goodman [Link] [PDF] |
| AAAI 2021 |
Pragmatic Code Autocomplete Gabriel Poesia and Noah D. Goodman [Link] [PDF] [Code] |
| OOPSLA 2020 |
Dynamic Dispatch of Context-Sensitive Optimizations Gabriel Poesia and Fernando Magno Quintão Pereira [Link] [PDF] [Code] |
| OOPSLA 2017 |
Static Placement of Computation on Heterogeneous Devices Gabriel Poesia, Breno Guimarães, Fabrício Ferracioli and Fernando Magno Quintão Pereira [Link] [PDF] |
| ECML/PKDD 2014 |
A Lossless Data Reduction for Mining Constrained Patterns in n-ary Relations Gabriel Poesia and Loïc Cerf [Link] [PDF] |
Other interests
Programming contests. I used to be an ACM-ICPC competitor (world finalist in 2015), and generally involved in programming contests in various ways. In particular, I authored 3 problems for the ACM-ICPC Latin American regionals, 2 in 2017, one in 2020, and another one upcoming in 2023. I've also coached several teams, taught at training camps in Latin America, and co-authored the problems that selected high schoolers to represent Brazil in the International Olympiad of Informatics in 2018.
Data musicalization. I've been having a lot of fun in creating music from data, as a powerful way to subjectively experience information. One recent finished project on this line was a musicalization of the COVID deaths in Brazil, along with the equally disturbing reactions from our president at the time, which you can watch on YouTube.
Invited Talks
- Synchromesh: Reliable Code Generation from Pre-trained Models @ Microsoft Research, Oct 2021.
- Pragmatic Code Autocomplete: Resolving User Input Ambiguity in Context @ Microsoft Research Cambridge, Aug 2021.
- Contrastive Reinforcement Learning of Symbolic Reasoning Domains @ Google Research, Jul 2021.
- Pragmatic Code Autocomplete @ Microsoft Data+AI, Nov 2020.