SubgoalXL: Subgoal-based Expert Learning for Theorem Proving

## Abstract

Abstract Formal theorem proving, a field at the intersection of mathematics and computer science, has seen renewed interest with advancements in large language models (LLMs). This paper introduces 𝚂𝚞𝚋𝚐𝚘𝚊𝚕𝚇𝙻 𝚂𝚞𝚋𝚐𝚘𝚊𝚕𝚇𝙻 \mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{%
X}\mathtt{L} typewriter_SubgoalXL , a novel approach that synergizes subgoal-based proofs with expert learning to enhance LLMs’ capabilities in formal theorem proving within the Isabelle environment. 𝚂𝚞𝚋𝚐𝚘𝚊𝚕𝚇𝙻 𝚂𝚞𝚋𝚐𝚘𝚊𝚕𝚇𝙻 \mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{%
X}\mathtt{L} typewriter_SubgoalXL addresses two critical challenges: the scarcity of specialized mathematics and theorem-proving data, and the need for improved multi-step reasoning abilities in LLMs. By optimizing data efficiency and employing subgoal-level supervision, 𝚂𝚞𝚋𝚐𝚘𝚊𝚕𝚇𝙻 𝚂𝚞𝚋𝚐𝚘𝚊𝚕𝚇𝙻 \mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{%
X}\mathtt{L} typewriter_SubgoalXL extracts richer information from limited human-generated proofs. The framework integrates subgoal-oriented proof strategies with an expert learning system, iteratively refining formal statement, proof, and subgoal generators. Leveraging the Isabelle environment’s advantages in subgoal-based proofs, 𝚂𝚞𝚋𝚐𝚘𝚊𝚕𝚇𝙻 𝚂𝚞𝚋𝚐𝚘𝚊𝚕𝚇𝙻 \mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{%
X}\mathtt{L} typewriter_SubgoalXL achieves a new state-of-the-art performance of 56.1% in Isabelle on the standard miniF2F dataset, marking an absolute improvement of 4.9%. Notably, 𝚂𝚞𝚋𝚐𝚘𝚊𝚕𝚇𝙻 𝚂𝚞𝚋𝚐𝚘𝚊𝚕𝚇𝙻 \mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{%
X}\mathtt{L} typewriter_SubgoalXL successfully solves 41 AMC12, 9 AIME, and 3 IMO problems from miniF2F. These results underscore the effectiveness of maximizing limited data utility and employing targeted guidance for complex reasoning in formal theorem proving, contributing to the ongoing advancement of AI reasoning capabilities. The implementation is available at https://github.com/zhaoxlpku/SubgoalXL .

## 1 Introduction

Formal theorem proving, a field at the intersection of mathematics and computer science, has flourished alongside the development of languages like Lean (de Moura et al., ) and Isabelle (Paulson, ). These two prominent communities have been instrumental in advancing the field’s core challenge: mechanizing mathematical reasoning and proof verification (Li et al., ). Through the creation of rigorously verified proofs, this discipline strengthens the foundations of mathematical certainty, potentially opening doors to new mathematical discoveries.

The field has recently garnered renewed attention, driven by advancements in artificial intelligence, particularly in large language models (LLMs). The significance of this resurgence lies in its potential to push the boundaries of reasoning capabilities in modern AI methods, especially LLMs (Wu et al., ; Jiang et al., ; Zhao et al., ; Xin et al., ; Lin et al., ). Formal theorem proving represents a new frontier in AI reasoning, challenging LLMs to perform complex, logically rigorous tasks that were previously considered beyond their capabilities. From an application perspective, this breakthrough in language models’ ability to engage in sophisticated mathematical reasoning has profound implications that reach far beyond pure mathematics, extending to various fields of scientific research and automated decision-making systems.

In this work, we introduce $\mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{
X}\mathtt{L}$ (Figure 1), a novel approach that synergizes subgoal-based proofs with expert learning to enhance LLMs’ capabilities in formal theorem proving. $\mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{
X}\mathtt{L}$ tackles the scarcity of specialized mathematics and theorem proving data (Lin et al., ; Wu et al., ) by optimizing data efficiency, extracting richer information from limited human-generated proofs. Concurrently, it augments LLMs’ multi-step reasoning abilities through subgoal-level supervision. At its core, $\mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{
X}\mathtt{L}$ integrates subgoal-oriented proof strategies with an expert learning framework, iteratively refining formal statement, proof, and subgoal generators. By leveraging sampling from estimated optimal distributions, $\mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{
X}\mathtt{L}$ significantly elevates LLMs’ performance in theorem-proving tasks, enhancing their capacity to navigate intricate logical structures and generate more robust and precise formal proofs.

Leveraging the Isabelle environment’s advantages in subgoal-based proofs, $\mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{
X}\mathtt{L}$ significantly advances theorem-proving capabilities. It achieves a new state-of-the-art performance of 56.1% in Isabelle on the standard miniF2F dataset (Zheng et al., ), an absolute improvement of 4.9% over Zheng et al. (). $\mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{
X}\mathtt{L}$ successfully solves 41 AMC12, 9 AIME, and 3 IMO problems from miniF2F. The iterative expert learning process drives steady performance gains, underscoring $\mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{
X}\mathtt{L}$’s robustness and effectiveness. These results highlight the critical role of maximizing limited data utility and employing effective guidance for complex reasoning, complementing large-scale data efforts (Wu et al., ; Xin et al., ; ).

Figure: (a) Subgoal-based Proof
Refer to caption: x1.png

## 2 Related Work

Formal theorem proving has advanced significantly through machine learning, focusing on enhancing proof search strategies and leveraging Large Language Models (LLMs) for autoformalization Polu & Sutskever (); Polu et al. (); Jiang et al. (). Improvements in the proof search include self-supervised strategies in Expert Iteration (Polu et al., ) and PACT (Han et al., ), integrations of language models with automated provers in HyperTree Proof Search (HTPS)(Lample et al., ) and Thor(Jiang et al., ), and transformer-based premise selection in Magnushammer (Mikuła et al., ). Despite these advancements, scalability remains a challenge due to the increasing complexity of theorems. The application of LLMs for autoformalization and proof generation has also been explored, with Wu et al. () and Jiang et al. () demonstrating the conversion of mathematical problems into formal specifications. Baldur (First et al., ) further enhances proving capabilities by producing full proofs and incorporating a proof repair model. Additionally, LEGO-Prover (Xin et al., ) and Lyra Zheng et al. () contribute uniquely to theorem proving by focusing on the incremental development of reusable theorems and integrating error messages from external verifiers for proof post-processing, respectively. DeepSeek-Prover (Xin et al., ) highlights the potential of large-scale synthetic data, while Lean-STaR (Lin et al., ) leverages informal information to boost theorem-proving capabilities by training language models to produce informal thoughts before each proof step. InternLM2-StepProver (Wu et al., ) addresses data scarcity by utilizing extensive formal data from Lean 4 repositories on GitHub. Zhao et al. () introduce a subgoal-based demonstration learning framework that constructs and refines distinct subgoals for each example, significantly enhancing proof search efficiency in LLMs.

Nevertheless, challenges remain in addressing data scarcity and enhancing deep, multi-step reasoning in formal theorem proving. Building upon the insights from subgoal-based demonstration learning (Zhao et al., ), we introduce $\mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{
X}\mathtt{L}$, a novel framework that combines subgoal-based proofs with an expert learning system. This approach iteratively enhances formal statement, proof, and subgoal generation, aiming to improve data efficiency and achieve robust performance. $\mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{
X}\mathtt{L}$ complements existing methods by focusing on maximizing the utility of limited data and refining complex reasoning strategies.

## 3 Approach

### 3.1 Problem Formalization

Suppose we have an informal dataset $\mathcal{I}=\{(\mathcal{s}_{i}^{\mathcal{I}},\mathcal{p}_{i}^{\mathcal{I}})\}_
{i=1}^{|\mathcal{I}|}$, where $\mathcal{s}_{i}^{\mathcal{I}}$ is an informal statement and $\mathcal{p}_{i}^{\mathcal{I}}$ is an informal proof. Similarly, we have a formal dataset $\mathcal{F}=\{(\mathcal{S}_{i}^{\mathcal{F}},\mathcal{P}_{i}^{\mathcal{F}})\}_
{i=1}^{|\mathcal{F}|}$, where $\mathcal{S}_{i}^{\mathcal{F}}$ is a formal statement and $\mathcal{P}_{i}^{\mathcal{F}}$ is a formal proof. The goal is to train a language model $p_{\text{fpg}}(\mathcal{p},\mathcal{P}\mid\mathcal{s},\mathcal{S})$ using both $\mathcal{I}$ and $\mathcal{F}$. Consequently, given a new informal statement $\mathcal{s}$ and its formal version $\mathcal{S}$, the model can generate both the informal proof $\mathcal{p}$ and the formal proof $\mathcal{P}$, following the distribution $p_{\text{fpg}}(\mathcal{p},\mathcal{P}\mid\mathcal{s},\mathcal{S})$. In this paper, we treat $(\mathcal{p},\mathcal{P})$ as a sequence of language tokens, with $\mathcal{p}$ representing the prefix and $\mathcal{P}$ representing the suffix. In cases where an informal proof $\mathcal{p}$ is available, the model can directly generate the formal proof $\mathcal{P}$ following $p_{\text{fpg}}(\mathcal{P}\mid\mathcal{s},\mathcal{S},\mathcal{p})$.

The challenges mainly lie in (1) the limited effectiveness of informal proofs in $\mathcal{I}$ due to discrepancies between human-written informal proofs and the established practices of formal proofs in theorem-proving languages; and (2) the difficulty in constructing the full training dataset, which requires aligned $(\mathcal{s},\mathcal{S},\mathcal{p},\mathcal{P})$ quadruples. Inspired by Zhao et al. (), we use subgoal-based proofs (Figure 1(a)) to replace informal proofs in $\mathcal{I}$, achieving better consistency with the structure of formal proofs (see §3.2). Additionally, we develop an expert learning framework (Figure 1(b)) that samples $(\mathcal{s},\mathcal{S},\mathcal{p},\mathcal{P})$ quadruples by estimating their optimal distributions through iterative refinement, leveraging probabilistic modeling and gradient estimation techniques (see §3.3).

### 3.2 Subgoal-based Proof

To annotate subgoal-based proofs for the informal statements in $\mathcal{I}$, we begin by manually creating demonstration examples to serve as input for in-context learning (see Figure 1(a)). We select a subset of problems from the miniF2F validation set and manually construct the verified formal proof for each problem. Then, we prompt GPT-4o to generate subgoal-based proofs $\mathcal{g}$, conditioned on the informal statement $\mathcal{s}$, formal statement $\mathcal{S}$, and formal proof $\mathcal{P}$. This process ensures that: (1) the subgoal-based proofs are produced by autoregressive models; (2) they exhibit a consistent style, reducing the learning burden, as noted by Gu et al. (); and (3) each subgoal corresponds to a corresponding formal intermediate goal in Isabelle. These demonstrations are then used as in-context examples to annotate subgoal-based proofs for the informal statements in $\mathcal{I}$ (see Appendix A for further details).

### 3.3 Subgoal-based Expert Learning

We introduce the $\mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{
X}\mathtt{L}$ framework, which comprises a formal proof generator ($p_{\text{fpg}}$), a formal statement generator ($p_{\text{fsg}}$), and a subgoal generator ($p_{\text{sg}}$). Inspired by gradient estimation in probabilistic modeling (Schulman et al., ), this framework estimates optimal training data distributions for each component and iteratively refines these components by fine-tuning on data sampled from the respective distributions.(^1^11We do not include an iterative bootstrapping process for an informal statement generator, as generating informal statements from formal statements is significantly less challenging than the other three tasks. Instead, we annotate the informal statements for each formal statement in the formal dataset using in-context learning. The prompt template can be found in Appendix B.2.) The overall algorithm is presented in Algorithm 1.

#### Components.

The core components include a formal statement generator, a formal proof generator, and a subgoal generator. The formal statement generator annotates formal statements for informal ones in $\mathcal{I}$ following $p_{\text{fsg}}(\mathcal{S}\mid\mathcal{s})$. Subsequently, the formal proof generator produces formal proofs for the informal data in $\mathcal{I}$, based on $p_{\text{fpg}}(\mathcal{P}\mid\mathcal{s},\mathcal{S},\mathcal{g})$ and using subgoal-based proofs (see §3.2). The subgoal generator labels subgoal-based proofs for formal data in $\mathcal{F}$ according to $p_{\text{sg}}(\mathcal{g}\mid\mathcal{s},\mathcal{S})$ after informal statements have been generated for each data point in $\mathcal{F}$ (refer to Appendix B.2 for details).

Additionally, the formal proof generator assesses the performance of the subgoal generator by evaluating the likelihood of reconstructing formal proofs in $\mathcal{F}$. Conversely, the subgoal generator evaluates the formal statement generator by assessing the likelihood of reconstructing subgoal-based proofs in $\mathcal{I}$. We also introduce an auxiliary component, the posterior subgoal generator $p_{\text{psg}}(\mathcal{g}\mid\mathcal{s},\mathcal{S},\mathcal{P})$, which evaluates the formal proof generator based on the likelihood of reconstructing subgoal-based proofs in $\mathcal{I}$. The formal statement generator, formal proof generator, and subgoal generator iteratively improve through expert learning, with only the formal proof generator used during testing.

#### Initialization.

We begin by annotating the formal statements and proofs for the informal dataset $\mathcal{I}$ using in-context learning, retaining only those verified by Isabelle. Next, we annotate the informal statements and proofs for the formal dataset $\mathcal{F}$ in the same manner. The initial formal proof generator, denoted as $p_{\text{fpg}}^{(0)}$, is then trained on $\{(\mathcal{s}_{i}^{\mathcal{I}},\mathcal{S}_{i}^{\mathcal{I}},\mathcal{g}_{i}
^{\mathcal{I}},\mathcal{P}_{i}^{\mathcal{I}})\}_{i=1}^{|\mathcal{I}|}\cup\{(
\mathcal{s}_{i}^{\mathcal{F}},\mathcal{S}_{i}^{\mathcal{F}},\mathcal{p}_{i}^{
\mathcal{F}},\mathcal{P}_{i}^{\mathcal{F}})\}_{i=1}^{|\mathcal{F}|}$. Similarly, the formal statement generator $p_{\text{fsg}}^{(0)}$ and subgoal generator $p_{\text{sg}}^{(0)}$ are trained on $\{(\mathcal{s}_{i}^{\mathcal{I}},\mathcal{S}_{i}^{\mathcal{I}})\}_{i=1}^{|
\mathcal{I}|}\cup\{(\mathcal{s}_{i}^{\mathcal{F}},\mathcal{S}_{i}^{\mathcal{F}
})\}_{i=1}^{|\mathcal{F}|}$ and $\{(\mathcal{s}_{i}^{\mathcal{I}},\mathcal{S}_{i}^{\mathcal{I}},\mathcal{g}_{i}
^{\mathcal{I}})\}_{i=1}^{|\mathcal{I}|}\cup\{(\mathcal{s}_{i}^{\mathcal{F}},
\mathcal{S}_{i}^{\mathcal{F}},\mathcal{p}_{i}^{\mathcal{F}})\}_{i=1}^{|
\mathcal{F}|}$, respectively.

For training the posterior subgoal generator $p_{\text{psg}}$, we first obtain a version of the formal proof with all in-line comments removed, denoted as $\overline{\mathcal{P}}$. This component is trained on $\{(\mathcal{s}_{i}^{\mathcal{I}},\mathcal{S}_{i}^{\mathcal{I}},\overline{
\mathcal{P}}_{i}^{\mathcal{I}},\mathcal{g}_{i}^{\mathcal{I}})\}_{i=1}^{|
\mathcal{I}|}\cup\{(\mathcal{s}_{i}^{\mathcal{F}},\mathcal{S}_{i}^{\mathcal{F}
},\overline{\mathcal{P}}_{i}^{\mathcal{F}},\mathcal{p}_{i}^{\mathcal{F}})\}_{i
=1}^{|\mathcal{F}|}$. The posterior subgoal generator remains fixed during the expert learning process.

#### Expert Learning.

Given the uncertainty in the quality of generated statements and proofs, we employ probabilistic modeling to compute the reward for each component. This allows us to derive the optimal distribution from which we sample statements and proofs in each iteration. For instance, in training the formal proof generator, the optimization objective in the $k$-th iteration is:

$$ $\max_{p}\mathbb{E}_{(\mathcal{S},\mathcal{P})\sim p}[\log p_{\text{psg}}( \mathcal{g}\mid\mathcal{s},\mathcal{S},\overline{\mathcal{P}})]-\beta\mathbb{D }_{\text{KL}}[p(\mathcal{S},\mathcal{P}\mid\mathcal{s},\mathcal{g})\|p^{(k-1)} (\mathcal{S},\mathcal{P}\mid\mathcal{s},\mathcal{g})],$ (1) $$

where $p(\mathcal{S},\mathcal{P}\mid\mathcal{s},\mathcal{g})=p_{\text{fpg}}(\mathcal{
P}\mid\mathcal{s},\mathcal{S},\mathcal{g})p_{\text{fsg}}(\mathcal{S}\mid
\mathcal{s})$ and $\log p_{\text{psg}}(\mathcal{g}\mid\mathcal{s},\mathcal{S},\overline{\mathcal{
P}})$ represents the reward which is derived using gradient estimators (Schulman et al., ).
Intuitively, within the informal dataset, the formal statement and proof are treated as random variables, with optimal selections maximizing the likelihood of reconstructing the informal proof or subgoal-based proof. We also include KL-constraint terms to prevent overoptimization towards the reward. The optimal distribution of the formal proof is given by:

$$ $p^{\star}(\mathcal{S},\mathcal{P}\mid\mathcal{s},\mathcal{g})=\frac{1}{Z( \mathcal{s},\mathcal{g})}p^{(k-1)}(\mathcal{S},\mathcal{P}\mid\mathcal{s}, \mathcal{g})\exp\left(\frac{1}{\beta}\left(\log p_{\text{psg}}(\mathcal{g}\mid \mathcal{s},\mathcal{S},\overline{\mathcal{P}})\right)\right),$ (2) $$

where $Z(\mathcal{s},\mathcal{g})=\sum_{\mathcal{S},\mathcal{P}}p^{(k-1)}(\mathcal{S}
,\mathcal{P}\mid\mathcal{s},\mathcal{g})\exp\left(\frac{1}{\beta}\left(\log p_
{\text{psg}}(\mathcal{g}\mid\mathcal{s},\mathcal{S},\overline{\mathcal{P}})
\right)\right)$.
The optimal distributions for formal statements $p_{\text{fsg}}^{\star}(\mathcal{S}\mid\mathcal{s})$ and subgoal-based proofs $p_{\text{sg}}^{\star}(\mathcal{g}\mid\mathcal{s},\mathcal{S})$ follow a similar pattern, as detailed in Appendix B.3.

Let $\hat{\mathcal{S}}^{(k)}$ and $(\tilde{\mathcal{S}}^{(k)},\tilde{\mathcal{P}}^{(k)})$ be drawn from the distributions $p_{\text{fsg}}^{\star}(\mathcal{S}\mid\mathcal{s})$ and $p^{\star}(\mathcal{S},\mathcal{P}\mid\mathcal{s},\mathcal{g})$, respectively, for the informal dataset. Similarly, let $\mathcal{g}^{(k)}$ be drawn from the distribution $p_{\text{sg}}^{\star}(\mathcal{g}\mid\mathcal{s},\mathcal{S})$ for the formal dataset. In the $k$-th iteration, the formal statement generator updates with samples from $\{(\mathcal{s},\hat{\mathcal{S}}^{(k)})\}$, while the formal proof generator is trained on $\{(\mathcal{s},\tilde{\mathcal{S}}^{(k)},\mathcal{g},\tilde{\mathcal{P}}^{(k)}
)\}\cup\{(\mathcal{s},\mathcal{S},\mathcal{g}^{(k)},\mathcal{P})\}$. Simultaneously, the subgoal generator refines its parameters using $\{(\mathcal{s},\hat{\mathcal{S}},\mathcal{g}^{(k)})\}$. These updates are augmented by the corresponding training data generated during the initialization phase, contributing to increased data diversity and model robustness throughout training.

#### Diversity Efforts.

We employ various strategies to enhance the diversity of model outputs, thereby improving the efficiency of the search process.
(1) During the initialization phase, we train four distinct language models for the formal proof generator. These models are derived from combinations of two prompt templates (see Appendix B.1) and two proof lengths. For the proof lengths, one model retains the entire dataset, while the other selectively excludes shorter proofs based on indicators drawn from Bernoulli distributions. (^2^22For formal proofs with lengths $1$, $2$, and $3$, the drop rates are $0.8$, $0.6$, and $0.4$, respectively.) (2) In each iteration of the expert learning phase, we reinitialize the components from the Llama-3-8B rather than from the previous iteration’s checkpoints.

Figure: Algorithm 1 Subgoal-based Expert Learning

## 4 Experiments

### 4.1 Formal Environment

#### Interactive Theorem Provers.

Interactive Theorem Provers (ITPs), such as Isabelle (Paulson, ), are essential tools in modern mathematical verification. They help incorporate mathematical definitions and theorems into a consistent logical framework, such as Higher-Order Logic or Dependent Type Theory, which their kernels implement. The kernel is vital in the verification process, carefully checking each theorem to ensure it is correctly recognized by the ITP, thus maintaining system integrity. Using an ITP involves expressing the theorem in its programming language and then breaking it down into simpler goals or subgoals. A theorem is proven once it is reduced to known facts. We chose Isabelle for our paper because it has an intuitive interface, supports various logical frameworks, and offers a comprehensive library of formalized mathematics.

#### Sledgehammer.

Sledgehammer (Paulsson & Blanchette, ) is a powerful tool for automating reasoning within the interactive theorem prover Isabelle. It works by translating the goals expressed in Isabelle/HOL’s higher-order logic into other types of logic, such as first-order logic. These translated goals are then sent to automated theorem provers like E, CVC4, Z3, Vampire, and SPASS. If any of these automated provers succeed in finding proof, Sledgehammer reconstructs the proof within the Isabelle/HOL framework using certified provers, such as metis, meson, and smt. This reconstructed proof, being more understandable to humans, greatly improves the system’s usability and enhances the efficiency and effectiveness of interactive theorem proving.

### 4.2 Dataset and Evaluation

#### Dataset.

We evaluate our approach using the miniF2F dataset (Zheng et al., ), which includes $488$ formal mathematical problems from high-school competitions, expressed in three formal languages: Lean, HOL-Light, and Isabelle. The dataset is split into a validation set and a test set, each containing $244$ problems. These problems come from three different sources: $260$ problems are from the MATH dataset (Hendrycks et al., ), $160$ problems are from real high-school mathematical competitions (AMC, AIME, and IMO), and $68$ problems are designed to match the difficulty level of these competitions.

#### Evaluation.

The task involves generating formal sketches for problems in the miniF2F dataset. The validity of a formal sketch must meet two criteria: it should not contain ”cheating” keywords like ”sorry” and ”oops” that end a proof prematurely, and it must be verifiable by the interactive theorem prover Isabelle. To facilitate working with Isabelle, we use the Portal-to-Isabelle API introduced by Jiang et al. (). We use the pass rate to measure our results, reporting it for both the miniF2F-valid set and the miniF2F-test set.

### 4.3 Baselines

To assess the performance of our approach, we compare it against several established baselines.

#### Symbolic Automated Provers.

We first apply Sledgehammer, a proof automation tool extensively used within the Isabelle environment. Sledgehammer incorporates a 120-second timeout and utilizes five automated theorem provers (Z3, CVC4, SPASS, Vampire, E). Following Jiang et al. (), we enhance Sledgehammer with a set of 11 common tactics (e.g., auto, simp, blast, fastforce, force, eval, presburger, sos, arith, linarith, auto simp: field simps). If these tactics fail or take longer than 10 seconds, the system defaults to the basic Sledgehammer configuration.

#### Search-based Approaches.

We also employ search-based methods, particularly Monte-Carlo tree search (Silver et al., ), to explore proof possibilities. This includes Thor (Jiang et al., ) and a version enhanced with expert iteration on autoformalized data (Thor+expert iteration (Wu et al., )). Thor integrates language models with automated theorem provers to efficiently select premises from large libraries, while Thor+expert iteration further refines this by training on autoformalized theorems.

#### LLM-based Approaches.

In the LLM-based category, we evaluate several frameworks: Draft, Sketch, and Prove (DSP) (Jiang et al., ), LEGO-Prover (Xin et al., ), Lyra (Zheng et al., ), and Subgoal-Prover (Zhao et al., ). DSP uses the $540B$ Minerva model (Lewkowycz et al., ) to generate formal sketches from informal proofs. LEGO-Prover incrementally develops reusable theorems to enhance proof efficiency, while Lyra integrates feedback from external verifiers to optimize the verification process. Subgoal-Prover improves LLM performance in formal theorem proving by replacing informal proofs with subgoal-based proofs and using diffusion models to organize demonstrations optimally. Notably, all these methods employ Sledgehammer for consistency across evaluations.

Comparisons with theorem proving methods based on Lean (de Moura et al., ), a system utilizing distinct tactics and automation mechanisms that are not directly comparable to Isabelle, are deferred to Appendix C for thorough analysis.

**Table 1: Performance on the miniF2F dataset. Methods marked with ^† incorporate human-written informal proofs either fully or partially during the proof search process. Bold numbers denote the highest performance achieved.**
| Model | Base | miniF2F-valid | miniF2F-test |
| --- | --- | --- | --- |
| Sledgehammer | - | 9.9% | 10.4% |
| Sledgehammer+heuristic | - | 18.0% | 20.9% |
| Thor (Jiang et al., ) | - | 28.3% | 29.9% |
| Thor + expert iteration (Wu et al., ) | - | 37.3% | 35.2% |
| DSP (Jiang et al., )^† | Codex | 42.6% | 39.3% |
| Subgoal-Prover (Zhao et al., ) | GPT-3.5-Turbo | 48.0% | 45.5% |
| LEGO-Prover (Xin et al., )^† | GPT-3.5-Turbo | 55.3% | 50.0% |
| Lyra (Zheng et al., )^† | GPT-4 | 55.3% | 51.2% |
| $\mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{<br>X}\mathtt{L}$ (ours)^† | Llama-3-8B | 61.9% | 56.1% |

### 4.4 Implementation Details

We collected past AMC8, AMC10, AMC12, AIME, and IMO problems from the AOPS website (^3^33[https://artofproblemsolving.com/community](https://artofproblemsolving.com/community)) and combined them with training data from GSM8K (Cobbe et al., ) and MATH (Hendrycks et al., ) to build the informal dataset. The formal dataset was constructed using the AFP-2021 (^4^44[https://www.isa-afp.org/release/afp-2021-10-22.tar.gz](https://www.isa-afp.org/release/afp-2021-10-22.tar.gz)) library and the HOL library from Isabelle 2021 (^5^55[https://isabelle.in.tum.de/website-Isabelle2021/dist/Isabelle2021_linux.tar.gz](https://isabelle.in.tum.de/website-Isabelle2021/dist/Isabelle2021_linux.tar.gz)). This resulted in a total of 18k $\langle\text{Informal Statement},\text{Informal Proof}\rangle$ pairs and 195k $\langle\text{Formal Statement},\text{Formal Proof}\rangle$ pairs. To prevent data leakage, we filtered out problems that had more than 10% 3-gram overlap with those from the miniF2F dataset.

For the initialization phase, we employed a mixture of deepseek-math-base and Llama3-8b, with a maximum generation length of 2048 tokens and temperature settings of 0.6 and 0.8. This yielded 27k quadruples for the informal dataset and 174k quadruples for the formal dataset. The training of Llama3-8b was performed with a learning rate of 1e-5 over 3 epochs, utilizing a sequence length of 8192 tokens. These hyperparameters were also applied during the expert learning phase. All training was performed on a single SN20 node.

For the expert learning phase, we retained 11k problems from the informal dataset (after excluding GSM8K problems) and 10k problems from the formal dataset (after selecting 10k problems from the HOL library). The maximum number of expert learning iterations, $K_{\text{max}}$, was set to 3, with a sample size $m$ of 2. At each iteration, we trained 4 formal proof generators using combinations of two prompt templates and two proof lengths, leading to a total of 16 models after 3 iterations. The number of verified proofs generated during each iteration was 3156, 3592, and 4117, respectively. Adding the 27k verified proofs obtained during the initialization phase, a total of 38k verified proofs were generated.

For inference, each model generated 512 samples with and without human-written informal proofs, resulting in a total of 16384 proof attempts across all iterations for the miniF2F dataset. This includes 8192 attempts with human-written informal proofs and 8192 attempts without them. The inference process was executed across 4 SN40 nodes.

Verification was carried out using both Isabelle 2021 and Isabelle 2022. A formal proof was deemed correct if it passed verification in either version of Isabelle. The verification process was conducted on 2048 CPUs.

### 4.5 Main Results

Our main experimental results, as shown in Table 1, highlight several important findings: (1) $\mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{
X}\mathtt{L}$ achieves the best performance, setting a new state-of-the-art with 56.1% on the miniF2F-test dataset, surpassing previous methods by an absolute improvement of up to 4.9%. (2) The success of both $\mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{
X}\mathtt{L}$ and Subgoal-Prover emphasizes the effectiveness of subgoal-based proofs in enhancing the capabilities of large language models in formal theorem proving. (3) The benefits of expert iteration are evident, as demonstrated by the performance gains of Thor + expert iteration and $\mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{
X}\mathtt{L}$, reinforcing the value of iterative refinement in boosting theorem proving accuracy.

## 5 Analysis

**Table 2: Ablation study results on the miniF2F dataset.**
| Model | miniF2F-valid | miniF2F-test |
| --- | --- | --- |
| $\mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{<br>X}\mathtt{L}$ | 46.3% | 39.3% |
| -subgoal | 34.8% | 36.5% |

### 5.1 Ablation Study

In our study, we conducted ablation experiments on our proposed model using a search budget of $64$ to assess the impact of the subgoal-based framework. We evaluated two configurations: the complete model and a variant without subgoal-based proofs (-subgoal). Results in Table 2 demonstrate the importance of the subgoal-based component, as removing it (-subgoal) led to a significant decrease in performance. Specifically, the full model achieved 46.3% on the miniF2F-valid and 39.3% on the miniF2F-test, whereas the -subgoal variant saw a reduction to 34.8% on miniF2F-valid and 36.5% on miniF2F-test.

**Table 3: Impact of human-written informal proofs on the performance of $\mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{ X}\mathtt{L}$ on the miniF2F dataset. The miniF2F benchmark includes human-written informal proofs for each problem, provided by the benchmark’s publishers.**
| Model | miniF2F-valid | miniF2F-test |
| --- | --- | --- |
| $\mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{<br>X}\mathtt{L}$ (w/o informal proof) | 59.4% | 52.5% |
| $\mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{<br>X}\mathtt{L}$ (with informal proof) | 57.8% | 52.1% |

### 5.2 Impact of Human-Written Informal Proofs

We investigated the effect of human-written informal proofs on the performance of our model by conducting experiments with and without these proofs, using a search budget of $8192$. Table 3 presents the results on the miniF2F-valid and miniF2F-test datasets. Our model without informal proofs achieved 59.4% on miniF2F-valid and 52.5% on miniF2F-test, while the version incorporating informal proofs reached 57.8% on miniF2F-valid and 52.1% on miniF2F-test. These results suggest that the inclusion of human-written informal proofs does not significantly enhance the model’s performance. Our model’s generation of subgoal-based proofs appears to be more effective than utilizing informal proofs in certain scenarios (refer to §5.6 for detailed examples).

Figure: (a) Validation pass-rate over iterations
Refer to caption: x3.png

### 5.3 Iterative Performance Analysis

To evaluate our model’s iterative improvement, we conducted experiments with and without human-written informal proofs, tracking validation and test pass rates over several iterations in the expert learning process. Figures 2(a) and 2(b) present these pass rates across four iterations.
In the miniF2F-valid split (Figure 2(a)), the model without informal proofs began at 54.92% in iteration 0 and plateaued at 59.43% by iteration 2, maintaining this performance in iteration 3. The model with informal proofs started at 54.10%, peaking at 57.79% in iteration 3. Overall validation performance increased consistently from 58.20% in iteration 0 to 61.89% in iteration 3.
In the miniF2F-test split (Figure 2(b)), the model without informal proofs improved from 47.13% in iteration 0 to 52.46% in iteration 3, while the model with informal proofs started at 48.36% and reached 52.05% by iteration 3. Overall test performance increased from 51.23% in iteration 0 to 56.15% in iteration 3.
These results indicate that our subgoal-based framework drives iterative performance improvements, with the exclusion of informal proofs often yielding better results.

Figure: Figure 3: Synthetic proof pass-rate over iterations.
Refer to caption: x5.png

### 5.4 Synthetic Proof Pass Rate Analysis

We analyzed the pass rates of synthetic proofs over three iterations to evaluate the iterative learning process. The results, depicted in Figure 3, show a steady increase in performance. In iteration 1, the pass rate was 32.18%. This improved to 36.63% in iteration 2 and further to 41.98% in iteration 3. These results indicate a consistent improvement in the generation of synthetic proofs as the iterations progress, highlighting the effectiveness of the iterative learning framework in enhancing the model’s proof generation capabilities.

Figure: Figure 4: Counts of Different Error Types
Refer to caption: x6.png

Figure: Figure 5: Case study comparing subgoal-based and informal proofs. The left example shows a successful attempt using subgoal-based proofs, while the right examples depict failed attempts with informal proofs.
Refer to caption: x7.png

### 5.5 Error Analysis in Proof Generation

To gain insights into the errors encountered during proof generation, we categorized and quantified various error types. The results, depicted in Figure 4, reveal the frequency of each error category.
The most prevalent error was “Outer syntax error” with $1,510,737$ occurrences, followed by “Failed to finish proof” ($127,082$), and “Undefined fact” ($124,611$). Other notable errors included “Type unification failed” ($90,664$), “Timeout” ($74,459$), and “Failed to apply initial proof method“ ($58,659$).
This detailed error analysis highlights common failure points in the proof generation process, providing a clear direction for targeted improvements.

### 5.6 Case Study

We evaluated the effectiveness of subgoal-based proofs versus informal proofs using a specific theorem. As shown in Figure 5, the leftmost example represents a successful proof using subgoal-based methods, while the other examples depict failed attempts using informal proofs. The subgoal-based proof demonstrated robustness and effectiveness, whereas the informal proof attempts failed to sufficiently establish the necessary conditions, leading to incomplete proofs.

## 6 Conclusion

In conclusion, $\mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{
X}\mathtt{L}$ marks a significant step forward in AI-powered theorem proving within the Isabelle environment. By addressing the challenges of complex multi-step reasoning, $\mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{
X}\mathtt{L}$ demonstrates the efficacy of integrating subgoal-based proofs with an expert learning framework. This method iteratively refines three key components: a formal statement generator, a formal proof generator, and a subgoal generator, leading to improved performance on theorem-proving tasks. The empirical results confirm the effectiveness of $\mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{
X}\mathtt{L}$, achieving state-of-the-art performance on the standard miniF2F dataset with a score of 56.1%, while successfully solving 41 AMC12 problems, 9 AIME problems, and 3 IMO problems. This work paves the way for further innovations in applying AI to tackle advanced mathematical challenges in formal theorem proving.

## Appendix A More Details about Subgoal-based Proof

After creating $26$ demonstration examples, as detailed in §3.2, we used the prompt shown in Figure 6 to annotate subgoal-based proofs for the problems in the informal dataset.

Figure: Figure 6: Prompt to generate subgoal-based proofs.
Refer to caption: x8.png

## Appendix B More Details about Expert Learning

### B.1 Implementation Details of Each Component

The prompt templates for the formal statement generator, subgoal generator, and posterior subgoal generator are shown in Figures 7-9, respectively. To improve the diversity of outputs generated by the formal proof generator, we employ two distinct prompt templates, as illustrated in Figures 10 and 11.
In this study, all components are initialized with Llama-3-8B.

Figure: Figure 7: Prompt for formal statement generator.
Refer to caption: x9.png

Figure: Figure 8: Prompt for subgoal generator.
Refer to caption: x10.png

Figure: Figure 9: Prompt for posterior subgoal generator.
Refer to caption: x11.png

Figure: Figure 10: Prompt for formal proof generator (template 1).
Refer to caption: x12.png

Figure: Figure 11: Prompt for formal proof generator (template 2).
Refer to caption: x13.png

### B.2 Annotation of Formal and Informal Data

For the problems within the informal dataset, we employed a mixture of deepSeek-math-base and Llama-3-8B using the prompt templates illustrated in Figures 12 and 13 to generate their corresponding formal statements and proofs. For the problems in the formal dataset, we use the prompt template shown in Figure 14 to annotate their informal statements and proofs.

Figure: Figure 12: Prompt to generate formal statements.
Refer to caption: x14.png

Figure: Figure 13: Prompt to generate formal proofs.
Refer to caption: x15.png

Figure: Figure 14: Prompt to generate informal statements and proofs.
Refer to caption: x16.png

### B.3 Optimal Distributions for Formal Statements and Subgoal-Based Proofs

The optimal distribution for the formal statement at the $k$-th iteration is given by:

$$ $p^{\star}_{\text{fsg}}(\mathcal{S}\mid\mathcal{s})=\frac{1}{Z(\mathcal{s})}p^{ (k-1)}_{\text{fsg}}(\mathcal{S}\mid\mathcal{s})\exp\left(\frac{1}{\beta}\left( \log p_{\text{sg}}(\mathcal{g}\mid\mathcal{s},\mathcal{S})\right)\right),$ (3) $$

where $Z(\mathcal{s})=\sum_{\mathcal{S}}p^{(k-1)}_{\text{fsg}}(\mathcal{S}\mid
\mathcal{s})\exp\left(\frac{1}{\beta}\left(\log p_{\text{sg}}(\mathcal{g}\mid
\mathcal{s},\mathcal{S})\right)\right)$.

Similarly, the optimal distribution for the subgoal-based proof at the $k$-th iteration is determined by:

$$ $p^{\star}_{\text{sg}}(\mathcal{g}\mid\mathcal{s},\mathcal{S})=\frac{1}{Z( \mathcal{s},\mathcal{S})}p^{(k-1)}_{\text{sg}}(\mathcal{g}\mid\mathcal{s}, \mathcal{S})\exp\left(\frac{1}{\beta}\left(\log p_{\text{fpg}}(\mathcal{P}\mid \mathcal{s},\mathcal{S},\mathcal{g})\right)\right),$ (4) $$

where $Z(\mathcal{s},\mathcal{S})=\sum_{\mathcal{g}}p^{(k-1)}_{\text{sg}}(\mathcal{g}
\mid\mathcal{s},\mathcal{S})\exp\left(\frac{1}{\beta}\left(\log p_{\text{fpg}}
(\mathcal{P}\mid\mathcal{s},\mathcal{S},\mathcal{g})\right)\right)$.

## Appendix C Comparative Analysis with Lean-based Methods

**Table 4: Performance on the miniF2F dataset. Methods marked with ^† integrate human-written informal proofs, either in full or partially, during the proof search. Methods denoted by ^‡ employ a tree search strategy, where the search budget is structured as N $\times$ M, representing N search trees with M as the budget per tree.**
| Model | Base | Synthetic Size | Search Budget | miniF2F-valid | miniF2F-test |
| --- | --- | --- | --- | --- | --- |
| Lean-based |  |  |  |  |  |
| HTPS (Lample et al., )^‡ | - | - | - | 58.6% | 41.0% |
| Lean-STaR (Lin et al., )^‡ | InternLM2-Math-plus | 50k Theorems | 64 $\times$ 50 | - | 46.3% |
| DeepSeek-Prover (Xin et al., ) | DeepSeekMath-Base | 712k Theorems | 65536 | - | 50.0% |
| InternLM2-StepProver (Wu et al., )^‡ | InternLM2-Math-plus | 1.155B Tokens | 64 $\times$ 3200 | 63.9% | 54.5% |
| DeepSeek-Prover-V1.5 (Xin et al., )^‡ | DeepSeekMath-Base | 9B Tokens | 32 $\times$ 6400 | - | 63.5% |
| Isabelle-based |  |  |  |  |  |
| Sledgehammer | - | - | - | 9.9% | 10.4% |
| Sledgehammer+heuristic | - | - | - | 18.0% | 20.9% |
| Thor (Jiang et al., )^‡ | - | - | 300 | 28.3% | 29.9% |
| Thor + expert iteration (Wu et al., )^‡ | - | - | - | 37.3% | 35.2% |
| DSP (Jiang et al., )^† | Codex | - | 100 | 42.6% | 39.3% |
| Subgoal-Prover (Zhao et al., ) | GPT-3.5-Turbo | - | 100 | 48.0% | 45.5% |
| LEGO-Prover (Xin et al., )^† | GPT-3.5-Turbo | - | 100 | 55.3% | 50.0% |
| Lyra (Zheng et al., )^† | GPT-4 | - | 200 | 55.3% | 51.2% |
| $\mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{<br>X}\mathtt{L}$ (ours)^† | Llama-3 | 38k Theorems | 16384 | 61.9% | 56.1% |

In this section, we provide a detailed analysis and discussion of the performance of our approach in relation to Lean-based theorem proving methods, including HTPS (Lample et al., ), Lean-STaR (Lin et al., ), DeepSeek-Prover (Xin et al., ), InternLM2-StepProver (Wu et al., ) and DeepSeek-Prover-V1.5 (Xin et al., ). Lean employs a unique set of tactics and automation techniques that differ significantly from those used in the Isabelle proof assistant, making direct comparisons within the main body of our evaluation less meaningful.

Table 4 demonstrates the significant performance variation across Lean-based and Isabelle-based approaches on the miniF2F dataset. Lean-based methods generally operate on a much larger scale, utilizing between $15\times$ and $120\times$ more synthesized proofs than Isabelle-based systems. For example, DeepSeek-Prover-V1.5 employs 9 billion tokens of synthesized data, while our approach uses only 38k theorems. Furthermore, these Lean methods typically operate with a search budget that is approximately $12.5\times$ larger than ours. InternLM2-StepProver, for instance, operates with a search budget of 64 $\times$ 3200, compared to our search budget of 16,384.

Despite this, $\mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{
X}\mathtt{L}$ outperforms most Lean-based methods, achieving 56.1% on the miniF2F-test dataset compared to 54.5% for InternLM2-StepProver and 50.0% for DeepSeek-Prover. On the miniF2F-valid dataset, $\mathtt{S}\mathtt{u}\mathtt{b}\mathtt{g}\mathtt{o}\mathtt{a}\mathtt{l}\mathtt{
X}\mathtt{L}$ also exhibits strong performance, further demonstrating the efficiency of our subgoal-based approach, even with significantly smaller synthetic data and a more moderate search budget. These results suggest that our approach is highly effective in optimizing formal theorem-proving tasks. A potential direction for future work is to scale up the size of synthesized proofs and the search budget, which could further enhance performance and competitiveness, particularly in comparison to resource-intensive Lean-based methods.

## Peer Reviews

confidence: 3
contribution: 2
initial_rating: 3
presentation: 2
questions: 1. Do you use the provided informal proofs for miniF2F when generating the
   formal proof in the final evaluation?
2. Could you release the fine-tuning datasets for inspection?
3. Could you release the 26 demonstrations of step-by-step proofs (Appendix C)?
4. Could you evaluate your system on PutnamBench?
5. What precisely is meant by "-subgoal" approach in Table 2?
6. Do you verify generated formal statements in any way?
7. The prompt for generating formal statements in Figure 7 has no mention of Isabelle. How does LLama 3 know that it is meant to generate formal statement in Isabelle?
8. Is the expert iteration run on miniF2F, on only on the fine-tuning datasets?
soundness: 2
strengths: The paper tackles a challenging and interesting problem of ML-guided formal theorem proving. It presents a new idea of applying an intermediate step of generating informal "subgoal proofs" before generating the formal proof.

The evaluation on miniF2F shows substantial improvement compared to the other approaches.

The authors release the code of SubgoalXL (although I didn't test it).
summary: The paper introduces SubgoalXL: a LLM-based system for formal theorem proving.  The system comprises of three components:

(1) formal statement generator,\
(2) formal proof generator,\
(3) subgoal generator.

These components are fine-tuned on sizable formal and informal data collected by the authors.

(3) is meant to produce step-by-step informal proofs that are closer in style to their formal counterparts, and can help to later produce a formal proof.

An evaluation on miniF2F is provided showing that SubgoalXL achieves better results than other published approaches.
weaknesses: The author do not analyze the inference-time compute in the evaluation.  For instance, you write "[a]t each iteration, we trained 4 formal proof generators". Are they all used when evaluating on miniF2F? This makes the inference cost potentially much higher than in the other approaches.

It is not described how you evaluate on miniF2F given the trained three components (see questions below).

The authors did not disclose the datasets for finetuning the components of SubgoalXL, which makes impossible to confirm there is no overlap between the datasets and miniF2F.

The authors did not disclose the 26 demonstrations of step-by-step proofs (Appendix C).

The authors instantiate SubgoalXL with only one LLM (LLama 3 8b). It would be good to see the results for different models (Mistral, Gemma, ...)

The author evaluate only on miniF2F, which has been available on the internet for a long time and it is likely that LLMs (like LLama 3) trained on it, which makes the evaluation less reliable. Additional evaluations on new benchmarks like PutnamBench would be recommended.

The description of the approach is sometimes inconsistent or difficult to understand. For example, in the Algorithm 1 there is no mention about the Isabelle verification of the produced formal proofs. Also, in line 14 the datasets are always initialized back to the initial versions, is it a mistake in the description?

In the related work section you completely omit non-LLM, but ML-based formal theorem proving works like [1,2,3,4,5].

[1] Blaauwbroek et al.: Graph2Tac: Online Representation Learning of Formal Math Concepts. ICML 2024\
[2] Piotrowski et al.: Machine-Learned Premise Selection for Lean. TABLEAUX 2023\
[3] Zhang et al.: Online Machine Learning Techniques for Coq: A Comparison. CICM 2021\
[4] Gauthier et al.: TacticToe: Learning to Reason with HOL4 Tactics. LPAR 2017\
[5] Urban et al.: MaLARea SG1 -- Machine Learner for Automated Reasoning with Semantic Guidance. IJCAR 2008

Minor remarks:
- In Introduction you mention Lean and Isabelle, but omit other important ITPs that were/are very important in the field of formal mathematics: Coq, Mizar, HOL, MetaMath.
- Figure 4 would look better if it used log scale X axis.
- The text in Figure 5 is way too small to be readable.
- line 152, "corresponds to corresponding": fix the style here
- sometimes you use wrong citation style (\citep vs \citet), e.g. in lines 97-98.

---

confidence: 3
contribution: 4
initial_rating: 6
presentation: 3
questions: In Section 4.3, the authors refer to SN20 and SN40 nodes. Could the authors elaborate on what these node types represent?
soundness: 3
strengths: + This paper introduces a novel method to address multi-step reasoning in interactive theorem proving by utilizing LLMs to generate subgoals. This approach is particularly valuable for scaling ITP by automating the decomposition of formal reasoning.
+ By generating informal-formal pairs of statements and proofs for subgoals, this work contributes to a richer dataset for formal theorem proving. This has implications beyond this paper, as it could aid the broader community in training more robust models for formal reasoning.
+ The approach achieves notable improvements on the miniF2F dataset, highlighting its effectiveness and potential to outperform current methods.
+ The authors conduct studies that reveal the impact of subgoal generation and the inclusion of human-written informal proofs, offering valuable insights into the mechanisms that enhance model performance.
summary: This paper proposes a novel approach to guiding formal theorem proving in the Isabelle proof assistant using Large Language Models (LLMs) through the generation of formal subgoals. By building three specialized generators—one for formal theorem statements, one for formal proofs, and one specifically for subgoal generation—the authors tackle the challenge of decomposing proofs into structured, manageable steps from both informal and formal contexts. The approach leverages probabilistic modeling methods for training these generators, and its performance is evaluated on the miniF2F dataset, showcasing notable improvements over existing methods. This work is an innovative application of LLMs to formal reasoning in Interactive Theorem Proving (ITP).
weaknesses: - Some evaluation results require additional clarification. In Table 2, the SubgoalXL model outperforms the -subgoal model by 11.5% on the miniF2F-valid dataset but only by 2.8% on the miniF2F-test dataset. This difference raises questions about the model’s consistency across different subsets of the dataset, and further explanation from the authors would help readers interpret this variation.
- In Figure 2, the "Overall" setting is presented alongside "With Informal" and "Without Informal" settings. It would be beneficial for the authors to clarify what "Overall" means and how it differs from the other settings.
- The quality of generated subgoals, while effective overall, shows occasional inaccuracies. For example, in line 523, the model generates a subgoal attempting to prove "gcd(6\*2+k)(6\*2+3)\\<noteq>1" when k=4, which is incorrect. Although the proof was completed by Isabelle’s sledgehammer using other contradiction in the context, the correct subgoal should likely be "gcd(6\*2+k)(6\*2+2)\\<noteq>1". This highlights a need for further refinement in subgoal generation accuracy, particularly in ensuring logical consistency across subgoals.

---

confidence: 4
contribution: 2
initial_rating: 3
presentation: 1
questions: **1. Writing issues:**
The Algorithm 1 refers to Eq. 3 and Eq. 4, but they are nowhere found in the main paper (they are in the appendix). At least mention that the equations are in some section in the appendix, it improves readability. I had a hard time finding these equations. 

**2. Lack of explanation:**
The authors don't explain the sampling steps clearly. There is some obscure reference to equations (steps 23 and 17 in Algorithm 1) but how the sampling is done along with examples will help in understanding the algorithm better.

**3. Proofs in Isabelle 2021 vs Isabelle 2022:**
Since any proof acceptable in either version is deemed correct, we don't know the split of proofs done in each version of Isabelle. It would be interesting to know if the model learns to prefer one version of the language over another based on the skew in training data.
soundness: 2
strengths: 1. **Independent sub-goal creation:**
While sub-goal creation for theorem proving is not a new idea, the authors try to make the sub-goal generation independent of the original theorem we are trying to prove. I believe that they could do this because of the choice of ITP (i.e. Isabelle) because proofs in Isabelle are written by adding hypothesis to the existing set of hypotheses, util one of the hypotheses matches the goal. In Lean, proofs are generally not written like this, we try to simplify or transform the goal using tactics. This makes sub-goaling more effective for approaches which use Isabelle versus the ones which use Lean.

2. **Separate model for sub-goal generation:**
Because of 1 the authors can train an independent sub-goal generation model, which is slightly different (and maybe better) from what has been done so far in this area.
summary: The authors propose an approach for improving formal theorem proving using expert iteration on data generated by sub-goal annotations. While it is well-known that creating sub-goals helps in writing formal proofs, the authors try to generate subgoals by training multiple models which specialize in formal proof generation, formal statement generation, and subgoal generation. As per the authors, training of these models in an expert iteration loop helps in boosting their performance further. The authors try to use KL-constraints while sampling proofs to avoid overoptimization for rewards during iterative training.
weaknesses: **1. Lack of Novelty:**
	This specific idea already exists in other forms for other ITPs. The LeanStar paper (https://arxiv.org/abs/2407.10040) which the authors cite, follows a very similar approach for Lean. The only difference is that instead of creating a sub-goal, CoT is created to explain the intermediate steps while writing formal Lean proofs. Just like Subgoal XL they also end up doing an expert iteration training. Other than the use of Isabelle instead of Lean, and sub-goal formulation instead of informalization, which I feel is a very natural thing to do in Lean as opposed to Isabelle because of forward proof writing style in Isabelle (see my point 1 in Strengths section), I don't see any significant difference between the two work. I would appreciate if the authors explained the key differences between the two approaches. I would like to understand what would their approach look like if they were doing the same thing for Lean. Will it be more similar to what is done in LeanStar?

**2. Use of miniF2F validation set for annotation generation and subsequent use of miniF2F validation set for evaluation:**
While authors mention that they filter out those problems which has some overlap with the miniF2F dataset, however, the initial sub-goal annotation is done using subset of manually proved theorems from miniF2F validation set as in-context examples. There is a chance that sub-goals thus generated for the training dataset, have parts of proofs leaked from miniF2F validation set itself because these sub-goals can itself be part of solutions in different problems. One possible evidence for my hypothesis is that there is a huge difference in performance when we compare removing sub-goal generation in the ablation study in Table 2. The performance on miniF2F-valid drops from 46.3% to 34..8% while miniF2F-test drops from 39.3% to 36.5%, this 12% drop vs 3% drop can be explained by possible leakage of miniF2F-valid data in the training data during the annotation phase because the annotations are generated using in-context miniF2F valid examples itself. I would like to see the performance of their approach for datasets other than miniF2F, most of the pre-trained models seemed to be potentially trained on miniF2F, GSM8k, etc. already. You can potentially test your approach on this new evaluation benchmark PutnamBench (https://arxiv.org/abs/2407.11214), which is harder than miniF2F and does not have proofs mentioned in their repository, thus avoiding potential leak issues.

**3. Impact of Human Written Proofs:**
	The ablation study claims that human written proofs don't help boost performance but rather deteriorate the performance of writing formal proofs. This claim is in sharp contrast of what is has been established in some of the well-known state-of-the-art works in this area like the DSP paper (https://arxiv.org/abs/2210.12283) which is cited by the authors. In the DSP paper, the authors show that even for a large number of samples (as high as 100) drawn from the LLM for informal proof generation, the performance on generating correct formal proofs was better with the ground truth informal proofs written by humans. I would like to see a more detailed study as to why the conclusion is different from DSP, and what is the explanation regarding this difference, is it because of some minor differences in the approach, or sub-goal generation, etc?

**4. Relaxed criteria for validation of correctness of proof:**
The authors mention in section 4.3 (page 7), that verification was carried out using both Isabelle 2021 and Isabelle 2022. Proof is considered valid if either of them passes, however, this can be problematic because there can be subgoals that work in different versions. There can be formalization differences and since individual subgoals may not compile in both versions the sub-goals themselves may not align. This is problematic and it hides the model's ability to generate consistent proof in one language, also this highlights that authors don't build the capability to control the language in which the proof has to be generated. The proof must be generated in a consistent language for the approach to be useful in a broader setting. Uncontrolled generation might as well mean that the formal proof thus generated is of no use, even when we can sample more to maybe get a working proof, the inability to control the generation is problematic and makes the approach inefficient. I would like to know the split of proofs done in each version of Isabelle. It would be interesting to know if the model learns to prefer one version of the language over another based on the skew in training data.

---

confidence: 5
contribution: 1
initial_rating: 3
presentation: 1
questions: Please address the concerns raised in the weakness section. Additionally, I have a few further questions:

- Could you provide an ablation study on your proposed diversity efforts, as well as the performance of SubgoalXL with search budgets of 100 and 200, to align with the other baselines for a fair comparison?

- Why does incorporating human-generated informal proofs seem to decrease performance on the miniF2F dataset?

- In Figure 5, why are all the proofs completed using sledgehammer? Does this indicate that the model primarily generates a formal sketch, leaving sledgehammer to fill in the rest? If sledgehammer were disabled, how many proofs could SubgoalXL complete independently?

- Could you provide more case studies demonstrating instances where SubgoalXL, with a search budget of 16,384, successfully proves additional theorems that existing baselines and SubgoalXL with a reduced search budget (e.g., 100-200) fail to prove on the miniF2F dataset?
soundness: 2
strengths: - The paper constructs an (aligned) informal-formal dataset by combining existing informal or formal datasets, which may be valuable to the community if made publicly available.

- SubgoalXL demonstrates strong performance on the miniF2F dataset, validating the effectiveness of its subgoal-based proofs and expert iteration approach.
summary: This paper introduces SubgoalXL, a method that combines subgoal-based proofs with expert iteration to improve formal theorem proving in Isabelle. SubgoalXL generates subgoal-based informal proofs, formal statements, and formal proofs for existing informal datasets, and produces informal statements and informal proofs for formal datasets. This creates an aligned informal-formal dataset, which is used to fine-tune an LLM (Llama-3-8B) with expert iteration for theorem proving. The results show that SubgoalXL outperforms existing methods on the miniF2F-valid and test sets, demonstrating the benefits of using subgoal-based proofs and expert iteration for formal theorem proving.
weaknesses: - The paper is poorly written in some sections, making it hard to follow.

First, I find the two key terms, "subgoal-based proofs" and "expert learning", somewhat confusing. Based on my understanding from the paper (e.g., Figures 1 and 6), "subgoal-based proofs" seem to refer to step-by-step informal proofs. However, in the abstract and line 84, the authors mention "leveraging the Isabelle environment’s advantages in subgoal-based proofs." This raises confusion because Isabelle handles formal proofs, not informal ones, which appear only as comments. It's unclear what specific advantages Isabelle provides in handling subgoal-based proofs. As for "expert learning", it appears that the authors are referring to "expert iteration", a more commonly used term in the ML community.

Second, while the paper uses standard ML terminology, in practice, it only implements prompt-based LLM fine-tuning and inference. The mathematical formulation and proofs presented are fairly simple and straightforward, but they come across as somewhat unnecessary and distracting. Additionally, the subscripts (e.g., "pfg") are introduced without explanation in Section 3.1. Though it later seems to stand for "formal proof generator," it appears inconsistent because in Section 3.1, it is involved in generating both informal and formal proofs, which adds to the ambiguity.

Third, there are some inconsistencies in the methodology. Section 3.2 and Figure 1 suggest that the generation of subgoal-based proofs is conditioned on manually provided formal proofs, but Figure 6 seems to indicate that no formal proofs are included in the prompt. This discrepancy needs further clarification.

- The methodology lacks technical novelty.

The main idea of decomposing proofs—whether informal or formal—into more manageable sub-proofs (or subgoal-based proofs) and leveraging expert iteration has already been widely explored in existing literature (e.g., [1, 2, 3]). This paper largely applies these well-established concepts to create a dataset for fine-tuning an LLM for neural theorem proving in Isabelle. While this may yield improved results, it doesn't introduce significant new insights, and thus offers limited added value to the community.

- The evaluation is not comprehensive and potentially unfair.

First, the paper evaluates its approach exclusively on the miniF2F dataset, which mainly consists of high-school level problems (e.g., AMC, AIME, IMO). The evaluation could be more comprehensive by including other datasets used in the literature, such as PutnamBench, which contains undergraduate-level math problems. Additionally, the error analysis and case studies are based solely on feedback from Isabelle. It would have been more informative to explore whether incorrect subgoal-based or informal proofs could still lead to corrected formal proofs.

Second, for the in-context learning examples, the authors manually annotate formal proofs for the miniF2F-valid dataset and then evaluate the model on that same dataset. For data generation and fine-tuning, they draw from high-school-level math problems in sources like AMC, AIME, IMO, GSM8K, and MATH. Although they mention filtering out problems with more than 10% 3-gram overlap, concerns about data contamination remain. Many of these problems share similar structures and proof strategies with those in miniF2F, which raises questions about the robustness of the evaluation. Furthermore, the model’s generalization ability remains unclear, as it has not been tested on out-of-distribution datasets like PutnamBench.

Third, the search budget for SubgoalXL in Table 1 is set to 16,384, while the other baselines only use 100-200, a detail that is not mentioned in the table, which feels a bit misleading. When the search budget is reduced to 64, SubgoalXL’s performance drops significantly, achieving only 46.3% and 39.3% accuracy on the miniF2F-valid and miniF2F-test, respectively. Additionally, many of SubgoalXL's proofs seem to rely heavily on the sledgehammer tool (as shown in Figure 5), suggesting that the model may not be solving the subgoals mathematically on its own, but instead calling sledgehammer whenever possible.

Reference:

[1] Jiang, Albert Q., et al. "Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs."

[2] Polu, Stanislas, et al. "Formal Mathematics Statement Curriculum Learning."

[3] Wang, Haiming, et al. "LEGO-Prover: Neural Theorem Proving with Growing Libraries."