66 citations · 130 across the 22 of their papers we have counts for
12 papers · 1 filter
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…
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…
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…
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…
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…
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…
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,…