ABEL: Sample Efficient Online Reinforcement Learning for Neural Theorem Proving

Authors: fabian  gloeckle
gabriel  synnaeve
amaury  hayat
école  des
ponts  paris
Venue: NeurIPS_cc_2024_Workshop_MATH-AI
Published: 2024-09-26 13:20:34

Abstract: We propose a scalable and efficient reinforcement learning framework as a strong baseline for theorem proving with limited data. This baseline reaches performances comparable to the current state-of-the-art in theorem proving, while only training on a few hundred examples. This a first step toward an efficient and easily reproducible combination of autoformalization, synthetic data generation and reinforcement learning, which could unlock significant advancements in neural theorem proving.

Main paper: 
 introduction: 
 Mathematical reasoning constitutes a major challenge for deep-learning models, and now a very active research area [Williamson, 2024] . Formal languages such as Isabelle [Paulson, 1994] , Coq [Barras et al., 1997] , and Lean [de Moura et al., 2015, Moura and Ullrich, 2021] have been developed to enable automatic computer verification of proofs and can now serve as grounding to prevent language model hallucinations. Several approaches relying on LLMs and formal proof search environments have recently been proposed (App. A), but were limited by the scarcity of formal training data (around 100k lemmas in Lean's central theorem library Mathlib [Mathlib Community, 2020] ) and the data inefficiency of machine learning methods. For this reason, most of the works on neural theorem proving have focused on obtaining more data, either from autoformalization or synthetic data generation [Xin et al., 2024a] .In this paper, we present ABEL, a scalable and compute efficient online reinforcement learning framework for theorem proving. This serves as a strong baseline of what is achievable with very limited data and as a first step toward a combination of online reinforcement learning and autoformalization.We show that training on only several hundred maths exercises, one can reach performances comparable to the current state-of-the-art in theorem proving. We use MiniF2F [Zheng et al., 2021] , a well-established benchmark in the field, as our primary evaluation set. Our model outperforms the cumulative performances of [Lample et al., 2022] with 13 times less compute and no synthetic data. It also reaches a new state-of-the-art on PutnamBench [Tsoukalas et al., 2024b] , a dataset of formidably challenging olympiad-like problems from the Putnam competition in North America, by solving 7 problems overall and discovering one formalization error, 4 more than the previous best [Tsoukalas et al., 2024a] . This suggests that combining our framework with autoformalization and synthetic data generation could achieve much higher levels of performance and unlock significant advancements in neural theorem proving.When approaching theorem proving as a problem of reinforcement learning, we must take care to cast the problem in a way that allows for efficient exploration and recombination of learned features. In this work, we follow the formulation of hypertree proof search (HTPS) [Lample et al., 2022] and opt for a two-fold tree structure for proof searches. An individual complete Lean proof is naturally represented as a tree, where nodes correspond to proof goals and tactics like induction transform a proof goal into a set of children, or subgoals, that jointly suffice to be shown instead (e.g. induction base and step). Proof search, on the other hand, involves applying several tactics at each node, proof success of any of which results in proof success for the parent node. Such a tree can be represented as an alternating tree of AND-joined sets of subgoals and OR-joined sets of tactic attempts, making the overall tree an AND/OR-tree or, equivalently, a "proof hypertree"1 . Our reinforcement learning system for formal theorem proving in Lean 4 [Moura and Ullrich, 2021] consists of three components: a programming interface based on Aesop [Limperg and From, 2023] to organize proof searches in Lean 4, the HTPS proof search procedure inspired by the AlphaZero expert iteration algorithm [Anthony et al., 2017 , Silver et al., 2018] and an online retraining mechanism. We will explain each component in the following paragraphs.AesopRepl: a proof search interface for Lean 4 Our Read-Eval-Print Loop (REPL), AesopRepl, makes the infrastructure of Lean's proof search automation tactic Aesop [Limperg and From, 2023] available as a command line interface. Aesop manages an AND/OR-proof tree and can receive tactic suggestions generated by a language model via the interface. It executes the tactics in their respective contexts and updates the tree, checking which goals have been resolved. Once the root node of the proof tree (i.e., the initial goal) is proved, the REPL passes the resulting proof to Lean's kernel. This guards against bugs in the applied tactics. The main benefit of using Aesop's proof tree implementation is that it allows goals with shared metavariables to be processed semi-independently, improving on GPT-f [Polu and Sutskever, 2020] and LeanDojo [Yang et al., 2023] and matching HTPS [Lample et al., 2022] . See App. J for details.Proof search with HTPS Our proof search procedure uses the AlphaZero algorithm [Silver et al., 2018] with the adaptations for hypertrees proposed by [Lample et al., 2022] . A proof search consists of several rounds, each of which has three steps: node selection, expansion and value propagation. The proof search is terminated when either a proof has been found during a round or a given node expansion budget is exceeded. In the selection phase, the tree is traversed down until a solving set of leaf nodes is found, i.e. a set of nodes which, if proven, would finish the overall proof. This means that at AND-nodes, all children are selected while at OR-nodes, we select a tactic based on the established predictor upper confidence bound for trees (PUCT) policy [Kocsis and Szepesvári, 2006 , Rosin, 2011 , Silver et al., 2017] given below. In the expansion phase, all selected nodes are expanded simultaneously, i.e. a tactic model suggests tactics and a critic model evaluates the value (likelihood of proof success) of the given proof goal. We execute the tactics eagerly in Lean in order to return from successful proof searches as early as possible. The transition dynamics T (s, a) = s ′ of Lean, where s is a state/goal and a an action/tactic, i.e. the effect of a tactic execution, are sometimes hard to model (tactics like simp involve a search procedure themselves), so we follow HTPS in using a state value critic c(s ′ ) as opposed to a state-action critic Q(s, a) in AlphaZero [Silver et al., 2018] . These critic values of expanded nodes are then propagated up the tree: each edge (s, a) maintains a visit count N (s, a) and a cumulative action value W (s, a). Each node s in the selected proof tree is assigned an update value v(s) which is defined as follows:v(s) =    1 if s is proved, c(s) if s was just expanded, γ c child of s v(c) otherwise,where γ ∈ [0, 1] is a depth penalty factor and c(s) denotes the evaluation provided by the critic model. The cumulative action value W (s, a) of each edge (s, a, s ′ ) in the selected tree is then increased by the update value v(s ′ ) of its target node, and its visit count by 1. With these quantities, we can define the PUCT selection policy:PUCT(s) = argmax a Q(s, a) + c puct • π(a | s) a ′ N (s, a ′ ) 1 + N (s, a), whereQ(s, a) = W (s,a) N (s,a) if N (s, a) > 0, c(s)otherwise is the empirical action value of the edge (s, a) and c puct is an exploration coefficient and π(a | s) is the prior of action a under our tactic model π, for which we take the product of token probabilities of each tactic sequence, renormalized to sum to one at any node. Note that in our choice of Q(s, a) = c(s) for unvisited nodes we depart from Lample et al. [2022] (who choose Q(s, a) = 1 2 ), leveraging the intuition that c(s) is trained to match the expected proof success rate when performing tree search using π, and that a is a sample from π.Following Lample et al. [2022] , instead of fixing proof search hyperparameters upfront, we sample them on a per proof attempt basis (App H).Online reinforcement learning When a proof search is terminated (because a proof has been found or the search budget is exhausted), we extract training samples for the policy and critic models for retraining. We train the policy model with supervised training using standard causal language modelling loss on all tactic samples that are part of a proof of their parent node -regardless of whether they were part of a proof of the root node (All Solved setting of Lample et al. [2022] ). This makes the tactic reinforcement learning loop a form of iterated rejection sampling.The critic model is trained with supervised training using a binary cross-entropy loss of Bernoulli variables for the classification task of provability. As the supervision target, we use Bernoulli(V (s)) with V (s) given byV (s) = W (s, a * ) N (s, a * ) ,for a node s and a * = PUCT(s). Unlike Lample et al. [2022] , we do not threshold the visit counts a N (s, a) of a node to be selected. Our distributed reinforcement learning setup comprises worker and trainer GPUs, prover threads controlling Lean AesopRepl processes as well as a centralized replay buffer and a task dispenser (App. D). We select proof tasks with prioritized sampling to favor exploration: if n i is the number of successful proof searches for problem i so far, we use a weight proportional to (n i + 1) -α for sampling problem i as the next task, where α ≥ 0 is an upsampling coefficient for hard tasks2 . We postprocess tactics to induce a distribution shift from style aimed at efficient proof presentation as pursued in Lean's Mathlib [Mathlib Community, 2020] to effective proof search (App. E). 
results: 
 We conduct experiments on challenging theorem proving datasets, showcasing the efficiency of our theorem proving system. We use Llama 3.1 base 8B [Dubey et al., 2024] as a starting point and finetune on proof step data from Mathlib [Mathlib Community, 2020] extracted with LeanDojo [Yang et al., 2023] (App. F for details). We then apply the RL training procedure described in Section 2. Our results are summarized in Table 1 .Our models' cumulative performance, while below other approaches relying on large sets of data, outperforms HTPS [Lample et al., 2022] despite using a much smaller compute budget and no synthetic data. Our models also show high pass@1 performances on the test set, which are only surpassed by DeepSeek-Prover, and achieve a new state-of-the-art on PutnamBench. This is detailed below.Table 1 : Performance of different models on MiniF2F-valid and MiniF2F-test. We compare representative methods without reinforcement learning with recent expert iteration and online reinforcement learning approaches. Numbers on MiniF2F-test are with the indicated evaluation budget given as n attempts × n expansions × n tactics . For MiniF2F-valid, we report cumulative solve rates over the course of the run where it is included in the reinforcement learning set. We convert train times to A100-days with a factor 3 for H100 to A100 performance [Databricks, 2023] trained with an additional synthetic supervised dataset of Lean problems and 54.9% without. These results required HTPS 30240 A100-hours of compute, while we need 768 H100-hours ≈ 2304 A-100-hours [Databricks, 2023] , approximately 13 times less. Halving the number of GPUs to 128, we reach a cumulative solve rate of 57.4% after 5 hours, still competitive with HTPS.A new state of the art on PutnamBench When run on a 1:1:1 mix of problems from MiniF2Fvalid, MiniF2F-test and PutnamBench [Tsoukalas et al., 2024b] , we solve 7/640 problems in the setting with provided solutions after only attempting each problem between 6 and 16 times (and with no improvements thereafter with up to 590 attempts). This improves over the previous state of the art of 4/640 solved problems [Tsoukalas et al., 2024a] held by InternLM2-StepProver [Wu et al., 2024] and obtained with 4096 attempts per problem. In a different run, our system solved another problem, bringing the total to 8/640. See App. B for the proofs, a qualitative evaluation and the cumulative solve rates on the respective datasets.We evaluate the performance of pure sampling, expert iteration [Anthony et al., 2017 , Polu et al., 2022] , and online reinforcement learning by comparing runs with model updates at different frequencies. Our findings indicate that online reinforcement learning is crucial (App. C).Stability and exploration Reinforcement learning on MiniF2F-valid -which comprises 244 problems only -presents challenges regarding stability and distributional collapse. In our online training loop, this becomes exacerbated by the fact that at least 26.6% of problems in MiniF2F can be solved by a single or a short sequence of automation tactics (among aesop, ring, linarith, nlinarith). Such proofs will be found first and could quickly flood the trainers low-quality data that lacks diversity. We remediate this issue in several ways: by setting a burn-in of 8000 training samples to discard before training, by using supervised data for 10% of training samples, by using hard negative sampling (Sect. 2) by using a large number of tactics per node and decoding parameters that favor diversity as well as carefully tuning key hyperparameters (App. I). As shown in Fig. 1 , the policy continues to explore and optimizes solved problems to shorter proofs, but we still see a slow decline in tactic diversity when problem solve rates eventually plateau. Running average of the number of steps of the most recent proof per problem, indexed by the total number of proofs found so far. Over the course of each of the five depicted runs, models "golf" proofs to more compressed versions. At the same time, the policy loses diversity: the proportion of unique tactics among the total number of tactics sampled at each expansion declines (two runs). 
conclusion: 
 We presented an online reinforcement learning method for Lean that reaches near state-of-the-art performance on theorem proving while relying only on few hundred problems in its reinforcement learning problem set. It is orders of magnitude more sample efficient than methods of comparable performance that require extensive synthetic datasets with up to millions of additional data points [Xin et al., 2024a] , and around 13 times more compute efficient than the current state-of-the-art RL method [Lample et al., 2022] .Online reinforcement learning can be tricky to stabilize but carefully tuned, complements and empowers other recent techniques such as synthetic data from large-scale autoformalization [Xin et al., 2024a] , bootstrapping chains-of-thought [Lin et al., 2024] or hybrid local-global tree search [Xin et al., 2024b] . In future work, we believe the setup should be adapted to condition the policy on the node's ancestors, i.e. on the partial proof to be completed. When deploying automated provers for theory autoformalization, additional conditioning on a human-written or language model generated informal proof is additionally required, for instance in a setting similar to Draft-Sketch-Prove [Jiang et al., 2023] .Harnessing reinforcement learning as a test-time inference technique could allow tackling challenging problems such as the International Mathematics Olympiad [DeepMind, 2024] or autoformalizing mathematical theories, where sample efficiency is the primary concern. 
 
 Appendix: Mathematics is often seen as the culmination of reasoning tasks because of its intricacy and level of abstraction. While deep-learning approaches enabled mathematical discoveries in the last few years [Davies et al., 2021 , Douglas, 2022 , Blundell et al., 2022 , Alfarano et al., 2024] , it was used merely as a tool where the reasoning is left to the human. In the recent years many neural approaches have been proposed for neural theorem proving. These include, among others, fine-tuning a language model used to guide a step-by-step proof search [Polu and Sutskever, 2020 , Polu et al., 2022 , Azerbayev et al., 2024 , Wu et al., 2024] or to generate whole proofs [First et al., 2023] ; autoformalization of natural language data to either bridge the link between language models and classical automated theorem proving tools [Jiang et al., 2023] or increase the quantity of available data for training a model [Xin et al., 2024a] ; combination of fine-tuned model and retriever to suggest relevant context from a library [Yang et al., 2023] ; reinforcement learning (RL) [Lample et al., 2022] inspired from AlphaZero [Silver et al., 2018] . Qualitatively evaluating the last proofs found by the model, we observe: One statement had a formalization mistake, rendering the problem trivial. Other problems were easy compared to other Putnam problems because the solution was provided. In all cases, our model relies heavily on Lean's automation tools simp, ring, omega, nlinarith, linarith, but provides arguments and data without which the automation would not succeed (a classic pattern in idiomatic Lean proofs).1 theorem putnam_1988_b1 2 : ∀ a ≥ 2, ∀ b ≥ 2, ∃ x y z : Z, x > 0 ∧ y > 0 ∧ z > 0 ∧Cumulative solve rates on the three datasets used in the runs are reported in Table 2 . We compare runs with online model updates every 50 training steps, to a setting resembling batch reinforcement learning or expert iteration (as used in [Polu et al., 2022 , Xin et al., 2024a] ) with updates every 500 steps and a pure supervised model solving benchmark problems without any retraining. Figure 2 shows the cumulative proof rates on MiniF2F-valid for the respective runs each using 56 workers and 8 trainers (if applicable). The online reinforcement run clearly outperforms the others. Note that in our final runs, we update the weights even more frequently, namely every 10 steps. Our distributed setup comprises worker GPUs for language model inference, trainer GPUs for language model training and prover CPU threads orchestrating proof searches and controlling Lean AesopRepl processes. In our experiments, we assign 10 prover threads to each worker GPU, enabling stable generation inference workloads in our GPU-bound setup. A central service distributes proof tasks according to the hard negative sampling policy described in Sect. 2. Workers send their tactic and critic training samples to a centralized replay buffer which distributes them to the trainers, prioritizing samples seen fewer times and from more recent model generations. Unlike [Lample et al., 2022] , we do not parallelize within individual tree searches but only at the level of proof attempts (i.e. we apply node selection and expansion sequentially rather than asynchronously).To remediate this distribution discrepancy between proof search and proof presentation, we add post-processing to the tactics generated by the policy model. This facilitates distribution shift toward a better proof search policy: we turn simp only into simp, add a single-rule rewrite with the first rule for each multi-rule rewrite and deduplicate simp lemmas to break model repetitions.For supervised finetuning on the proof step dataset extracted from Mathlib (see App. L), we train with a peak learning rate of 10 -4 and a total batch size of 16k tokens using a block-causal attention mask that does not split sequences. We use the Adam optimizer [Kingma and Ba, 2015] with decoupled weight decay [Loshchilov and Hutter, 2019] with a peak learning rate of 10 -4 , β 1 = 0.9, β 2 = 0.95 and L 2 weight decay coefficient 0.1. We schedule the learning rate with cosine decay [Loshchilov and Hutter, 2017] over 5000 steps to a final learning rate of 10 -6 .reinforcement learning [Silver et al., 2018] . With our joint inference mechanism, we can, moreover, leverage existing autoregressive language model generation pipelines at the expense of a single additional token.As an additional inference speed optimization, we compute the key-value cache of the (typically long) prompt only once during the "pre-fill phase" before copying it as many times as we would like to decode independent tactic suggestions. Using this method, we observed a 2-3x inference speedup.We stop decoding at a special stop token between the "tactic:" and the "result:" field not shown above.Following Lample et al. [2022] , we sample the decoding and proof search hyperparameters before each proof search as follows:• temperature for nucleus sampling [Holtzman et al., 2020] Unlike HTPS, we always sample 64 tactics per node expansion with the understanding that tactic decoding is fast compared to the encoding (kv-cache pre-fill) of the proof state prompt. 3 .The replay buffer uses the following selection and eviction policy: it sorts samples by the smallest number of times they have already been sent to the trainers, then by the most recent model version they come from, and randomly for ties, and sends them by increasing priority. Samples are evicted from the buffer if they have been sent a certain maximum number of times or if the buffer has reached its maximum capacity, the sample has been sent at least once and it is lowest in the buffer's priority ordering.Aesop's proof tree implementation is very similar to that HTPS [Lample et al., 2022] , with one exception concerning the handling of shared metavariables. These are Lean constructs representing objects that will be filled in during the proof. For example, a transitivity tactic might reduce the goal ⊢ 1 < 3 to two goals ⊢ 1 < ?x and ⊢ ?x < 3, where the metavariable ?x stands for a number to be determined later. Another tactic application could then solve the first goal for ?x = 2, at which point ?x is replaced with 2 in the second goal as well.The example demonstrates the central issue with metavariables: If the proof of the first goal had assigned ?x = 4, the second goal would have become unprovable. In other words, the possible proofs of the second goal depend on which proof was chosen for the first goal (or vice versa); the goals are no longer independent. But independence of goals is a central assumption underlying the hypertree proof search model.GPT-f [Polu and Sutskever, 2020] and LeanDojo [Yang et al., 2023] address this issue by operating on tactic states, i.e. lists of goals. However, this reduces parallelism and leads to duplicate work since the same goal may have to be proved in multiple tactic states. HTPS refines the GPT-f approach by using tactic states (with more than one goal) only when goals are, in fact, coupled by a shared metavariable. Aesop goes even further and treats coupled goals as independent, but when a metavariable is assigned, Aesop makes a copy of any goals affected by this assignment [Limperg and From, 2023, Sec. 4 ].Hence, the doomed proof attempt that sets ?x = 4 does not prevent a later successful proof attempt with ?x = 2.Compared with HTPS, Aesop's approach may enable future optimisations that transfer a tactic application from a goal to its copies if the tactic application is independent of any specific metavariable assignment. This would reduce the amount of effort spent during proof search on applying the same tactics to goals that differ only in their metavariable assignments. Unlike [Lample et al., 2022] , we do not currently attempt to merge duplicate goals.In Table 1 , we include representative methods without reinforcement learning (classical solvers, pretrained models with few-shot prompting, supervised finetuning) and recent reinforcement learning approaches.Lean automation refers to a small search using the following Lean tactics: aesop, ring, linarith and nlinarith.ReProver [Yang et al., 2023 ] is a language model coupled with a premise retrieval model which was trained on supervised data extracted from Mathlib.Llemma-7b [Azerbayev et al., 2024] is a model based on CodeLlama [Rozière et al., 2023] that was trained on formal and informal mathematical data extacted from the web [Paster et al., 2023] .We do not include InternLM2-StepProver [Wu et al., 2024] which reaches 48.8% on MiniF2F-test with a budget of 1 × 100 × 32 and 63.9% on MiniF2F-valid, but whose data collection raises concerns about data contamination. For instance, the Lean 3 MiniF2F dataset at https://github.com/ facebookresearch/miniF2F contains solutions.DeepSeek-Prover [Xin et al., 2024a] and DeepSeek-Prover-1.5 [Xin et al., 2024b] do not report the total amount of compute used for developing their models. Based on the large numbers of problems in their reinforcement learning set, expensive evaluation settings of up to pass@65536 and the large number of models and methods reported in the publications , we expect it to be significantly larger than for the other models in the comparison. We also note that while all other models in the comparison are sized between 600M parameters (HTPS) and 8B parameters (ours), DeepSeek-Prover also uses sequence distillation from a 236B parameter model.DeepSeek-Prover uses 8M autoformalized problems in its reinforcement learning set. DeepSeek-Prover-1.5 adds MiniF2F-valid (244 problems), ProofNet-valid [Azerbayev et al., 2023] (185 problems) and Lean Workbook [Ying et al., 2024] (57k problems, or 140k including "Workbook Plus").GPT-f [Polu et al., 2022] uses MiniF2F-curriculum instead of MiniF2F-valid in the reinforcement learning set. The reported number on MiniF2F-valid is hence an evaluation number with the same budget as the number on MiniF2F-test, not a cumulative one.HTPS [Lample et al., 2022] samples the number of tactics sampled at each node uniformly from {8, 16, 32, 48}, with an average of 26, which we report in the table. (Note however, that for pass@64, the maxmum may be more relevant than the average.)Both GPT-f and HTPS additionally use synthetically generated data. GPT-f generates 5600 problems without proof as reinforcement learning tasks. HTPS generates problems including proofs, and uses the data as an additional supervised dataset instead.38th Conference on Neural Information Processing Systems (NeurIPS 2024).when considering the set of children of a tactic's child AND-node the collective target of a hyperedgeα = 0 reduces to uniform sampling, α = +∞ to uniform sampling among least often solved problems 



Reviews: review: title: title: A Scalable and Efficient Reinforcement Learning Framework
main_review: main_review: This paper proposes a scalable and efficient reinforcement learning framework for neural theorem proving. The authors present ABEL, a system that achieves comparable performance to state-of-the-art methods while using significantly less data and computational resources. The framework use online reinforcement learning to improve data efficiency in mathematical reasoning tasks.

## Pros:
1. High data efficiency: The system achieves performance comparable to current state-of-the-art methods using only a few hundred mathematical exercises. This represents a significant advancement in sample efficiency for neural theorem proving.
2. Computational efficiency: Compared to HTPS, the proposed method reduces computational requirements by a factor of 13 while slightly improving performance. This is an impressive result that could make advanced theorem-proving systems more accessible and practical.

## Cons:
1. The paper's writing and structure need improvement. After reading the entire article, the system architecture and algorithm usage remain unclear. The absence of a clear system architecture diagram or algorithm examples, hinders full comprehension. While it's evident that the authors conducted numerous experiments, the paper would benefit from a high-level summary analyzing more about which components contribute most significantly to the impressive results.
2. The code is not open-sourced, which limits reproducibility and further exploration by the research community.
title: title: Efficient Reinforcement Learning for Theorem Proving: A Promising Approach with Room for Improvement
main_review: main_review: This paper introduces a robust baseline for reinforcement learning (RL) applied to theorem proving, achieving state-of-the-art performance while utilizing fewer training samples.

Pros:

The paper proposes a proof search algorithm that adapts the AlphaZero framework, presenting a novel approach within the domain of automated theorem proving. This innovation stands out as a key contribution.

The experimental results are compelling. The proposed algorithm significantly outperforms HTPS, requiring 13x less computational resources and establishing a new state of the art on the PutnamBench benchmark. This efficiency in both computation and performance is highly noteworthy.

Cons:

However, from the results in Table 1, the proposed method still falls short when compared to DeepSeek-Prover in terms of overall performance. It would be valuable to explore strategies for reducing the training samples required by DeepSeek-Prover, which could enhance its applicability and competitiveness in the field.
title: title: ABEL is a scalable and sample-efficient online reinforcement learning framework for theorem proving in Lean 4. It outperforms prior approaches while using significantly less compute and data. ABEL achieves a new state-of-the-art on the challenging PutnamBench dataset and opens promising directions for combining RL with auto-formalization and synthetic data generation.
main_review: main_review: The authors propose ABEL, a scalable and efficient online reinforcement learning framework for theorem proving in Lean 4. ABEL incorporates several key features, including efficient online RL using hypertree proof search (HTPS) and AlphaZero-style tree search, an interface layer (AesopRepl) between the RL system and Lean's Aesop automation system, optimizations for critic and policy training to improve sample efficiency and exploration, and a distributed RL setup for scalability. Experiments demonstrate that ABEL outperforms prior HTPS results with 13x less compute and no synthetic data. Furthermore, it achieves a new state-of-the-art on the challenging PutnamBench dataset.

Pros
- ABEL achieves competitive theorem-proving performance with orders of magnitude better sample efficiency than prior work.
- The paper introduces a scalable online RL setup tailored specifically for theorem proving, enabling rapid iterations and improvements.
- Several interesting technical innovations are presented around stabilizing online RL, such as hard negative sampling, burn-in, rehearsal, and tactic post-processing.
- The empirical results are strong, including establishing a new state-of-the-art on the difficult PutnamBench benchmark.
This work opens up promising new research directions around combining RL with auto-formalization and synthetic data generation to advance theorem-proving capabilities.

Cons
- The empirical evaluation is somewhat limited in scope, focusing primarily on the MiniF2F and PutnamBench datasets. Broader evaluation on additional datasets would strengthen the claims. This is not a major concern, given the scope of a workshop.
- While the authors provide some comparison to existing systems, the comparative analysis could be more comprehensive and detailed. However, the authors acknowledge the challenges in making apples-to-apples comparisons given the differences in datasets and compute resources.
- The inclusion of ablation studies or a deeper analysis of the key design choices and hyperparameters would help disentangle the impact of various components and strengthen the technical contributions.
title: title: Review of ABEL
main_review: main_review: Pros: The paper presents ABEL, an innovative reinforcement learning framework aimed at addressing the challenges of neural theorem proving with a strong emphasis on sample and computational efficiency. ABEL integrates hypertree proof search (HTPS) with online reinforcement learning techniques, drawing inspiration from the AlphaZero algorithm to deliver high performance on formal mathematics tasks. Key aspects of ABEL include a proof tree structure that enables efficient proof searches and an online retraining mechanism that continuously enhances model performance with new data. ABEL requires significantly fewer training examples than existing state-of-the-art models, making it a strong baseline for formal theorem proving tasks.

Cons: The experiments are conducted using only one model and a single setting, which limits the ability to demonstrate the generalizability and overall effectiveness of the proposed method
title: title: An Incremetnal Work of HTPS
main_review: main_review: The paper presents ABEL, a reinforcement learning framework designed for formal theorem proving that builds upon the previous work of HTPS. ABEL incorporates more advanced language models and is trained on the latest datasets, LeanDojo. Experimental results demonstrate that ABEL outperforms several state-of-the-art baselines, including DeepSeek Prover, GPT-f, and HTPS on the miniF2F and PutnamBench benchmarks.

The paper is well-written and easy to follow. While many core techniques (e.g., hypertree proof search, online training) are inherited from HTPS, ABEL integrates a better fine-tuned LLM and a relatively smaller real-world dataset within its reinforcement learning loop. This allows ABEL to surpass HTPS in cumulative performance, achieving these results with less computational overhead and without relying on synthetic data.

Minor: Reference 18 in the appendix has a missing author name (shown as `author?`).