Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving
Reasoning remains a challenging task for large language models (LLMs), especially within the logically constrained environment of automated theorem proving (ATP), due to sparse rewards and the vast scale of proofs. These challenges are amplified in benchmarks like PutnamBench, which contains university-level problems requiring complex, multi-step reasoning. To address this, we introduce self-generated goal-conditioned MDPs (sG-MDPs), a new framework in which agents generate and pursue their subgoals based on the evolving proof state. Given this more structured generation of goals, the resulting problem becomes more amenable to search. We then apply Monte Carlo Tree Search (MCTS)-like algorithms to solve the sG-MDP, instantiating our approach in Bourbaki (7B), a modular system that can ensemble multiple 7B LLMs for subgoal generation and tactic synthesis. On PutnamBench, Bourbaki (7B) solves 26 problems, achieving new state-of-the-art results with models at this scale.
Code (0)
등록된 구현이 없습니다.
Tasks
Automated Theorem ProvingSimilar Papers 제목 키워드 기반
Learning Domain Invariant Representations in Goal-conditioned Block MDPs
Deep Reinforcement Learning (RL) is successful in solving many complex Markov Decision Processes (MDPs) problems. However, agents often face unanticipated environmental changes after deployment in the real world. These c…
Deep Reinforcement LearningDomain GeneralizationReinforcement Learning (RL)Rethinking Goal-conditioned Supervised Learning and Its Connection to Offline RL
Solving goal-conditioned tasks with sparse rewards using self-supervised learning is promising because of its simplicity and stability over current reinforcement learning (RL) algorithms. A recent work, called Goal-Condi…
Offline RLReinforcement Learning (RL)Self-Supervised LearningA tale of two goals: leveraging sequentiality in multi-goal scenarios
Several hierarchical reinforcement learning methods leverage planning to create a graph or sequences of intermediate goals, guiding a lower-level goal-conditioned (GC) policy to reach some final goals. The low-level poli…
Hierarchical Reinforcement LearningAbstraction for Offline Goal-Conditioned Reinforcement Learning
Markov Decision Processes (MDPs) often exhibit significant redundancy due to symmetries and shared structure across state-goal pairs in real-world Goal-Conditioned Reinforcement Learning (GCRL). While hierarchical polici…
Reinforcement LearningFirst-Order Representation Languages for Goal-Conditioned RL
First-order relational languages have been used in MDP planning and reinforcement learning (RL) for two main purposes: specifying MDPs in compact form, and representing and learning policies that are general and not tied…
Reinforcement Learning