66 citations · 130 across the 22 of their papers we have counts for
23 papers
Formal Disco: Scalable Open-Ended Generation of Formally Verified Programs
Gabriel Poesia, Simon Henniger, Tzu-Han Hsu +2
The cost of producing code is rapidly diminishing with increasingly capable AI agents, while quality assurance of generated programs has not kept pace. Formal verification provides…
Learning to Rank the Initial Branching Order of SAT Solvers
Arvid Eriksson, Gabriel Poesia, Roman Bresson +2
Finding good branching orders is key to solving SAT problems efficiently, but finding such branching orders is a difficult problem. Using a learning based approach to predict a goo…
The Token Games: Evaluating Language Model Reasoning with Puzzle Duels
Simon Henniger, Gabriel Poesia
Evaluating the reasoning capabilities of Large Language Models is increasingly challenging as models improve. Human curation of hard questions is highly expensive, especially in re…
A Matter of Interest: Understanding Interestingness of Math Problems in Humans and Language Models
Shubhra Mishra, Yuka Machino, Gabriel Poesia +9
The evolution of mathematics is shaped importantly by interestingness: researchers choose which problems to pursue, and students choose which problems to engage with, based on expe…
Code-enabled language models can outperform reasoning models on diverse tasks
Cedegao E. Zhang, Cédric Colas, Gabriel Poesia +2
Reasoning models (RMs), language models (LMs) trained with reinforcement learning to produce long-form natural language reasoning, have been remarkably successful, but they still r…
ProofCompass: Enhancing Specialized Provers with LLM Guidance
Nicolas Wischermann, Claudio Mayrink Verdun, Gabriel Poesia +1
Language models have become increasingly powerful tools for formal mathematical reasoning. However, most existing approaches rely exclusively on either large general-purpose models…
Automated Discovery of Tactic Libraries for Interactive Theorem Proving
Yutong Xin, Jimmy Xin, Gabriel Poesia +3
Enabling more concise and modular proofs is essential for advancing formal reasoning using interactive theorem provers (ITPs). Since many ITPs, such as Rocq and Lean, use tactic-st…
Formal Mathematical Reasoning: A New Frontier in AI
Kaiyu Yang, Gabriel Poesia, Jingxuan He +4
AI for Mathematics (AI4Math) is not only intriguing intellectually but also crucial for AI-driven discovery in science, engineering, and beyond. Extensive efforts on AI4Math have m…
Data for Mathematical Copilots: Better Ways of Presenting Proofs for Machine Learning
Simon Frieder, Jonas Bayer, Sam Looi +13
The datasets and benchmarks commonly used to train and evaluate the mathematical capabilities of AI-based mathematical copilots (primarily large language models) exhibit several sh…
dafny-annotator: AI-Assisted Verification of Dafny Programs
Gabriel Poesia, Chloe Loughridge, Nada Amin
Formal verification has the potential to drastically reduce software bugs, but its high additional cost has hindered large-scale adoption. While Dafny presents a promise to signifi…
h4rm3l: A language for Composable Jailbreak Attack Synthesis
Moussa Koulako Bala Doumbouya, Ananjan Nandi, Gabriel Poesia +5
Despite their demonstrated valuable capabilities, state-of-the-art (SOTA) widely deployed large language models (LLMs) still have the potential to cause harm to society due to the…
From Next-Token to Mathematics: The Learning Dynamics of Mathematical Reasoning in Language Models
Shubhra Mishra, Gabriel Poesia, Noah D. Goodman
Large Language Models (LLMs) solely trained on next-token prediction learn to solve a wide range of problems involving mathematical reasoning. But how does this ability evolve duri…
Learning Formal Mathematics From Intrinsic Motivation
Gabriel Poesia, David Broman, Nick Haber +1
How did humanity coax mathematics from the aether? We explore the Platonic view that mathematics can be discovered from its axioms - a game of conjecture and proof. We describe Min…
When Do Skills Help Reinforcement Learning? A Theoretical Analysis of Temporal Abstractions
Zhening Li, Gabriel Poesia, Armando Solar-Lezama
Skills are temporal abstractions that are intended to improve reinforcement learning (RL) performance through hierarchical RL. Despite our intuition about the properties of an envi…
Hypothesis Search: Inductive Reasoning with Language Models
Ruocheng Wang, Eric Zelikman, Gabriel Poesia +3
Inductive reasoning is a core problem-solving capacity: humans can identify underlying principles from a few examples, which robustly generalize to novel scenarios. Recent work eva…
Certified Deductive Reasoning with Language Models
Gabriel Poesia, Kanishk Gandhi, Eric Zelikman +1
Language models often achieve higher accuracy when reasoning step-by-step in complex tasks. However, even when arriving at a correct final answer, their rationales are often logica…
Solving Math Word Problems by Combining Language Models With Symbolic Solvers
Joy He-Yueya, Gabriel Poesia, Rose E. Wang +1
Automatically generating high-quality step-by-step solutions to math word problems has many applications in education. Recently, combining large language models (LLMs) with externa…
Parsel: Algorithmic Reasoning with Language Models by Composing Decompositions
Eric Zelikman, Qian Huang, Gabriel Poesia +2
Despite recent success in large language model (LLM) reasoning, LLMs struggle with hierarchical multi-step reasoning tasks like generating complex programs. For these tasks, humans…
Peano: Learning Formal Mathematical Reasoning
Gabriel Poesia, Noah D. Goodman
General mathematical reasoning is computationally undecidable, but humans routinely solve new problems. Moreover, discoveries developed over centuries are taught to subsequent gene…
LEMMA: Bootstrapping High-Level Mathematical Reasoning with Learned Symbolic Abstractions
Zhening Li, Gabriel Poesia, Omar Costilla-Reyes +2
Humans tame the complexity of mathematical reasoning by developing hierarchies of abstractions. With proper abstractions, solutions to hard problems can be expressed concisely, thu…
Synchromesh: Reliable code generation from pre-trained language models
Gabriel Poesia, Oleksandr Polozov, Vu Le +4
Large pre-trained language models have been used to generate code,providing a flexible interface for synthesizing programs from natural language specifications. However, they often…
Open-domain clarification question generation without question examples
Julia White, Gabriel Poesia, Robert Hawkins +2
An overarching goal of natural language processing is to enable machines to communicate seamlessly with humans. However, natural language can be ambiguous or unclear. In cases of u…
Contrastive Reinforcement Learning of Symbolic Reasoning Domains
Gabriel Poesia, WenXin Dong, Noah Goodman
Abstract symbolic reasoning, as required in domains such as mathematics and logic, is a key component of human intelligence. Solvers for these domains have important applications,…