ImProver: Agent-Based Automated Proof Optimization

## Abstract

Abstract Large language models (LLMs) have been used to generate formal proofs of mathematical theorems in proofs assistants such as Lean.
However, we often want to optimize a formal proof with respect to various criteria, depending on its downstream use.
For example, we may want a proof to adhere to a certain style, or to be readable, concise, or modularly structured.
Having suitably optimized proofs is also important for learning tasks, especially since human-written proofs may not optimal for that purpose.
To this end, we study a new problem of automated proof optimization: rewriting a proof so that it is correct and optimizes for an arbitrary criterion, such as length or readability.
As a first method for automated proof optimization, we present ImProver ImProver \mathrm{ImProver} roman_ImProver , a large-language-model agent that rewrites proofs to optimize arbitrary user-defined metrics in Lean.
We find that naively applying LLMs to proof optimization falls short, and we incorporate various improvements into ImProver ImProver \mathrm{ImProver} roman_ImProver , such as the use of symbolic Lean context in a novel Chain-of-States technique, as well as error-correction and retrieval. We test ImProver ImProver \mathrm{ImProver} roman_ImProver on rewriting real-world undergraduate, competition, and research-level mathematics theorems, finding that ImProver ImProver \mathrm{ImProver} roman_ImProver is capable of rewriting proofs so that they are substantially shorter, more modular, and more readable.

## 1 Introduction

The fundamental virtue of a mathematical proof is that it provides certainty: a deductive argument shows that the assumptions of a mathematical statement logically guarantee the conclusion. In practice, however, informal, natural-language proofs are prone to imprecision, ambiguity, and error.
Using a formal language such as Lean (Moura & Ullrich, ) removes ambiguity and precision and enables a proof assistant to verify correctness down to the primitives of a formal axiomatic system.

Formal proofs, however, can be hard to read and often suffer from low reusability or excessive detail.
For example, formal proofs in Lean’s extensive mathematical library, Mathlib (mathlib Community, ), are generally designed to be concise and very general, often at the expense of readability.
Formal proofs in an expository text, in contrast, may include detailed calculations steps, making them readable but verbose.
Machine learning systems trained on such proofs learn to mimic these varied conventions (Hu et al., ), which may not be the optimal use of the limited supply of human-written proofs.
As a result, we would like to be able to automatically refactor proofs to meet a secondary objective such as length or readability.

To this end, we study a new problem of automated proof optimization: rewriting a proof so that it is correct and optimizes a criterion such as length or readability.
We find that naively applying LLMs to proof optimization falls short, often resulting in incorrect or poorly optimized proofs.
We develop various improvements that can be applied on top of a black-box language model, including Chain-of-States prompting–an analogy to chain-of-thought prompting (Wei et al., ) that shows intermediate proof states–along with error-correction and retrieval.
We incorporate these into $\mathrm{ImProver}$: a large language model agent that rewrites proofs to optimize arbitrary user-defined metrics in Lean.

We test $\mathrm{ImProver}$ on rewriting real-world undergraduate theorems, competition problems, and research-level mathematics, finding that $\mathrm{ImProver}$ is capable of rewriting proofs so that they are substantially shorter, more readable, and more declarative in style.(^1^11Code is available at [https://github.com/riyazahuja/ImProver](https://github.com/riyazahuja/ImProver).)

Figure: Figure 1: $\mathrm{ImProver}$ automatically rewrites formal proofs to optimize a criterion such as length or readability while remaining correct. In this example, $\mathrm{ImProver}$ optimizes a human-written lemma (right) from the 2022 International Math Olympiad (Question 2, solution from Compfiles (David Renshaw, )) for length. $\mathrm{ImProver}$’s optimized proof is correct and more concise.

## 2 Related work

Recently there has been wide interest in automating theorem proving in interactive proof assistants; see (Lu et al., ; Li et al., ) for surveys.

A typical approach (Polu & Sutskever, ) is to train on a large corpus of mathematical proofs such as Lean’s Mathlib (mathlib Community, ; Han et al., ; Polu et al., ; Lample et al., ; Yang et al., ; Hu et al., ).
A model learns from the distribution of proofs in the corpus, such as Mathlib-style proofs.
Recently, the AlphaProof (AlphaProof & Teams, ) system was shown to produce proofs with an arcane, non-human structure and syntax.
We consider the new problem of rewriting a proof to optimize a metric, such as rewriting a proof into a more readable or more concise one.
Proof optimization is more general than theorem proving, since we can also rewrite an empty proof to optimize correctness.
Finally, there is a rich literature on the varied styles of (human) formal proofs (e.g., (Autexier & Dietrich, ; Wiedijk, )).
Our model, $\mathrm{ImProver}$, builds on neural theorem proving techniques including full proof generation (Jiang et al., ; First et al., ), conditioning on example proofs (Jiang et al., ), retrieval (Yang et al., ; Thakur et al., ), and preceding file context (First et al., ; Hu et al., ), as well as error correction (Madaan et al., ; Chen et al., ) and documentation retrieval (Zhou et al., ) from code generation.
$\mathrm{ImProver}$ brings these code generation techniques, along with new Chain-of-States prompting and meta-programmed contextual information, into a unified proof optimization agent.

## 3 Automated Proof Optimization with ImProver ImProver \mathrm{ImProver} roman_ImProver

##### Automated Proof Optimization.

Given a theorem statement $x$, additional context $c$, and an initial proof $y_{0}$, proof optimization consists of generating a new proof $y$ that is correct and minimizes (or maximizes) a metric $\mu(x,c,y_{0},y)\rightarrow\mathbb{R}$.

By varying the metric, we can perform tasks such as shortening proofs, making them more readable, or even automated proving.
We consider 3 metrics:

Length Metric: The length metric measures the number of tactic invocations in the tactic proof, aiming to reduce the proof’s length while ensuring its correctness. Note that shorter proofs often represent more efficient proofs.

Readability Metric: We consider a proof to be readable if it is written in a declarative style (Autexier & Dietrich, ; Wiedijk, ), which is related to the number of independent subproofs in a proof. Concretely, we evaluate this using the ratio of number of explicitly typed have tactics to total number of tactic invocations.

Completion Metric: The completion of a proof simply describes its correctness. This is a trivial metric which measures the number of errors present. The completion metric is used for concretely viewing proof optimization as a generalization of neural theorem proving.

### 3.1 Improver

We develop several improvements that can be applied to a black-box LLM generator $y_{out}\sim G(\cdot|x_{in})$, such as GPT-4 (OpenAI et al., ), and specify $\mathrm{ImProver}$ with respect to these parameters. The explicit prompts and templates that are sent to the LLM can be found in (§A).

#### 3.1.1 Chain-of-States Prompting

Typical formal proofs are a sequence of tactics (akin to steps) and states that show the hypotheses and goals at each step.
The intermediate states often contain valuable information (e.g., an expression after it has been simplified) that is not present in the tactics. To allow the model to reason about these intermediate goals and hypotheses, we use tools from Lean metaprogramming to automatically annotate each proof state as a comment prior to each tactic.
We refer to this method as Chain-of-States (CoS) prompting since it makes intermediate states explicit, akin to how chain-of-thought prompting (Wei et al., ) makes intermediate steps of a solution explicit.

These states are extracted directly and symbolically from the underlying Lean compilation steps using Lean’s rich metaprogramming suite. The implementation of this extraction system is modeled from the work (Kim Morrison, ). Specifically, in the compiler’s elaboration and evaluation stages – where the parsed theorem code is first converted into concrete syntax trees (in practice, Syntax objects) and abstract syntax trees (Expr objects) – we convert the CST and AST output objects into the relevant proof data and proof states in the form of proof trees (Lean.Elab.InfoTree). These proof trees contain detailed context and information on a tactic-by-tactic level relating to the modification of the proof state, metavariable context, and proof correctness.

After state extraction is completed and cached for efficient future access, we annotate the proof text itself to contain the intermediate states in the form as comments.
Figure 2 shows an example.

This explicit reasoning aims to help the generator model construct more optimized proofs via additional symbolic data.

Figure: Figure 2: A Lean proof (left) with Chain-of-States prompting annotations (right).

#### 3.1.2 Output formatting.

LLM outputs often contain ancillary and syntactically invalid content, especially before and after the actual proof. Additionally, by applying additional structure to the LLM outputs, we may hope to generate more structured proofs. To analyze this hypothesis, we introduce two additional output formats to the standard str output: flat and structured. The former enforces a tactic sequence output as a list of strings, and the latter enforces a proof tree output as a tree of strings.

#### 3.1.3 Sampling Method

We also introduce different methods of sampling between many (sequential or parallel) LLM inference calls, involving best-of-n and iterative refinement implementations, as well as combinations thereof.

##### Best-of-n

The best-of-n technique generates multiple ($n$) calls to the language model and selects the “best” via a simple selection policy that first prioritizes output correctness, and secondly prioritizes the evaluated metric delta score. More specifically, our scoring function is given by the $2$-ary comparison function $S$, whose arguments are output objects $y,y^{\prime}$.

$$ $S(y,y^{\prime})=\begin{cases}\max(y,y^{\prime},\text{key: }x\mapsto\mu(x)),&E( y)=E(y^{\prime})=0\\ y,&E(y)=0,E(y^{\prime})>0\\ y^{\prime},&E(y)>0,E(y^{\prime})=0\\ \min(y,y^{\prime},\text{key: }x\mapsto E(x)),&E(y)=E(y^{\prime})>0\\ \end{cases}$ $$

Where $\mu(x)$ is the metric score of $x$, and $E(x)$ is the number of errors in $x$.

This comparison function can be extended to evaluate the best output of any finite $n$ via induction.

This best-of-n technique is implemented as a curried function such that each of the $n$ calls can be handled by any arbitrary sampling method, or just a single standard prompt at user discretion. It utilizes thread-based parallelism to speed up the relatively large number of calls to the language model, as well as process-based parallelism for the $n$ evaluation calls to the Lean language server.

##### Error correction and Refinement

Inspired by self-debugging techniques in code generation (Madaan et al., ; Chen et al., ), $\mathrm{ImProver}$ identifies and corrects errors in the generated proofs by iteratively refining its outputs.
The refinement process relies on user-defined parameters n and prev_num to specify the number of iterations and the number of previous iteration info to forward, respectively. Each iteration carries information on the last prev_num iterations, including input, output, metric score, correctness, and error messages.

The refinement technique iteratively improves the prompt output by feeding back the results into the prompt function, additionally forwarding errors and metric scores. Similar to the best-of-n technique, it relies on an argument $n$ for the number of refinement steps, and is curried such that each refinement step can be handled by any other prompting function. However, unlike best-of-n, there is no opportunity for parallelism as each iteration is dependent on information from the previous call.

##### Combination Sampling and Compound Prompt Functions

Compound prompt functions utilize the curried nature of the implementations of best-of-n and refinement to nest these techniques within one another. For example:

best_of_n((refinement,m),n) is a compound sampling method that run a best-of-$n$, where each call is a $m$-step refinement.

refinement((best_of_n,m),n) is a compound sampling method that runs a $n$-step refinement, where each call is a best-of-$m$ call to the LLM.

Note that with each of these compound prompt functions, there are always a total of $mn$ iterations.

#### 3.1.4 Retrieval

$\mathrm{ImProver}$ uses MMR (Maximum Marginal Relevance)-based (Carbonell & Goldstein, ) retrieval-augmented generation to select relevant examples and documents.

More specifically, example retrieval selects the most relevant user-generated examples of proof optimization on a specific metric. Namely, each metric is loaded with a cached (vector) database populated with human-made examples of preoptimized and postoptimized pairs of Lean theorems. The number of examples that are retrieved is user-specified.

Document retrieval extracts information using MMR from a pair of fixed (vector) databases. The databases store semantically chunked data from the Theorem Proving in Lean (TPiL) handbook – containing syntax guides and tactic explanations – and the Mathlib mathematics libary – containing thousands of theorems and lemmas. The chunking is handled by a recursive character splitter, which splits the TPiL markdown files at on its headers and Mathlib files at the start of theorems, examples, lemmas, and definitions – with chunk sizes of 1000 characters with a 200 character overlap.

The Mathlib retriever finds the top $k$ documents that score the highest MMR score against the current theorem, the TPiL retriever finds the top $k$ documents that score the highest MMR score against the current theorem in context and all current error messages. This retrieval process helps in generating more contextually accurate prompts that allow the language model to better correct its own errors as well as find useful lemmas to reference.

## 4 Experiments

We test $\mathrm{ImProver}$ on rewriting real-world undergraduate theorems, competition problems, and research-level mathematics and compare its results to those of the base GPT-4o and GPT-4o-mini models. We examine the optimization capabilities of $\mathrm{ImProver}$ for the length and readability metrics - studying the effectiveness in maintaining the correctness of the tactic proof while making it more concise, as well as making it more declarative in style and readable in practice.

### 4.1 Setup

Our experimentation is split into three distinct stages. We first perform ablation testing on the $\mathrm{ImProver}$ model parameters (§3.1) to ensure that $\mathrm{ImProver}$’s parameter specification is the optimal one with respect to correctness and metric optimization score. We then evaluate this optimal parameter combination on datasets of varying complexity and analyze the performance and results thereof. Lastly, we note the performance of $\mathrm{ImProver}$ in NTP applications in comparison to the base GPT-4o and GPT-4o-mini models.

##### Datasets.

We evaluate $\mathrm{ImProver}$ on subsets of the following datasets.

Mathematics in Lean (MIL) (leanprover-community, ): this dataset contains pedagogical solutions of common undergraduate-level exercises, and as such contains many readable, yet verbose and inefficient proofs.
We use exercise solutions from set theory, elementary number theory, group theory, topology, differential calculus, and integration & measure theory. This dataset contains theorems at an undergraduate-level of complexity.
For our main results, we evaluated on $72$ theorems from exercise solutions from MIL chapters $4,5,8,9,$ and $10$.

Compfiles (David Renshaw, ): Solutions of International Mathematics Olympiad (IMO) and American Mathematics Olympiad (USAMO) competition problems from 2016 to 2024. This is a dataset of internationally-renowned competitive math problems, many of which are readable, yet quite verbose. This dataset contains theorems of a competitive format, and although they contain concepts only at a high-school level, the logical complexity of internationally-renowned competition results is far above that.
For our main results, we used all $26$ theorems and lemmas from the Compfiles database of complete solutions to the International Mathematics Olympiad (IMO) and the American Mathematics Olympiad (USAMO) from 2016-2024.

Mathlib (mathlib Community, ): Mathlib contains many advanced results at the forefront of mathematics, and has been at the center of research-level formalizations. These proofs are extremely efficient, concise, and generalized - which often comes at the cost of readability and understandability. These results and theorems often are at the cutting edge of research.

For our main results, we evaluated our methods on $43$ advanced research-level proofs from Mathlib/AlgebraicTopology/FundamentalGroupoid. This is the most difficult dataset.

##### Models.

Our base generator uses GPT-4o (OpenAI et al., ). Since no prior methods currently exist for automated proof optimization, we consider a prompted GPT-4o without the improvements described in (§3.1) as our baseline. Additionally, for a given metric, we write a prompt that briefly describes the metric and the proof optimization task. We also provide instructions, context, and information depending on the features selected, and add the theorem and proof to the prompt. Specific prompt information is detailed in (§A)

##### Performance metrics.

Since proof optimization is a new task, we define four performance metrics for measuring aspects of correctness and improvement.

First, we define improvement for length as percentage change in length, $\frac{\mu_{\text{len}}(y_{0})-\mu_{\text{len}}(y)}{\mu_{\text{len}}(y_{0})}
\times 100$.
For readability, we use the difference, $\mu_{\text{read}}(y)-\mu_{\text{read}}(y_{o})$.
If no correct output is generated by the model for a specific theorem, improvement is defined to be zero. We define nonempty improvement as the improvement restricted to theorems for which some output has nonzero improvement.

Intuitively, improvement is the expected improvement in metric score from the input to output, accounting for errors in the generation. The nonempty improvement score is the expected improvement in metric score, given that there are no errors in the generation.
Similar improvement scores can be defined for other metrics using a binary function of the metric assigned to the original and optimized proofs.

Additionally, the accuracy is the percentage of theorems in the dataset which the model was able to generate a correct output for. The improved accuracy is the percentage of theorems in the dataset which the model was able to generate a correct output for, as well as improve the metric to be nonzero.

#### 4.1.1 Ablations

When performing our ablation studies, we used a fixed dataset (MIL) and metric (length) and varied the parameters of all the features to find the optimal combination. However, as there are over $8640$ possible combinations, it is inefficient to test all combinations at once. As such, we evaluate using a factorial testing method.

##### Testing Groups.

We define the following testing groups with the specified parameter combinations:

GPT-4o-mini/GPT-4o: This varies the GPT-4o model, outputting a string with no other features.

Output and CoS: We evaluate the effects of different output formatting styles (string, string list, string tree) and CoS (True, False), with the model fixed as GPT-4o, with no other features enabled.

Example Retrieval: We evaluate the effects of increasing the number of examples provided (multi-shot prompting) in the range of $0,3,5,7,$ and $10$, with the model fixed as GPT-4o, CoS and output formatting fixed as the best combination from the previous test, and no other features enabled.

Sampling Method: Here, we evaluate the effects of best-of-n and refinement for a fixed $n=5$. Additionally we test on the refinement cases if forwarding the most recent iteration result, or all previous iteration results is the best, and if we should keep the best out of the iterations, or the most recent. The model is fixed as GPT-4o, CoS, output formatting, and examples are fixed as the best combination from the previous test, and no other features enabled.

$n$ and Model: Here, we evaluate the effects of larger $n$ values and different models. We test $n=3,5,7,10,15$ on GPT-4o and GPT-4o-mini, as well as $n=20$ for GPT-4o-mini (as it is of a far lower token cost). CoS, output formatting, examples, and sampling method are fixed as the best combination from the previous test, and no other features enabled.

Combos and RAG: We evaluate combination methods refinement(best_of_m’,m) and best_of_m’(refinement(m)), for $m\neq m^{\prime}$ with $mm^{\prime}$ equal to the optimal value $m$ from the previous test. We also test the effect of enabling document retrieval. Model, CoS, output formatting, examples, $n$, and sampling method are fixed as the best combination from the previous test.

##### Ablation data.

We evaluate our ablations on a subset of MIL. However, due to the increase in model calls for larger $n$ values, we switch a representative sample of this subset for some test groups. Namely,

GPT-4o-mini, GPT-4o, Output and Cos, Example Retrieval, and Sampling Method are tested on the $133$ theorems in the solutions of C03_Logic, C04_Sets_and_Functions, and C05_Elementary_Number_Theory.

$n$ and Model are tested on $55$ theorems from a representative sample of the aforementioned, and Combos and RAG are tested on a representative sample of $32$ theorems from the aforementioned.

### 4.2 Results

##### ImProver ImProver \mathrm{ImProver} roman_ImProver is capable of optimizing proofs in all settings.

**Table 1: Average Proof optimization results.**
| Metric | Model | Improvement | Nonempty Improvement | Accuracy | Improved Acc. |
| --- | --- | --- | --- | --- | --- |
| Length | GPT-4o | 3.7 | 15.15 | 26.36% | 8.31% |
| $\mathrm{ImProver}$ | 20.96 | 55.29 | 100.0% | 35.44% |  |
| Readability | GPT-4o | 2.21 | 8.02 | 18.75% | 6.13 % |
| $\mathrm{ImProver}$ | 9.34 | 30.53 | 100.0% | 24.56% |  |

**Table 2: MIL Proof optimization results.**
| Metric | Model | Improvement | Nonempty Improvement | Accuracy | Improved Acc. |
| --- | --- | --- | --- | --- | --- |
| Length | GPT-4o | 6.25 | 18.58 | 37.5% | 14.42% |
| $\mathrm{ImProver}$ | 30.54 | 56.56 | 100.0% | 50.0% |  |
| Readability | GPT-4o | 4.18 | 14.48 | 28.85% | 11.54% |
| $\mathrm{ImProver}$ | 13.45 | 30.97 | 100.0% | 34.21% |  |

**Table 3: Compfiles Proof optimization results.**
| Metric | Model | Improvement | Nonempty Improvement | Accuracy | Improved Acc. |
| --- | --- | --- | --- | --- | --- |
| Length | GPT-4o | 2.75 | 30.7 | 11.54% | 5.13% |
| $\mathrm{ImProver}$ | 18.86 | 54.48 | 100.0% | 34.62% |  |
| Readability | GPT-4o | 0.39 | 3.38 | 14.1% | 1.28% |
| $\mathrm{ImProver}$ | 5.74 | 24.89 | 100.0% | 19.23% |  |

**Table 4: Mathlib Proof optimization results.**
| Metric | Model | Improvement | Nonempty Improvement | Accuracy | Improved Acc. |
| --- | --- | --- | --- | --- | --- |
| Length | GPT-4o | 0.0 | 0.0 | 16.67% | 0.0% |
| $\mathrm{ImProver}$ | 6.19 | 53.65 | 100.0% | 11.54% |  |
| Readability | GPT-4o | 0.0 | 0.0 | 4.65% | 0.0% |
| $\mathrm{ImProver}$ | 4.63 | 33.19 | 100.0% | 11.63% |  |

From Table 2, Table 3, and Table 4, we can see that $\mathrm{ImProver}$ is capable of optimizing proofs on all datasets for both the length and readability metrics.
Furthermore, Table 1 shows that across all metrics, $\mathrm{ImProver}$ significantly outperforms GPT-4o on proof optimization tasks on every experimental measure – aggregated from all datasets. Additionally, from Table 2, Table 3, and Table 4, we can see that $\mathrm{ImProver}$ outperforms GPT-4o on each dataset as well.

We proceed to analyze this data and its implications.

##### Length optimization.

First focusing on the length metric, we see that $\mathrm{ImProver}$ outperforms GPT-4o with respect to the improvement score by $566\%$ (aggregated over all datasets). Additionally, we are guaranteed that $\mathrm{ImProver}$ produces a correct output, although that output may just be the same as the input. However, $35.44\%$ of the time, it generates a correct output that is not the same length as the input, and in that case, we expect an average of a $55.29\%$ reduction in length. Comparing this with GPT-4o, we conclude that not only can $\mathrm{ImProver}$ optimize at a higher level on arbitrary theorems, but its ability to generate nontrivial correct outputs is far greater in comparison to GPT-4o.

##### Readability optimization.

Readability optimization is similar, with $\mathrm{ImProver}$ outperforming GPT-4o by $423\%$. Moreover, the accuracy, improved accuracy, and nonempty improvement disparities for readability parallel those of the length tests. However, it should be noted that for both GPT-4o and $\mathrm{ImProver}$, the accuracy and improved accuracy scores were markedly smaller for readability than length optimization. This suggests that for both models, it was generally more “difficult” to generate a correct output, and moreover, generate a correct output with a better metric score than the input, for readability optimization than length optimization. In other words, optimizing for readability is more difficult for the underlying generator than optimizing for length. However, we speculate with higher-quality prompts, descriptions of the metric, and examples, this disparity can be minimized. Regardless, we note that different metrics can be less likely to be correctly optimized, and that model performance is correlated with the metric it seeks to optimize – both for GPT-4o and $\mathrm{ImProver}$.

##### Optimization varies based on dataset difficulty.

Additionally noting Table 2, Table 3, and Table 4, we observe that the improvement score for both metrics for both GPT-4o and $\mathrm{ImProver}$ is highest for the MIL dataset, lower for Compfiles, and the lowest on the Mathlib theorems. This suggests that the expected improvement in metric score decreases with higher difficultly – with undergraduate-level theorems having a significantly higher expected improvement than research-level theorems. However, it should be noted that for both metrics, the nonempty improvement of $\mathrm{ImProver}$ stayed consistent, whereas for GPT-4o, it followed the aforementioned trend of decreasing with difficulty. Similarly, the accuracy and improved accuracy scores for both metrics and models decreased with higher difficulty datasets (disregarding $\mathrm{ImProver}$’s accuracy scores, as they are ensured to be 100%). This suggests that although the base GPT-4o generator is less likely to generate a correct output for higher difficulty datasets, the improvements that $\mathrm{ImProver}$ makes to the base generator allows it to maintain its improvement in the metric score whenever a correct output is generated. As such, we can speculate that the bottleneck in the improvement score is not the model’s ability to optimize the proof for a metric, but rather its ability to generate a new correct proof at all. As such, we conjecture that with more capable generator models, the accuracy – and thus, the improvement score – in optimization tasks will continue to increase, until the improvement scores match the nonempty improvement.

Overall, we conclude that although the performance of both $\mathrm{ImProver}$ and GPT-4o decreases on length and readability optimization on more difficult datasets, $\mathrm{ImProver}$ significantly outperforms GPT-4o on all datasets for length and readability optimization.

#### 4.2.1 Ablation Testing

**Table 5: Ablation results. Each cell in the ablation tests shows best / worst, which are the best and worst parameter combinations in the test group. The ImProver specification outputs the input theorem when no correct proof is generated, which results in an accuracy of 100% on MIL.**
|  | Improvement | Nonempty Improve. | Accuracy | Improved Acc. |
| --- | --- | --- | --- | --- |
| GPT-4o-mini | 0 | 0 | 3.62% | 0% |
| GPT-4o | 7.03 | 19.67 | 35.77% | 15.33% |
| + Output and CoS | 8.04 / 6.31 | 12.38 / 14.17 | 64.96% / 44.53% | 21.17% / 16.06% |
| + Example Retrieval | 9.34 / 5.67 | 14.7 / 8.44 | 63.5% / 67.15% | 21.9% / 16.79% |
| + Sampling Method | 15.35 / 9.34 | 18.44 / 14.7 | 83.21% / 63.5% | 36.5% / 21.9% |
| + $n$ and Model | 23.51 / 3.65 | 26.28 / 4.63 | 89.47% / 78.95% | 45.61% / 8.77% |
| + Combos and RAG | 34.88 / 28.25 | 57.56 / 33.48 | 60.61% / 84.38% | 54.55% / 53.12% |
| $\mathrm{ImProver}$ | 34.88 | 57.56 | 100% | 54.55% |

We perform ablation studies using a subset of the MIL dataset as discussed in §4.1.1. The results of this factorial study are aggregated in Table 5. We measure the baseline results from the GPT-4o and GPT-4o-mini models, noting that GPT-4o is the better-scoring model (with respect to the improvement score). Thus, fixing this model, we vary the output formatting type and if CoS is enabled, and determine that outputting flat with CoS enabled maximizes the improvement score. Fixing these parameters, we now vary the number of examples retrieved, noting that prompting with $10$ examples maximizes the improvement score. Fixing this parameter, we vary the sampling methods (excluding compound methods and fixing $n=5$) and observe that best-of-n is the best parameter combination. Now, as GPT-4o-mini is significantly less computationally expensive than its GPT-4o counterpart, we test both models with the sample method fixed to best-of-n, and vary $n=1,3,5,7,10,15$, and for GPT-4o-mini, also $n=20$. We conclude that GPT-4o with $n=15$ is the most effective. Fixing these parameters, we consider all mixed compound sampling methods with and without document retrieval enabled, concluding that a $5$-step refinement with best-of-$3$ on each iteration, with RAG enabled, is the optimal combination.

Thus, as we can see from Table 5, the optimal parameter combination comes from gpt-4o outputting as a string list with CoS, RAG, $10$ examples, $5$-step refinement with each iteration being a best-of-$3$ evaluation. Changing any one of these parameters them leads to a reduction in performance. Additional ablation data can be found at (§B.1).

##### Readability and Chain-of-States (CoS) Ablation.

**Table 6: CoS Readability Ablation results.**
|  | Improvement | Nonempty Improve. | Accuracy | Improved Acc. |
| --- | --- | --- | --- | --- |
| GPT-4o | 4.97 | 15.89 | 37.5% | 12.5% |
| $\mathrm{ImProver}$, CoS Disabled | 9.23 | 24.61 | 100.0% | 28.12% |
| $\mathrm{ImProver}$ | 16.69 | 31.42 | 100.0% | 46.88% |

We additionally examine the effects of disabling CoS on readability optimization tasks, as the previous study focused on length optimization tasks, and we speculate that CoS has a high impact on the performance of readability optimization tasks, as the proof states that are embedded due to CoS seem to be a critical aspect to generating the explicit declarations that the readability metric measures.

We confirm this result by considering Table 6 and observe that simply enabling CoS nearly doubles the improvement score, and significantly improves the nonempty improvement score, suggesting that CoS has a high degree of impact on optimizing for the readability metric, as conjectured. However, we also note a significant increase in improved accuracy, which suggests that embedding the chain of states also improves the ability of the model to generate nontrivial correct outputs, implying that the symbolic information contained in the states are critical to effectively modifying the structure and content of a proof.

#### 4.2.2 Neural Theorem Proving Evaluation

**Table 7: Proof generation results. Each cell shows percent accuracy.**
| MIL | Set Theory | Group Theory | Overall |
| --- | --- | --- | --- |
| GPT-4o | 18.18% | 25% | 21.73% |
| $\mathrm{ImProver}$ | 45.45% | 33.33% | 39.13% |

We evaluate $\mathrm{ImProver}$’s neural theorem proving (NTP) performance using the completion metric. We evaluate on 23 exercises in group theory (12) and set theory (11) from MIL, with an empty input proof. Table 7 shows the accuracy on the dataset split by topic for both $\mathrm{ImProver}$ and GPT-4o. $\mathrm{ImProver}$ substantially outperforms GPT-4o across all topics, with an 80% increase in accuracy compared to the base model, showing that proof optimization systems are easily extendable to NTP systems.

### 4.3 Qualitative Results

Next, we discuss qualitative examples showing the improvements from $\mathrm{ImProver}$ in proof optimization. These examples show the balance between correctness and the desired optimization metric, showing how $\mathrm{ImProver}$ can produce more concise or readable proofs depending on the use case. Additional examples can be found in (§B.2)

##### Example 1: Compfiles Optimization.

Consider Figure 1, a lemma from the 2022 IMO Question 2 (Compfiles) that we optimize for length.

The original proof consisted of 12 tactic steps and multiple intermediate calculations. After applying $\mathrm{ImProver}$ for length optimization, the proof was halved to only 6 tactics, eliminating redundant steps while maintaining correctness.

In comparison, the shortened proof makes multiple nontrivial optimizations, such as eliminating the h2’ and h4 and hxw hypotheses, as well as fully generating proof terms for specific rewrites and other tactics.

##### Example 2: MIL.

Consider Figure 3, a result from MIL that we optimize for readability.

Figure: Figure 3: Optimizing a group-theoretic result from MIL Chapter 8 Section 1 for readability. We define a proof to be readable if it is written in a declarative style, which consists of intermediate conjectures (have $\cdots$ statements). $\mathrm{ImProver}$ introduces two intermediate conjectures into the proof.

This original proof carried a score of 0 0, as it does not contain any declarative statements. In comparison, after applying $\mathrm{ImProver}$, we transformed the proof to be more declarative, with many more intermediate steps with explicit have tactics for improved clarity. Additionally observe how the model defines hypotheses for use in the latter half of the proof; these predefined hypotheses could easily be converted into standalone lemmas for reuse.

##### Example 3: Full Proof Generation.

We analyze the application of $\mathrm{ImProver}$ to neural theorem proving in the MIL example from Figure 4.

Figure: Figure 4: Solving a group theorem exercise from MIL Chapter 8 Section 1 for readability.

This theorem relating to group theory originally has no proof, however, $\mathrm{ImProver}$ generates one from scratch. This generated proof is verified to be correct by Lean, utilizing all the included hypotheses as well as a retrieved mathlib theorem.

## 5 Conclusion

In this paper, we introduced $\mathrm{ImProver}$, a novel agent-based tool for automated proof optimization in Lean. By incorporating CoS, RAG, and other features, $\mathrm{ImProver}$ significantly outperforms base language models in proof optimization over undergraduate, competition, and research-level problems.

However, $\mathrm{ImProver}$ is limited by its high cost and slow runtime, which is exacerbated by its reliance on black-box LLM’s. We intend to address this inefficiency in future work by applying fine-tuning and RL on a smaller model to match performance at a lower cost.

$\mathrm{ImProver}$ demonstrates its ability to generate substantially shorter, more readable, and modular proofs while maintaining correctness. As such, we believe that $\mathrm{ImProver}$ sets the stage for further work on proof optimization to advance the study and use of AI in mathematics.

#### Acknowledgements

Riyaz Ahuja thanks the L3 Lab and Hoskinson Center for Formal Mathematics for their support.

Sean Welleck thanks Convergent Research, the Lean FRO, and the OpenAI Researcher Access Program for their support.

## Appendix A Prompts

In this appendix, we note the prompts used by $\mathrm{ImProver}$ both for general LLM prompting, as well as the metric-specific prompts.

### A.1 Template

For the main prompt sent to the LLM on each sample, we build a prompt string using a chat prompt template that is then invoked at runtime to fill in the variables.

Namely, these variables include the set of metric prompts, previous results, input theorem, context, a syntax documents, Mathlib documents, and examples.

The prompt template is a conversation of the format:

- Placeholder: All metric prompts with a ‘System’ role
- System: You will be given the proof context (i.e. the lean file contents/imports leading up to the theorem declaration) wrapped by <CONTEXT>…</CONTEXT>.
You will be given the previous num_prev input/output pairs as well as their metric (metric.name) score and correctness score, as well as any error messages, for your reference to improve upon. Each of these previous results will be wrapped with <PREV I=0></PREV I=0>,…,<PREV I=num_prev-1></PREV I=num_prev-1>, with I=num_prev-1 being the most recent result.
Remember to use lean 4 syntax, which has significant changes from the lean 3 syntax.
To assist with the syntax relating to the current theorem and current error messages, you will be given num_syntax_docs documents to refer to for fixing these syntax issues. Each of these documents will be wrapped with <SYNTAX_DOC>…</SYNTAX_DOC>.
You will also receive num_mathlib_docs documents relevant to the current theorem to help with formulating your modified proof. Each of these will be wrapped with <CONTENT_DOC>…</CONTENT_DOC>
You will also receive num_examples examples of input-output pairs of proofs that were optimized for the metric metric. Each of these will be wrapped with <EXAMPLE>…</EXAMPLE>
You will be given the tactic states as comments for reference.
The current theorem will be wrapped in <CURRENT>…</CURRENT>
- System: Output format instructions
- Placeholder: All retrieved syntax documentation
- Placeholder: All retrieved mathlib documentation
- Placeholder: All retrieved examples
- User: <CONTEXT>
context
</CONTEXT>
- Placeholder: Previous results and inputs/outputs
- Placeholder: All metric prompts with a ‘User’ role
- User: <CURRENT>
theorem
</CURRENT>

This prompt is then invoked and sent to the language model by filling in all the variables and placeholders. Notably, when we invoke the chain given by $\texttt{chain}|\texttt{llm}|\texttt{parser}$, we throttle the invocation with a randomized exponential rate limit throttling to account for API rate limits, especially in highly-parallelized requests like when benchmarking over a large number of theorems.

### A.2 Metric Prompts

Length Metric

- System: You are an AI assistant who shortens Lean 4 proofs while ensuring their correctness. You will aim to reduce the number of lines of the tactic proof while ensuring that it properly compiles in Lean 4.
- User: Shorten the current theorem (wrapped in <CURRENT>…</CURRENT>) to be as short in length—measured in the number of lines of the proof—as possible, while also ensuring that the output is still syntactically correct."

Readability Metric

- System: You are an AI assistant who rewrites Lean 4 proofs to be more readable while ensuring their correctness. We measure readablity by considering the ratio of the number ofexplicitly typed have tactics against the total number of tactics in the proof, as this is proportional to whether a proof is declarative in style, and thus, readable.
- User: Rewrite the current theorem (wrapped in <CURRENT>…</CURRENT>) so it is more readable and declarative and modular.

Completion Metric

- System: You are an AI assistant who automatically solves Lean 4 proofs (as in, generates the tactic proof) and ensures its correctness. You will receive a Lean 4 proof you must modify to eliminate any errors so that it compiles correctly and eliminate any “sorry”s with full proofs.
- User: Rewrite the current theorem (wrapped in <CURRENT>…</CURRENT>) so it is a formal, complete, and correct Lean 4 proof by filling in its tactic proof.

## Appendix B Additional Experimental Results

In this section, we provide more detailed information on the experimental setup and results used to evaluate $\mathrm{ImProver}$.

### B.1 Ablation Details

We now proceed to show detailed results from our ablation testing.

**Table 8: Output and Chain-of-States Ablations**
| Output Format | CoS | Improvement | Nonempty Improve. | Accuracy | Improved Acc. |
| --- | --- | --- | --- | --- | --- |
| string | True | 7.53 | 16.12 | 46.72% | 16.79% |
| string | False | 7.03 | 19.67 | 35.77% | 15.33% |
| string list | True | 8.04 | 12.38 | 64.96% | 21.17% |
| string list | False | 7.04 | 13.58 | 51.82% | 18.98% |
| string tree | True | 7.62 | 15.34 | 49.64% | 18.25% |
| string tree | False | 6.31 | 14.17 | 44.53% | 16.06% |

By Table 8, we see that the optimal combination in this testing group is a string list output format with CoS enabled. Fix these values for all future tests.

**Table 9: Example Retrieval Ablations**
| Examples | Improvement | Nonempty Improve. | Accuracy | Improved Acc. |
| --- | --- | --- | --- | --- |
| 0 | 5.67 | 8.44 | 67.15% | 16.79% |
| 3 | 8.49 | 13.68 | 62.04% | 19.71% |
| 5 | 8.38 | 12.9 | 64.96% | 21.17% |
| 7 | 7.56 | 12.04 | 62.77% | 19.71% |
| 10 | 9.34 | 14.7 | 63.5% | 21.9% |

With the previous optimal parameters fixed, run the ablation on the number of examples. By Table 9, we see that the optimal combination in this testing group is $10$ examples. Fix this value for all future tests.

**Table 10: Sampling Method Ablations**
| Method | Forward | Keep Best | Improvement | Nonempty Improve. | Accuracy | Improved Acc. |
| --- | --- | --- | --- | --- | --- | --- |
| None | N/A | N/A | 9.34 | 14.7 | 63.5% | 21.9% |
| refinement | 1 | False | 14.76 | 30.63 | 48.18% | 30.66% |
| refinement | 5 | False | 12.5 | 20.88 | 59.85% | 30.66% |
| refinement | 1 | True | 14.95 | 14.95 | 100.0% | 30.66% |
| refinement | 5 | True | 13.15 | 13.15 | 100.0% | 29.93% |
| best-of-n | N/A | N/A | 15.35 | 18.44 | 83.21% | 36.5% |

Note that forward and keep-best values are parameters for refinement of how many previous iterations to forward, and whether to keep the most recent or the best iteration in subsequent refinement steps.

Now, with the previous optimal parameters fixed, run the ablation on the sample method. By Table 10, we see that the optimal combination in this testing group is best-of-n. Fix this value for all future tests.

**Table 11: Model and $n$ Ablations**
| Model | $n$ | Improvement | Nonempty Improve. | Accuracy | Improved Acc. |
| --- | --- | --- | --- | --- | --- |
| gpt-4o | 3 | 19.66 | 24.36 | 80.7% | 38.6% |
| gpt-4o | 5 | 20.12 | 24.97 | 80.56% | 36.11% |
| gpt-4o | 7 | 22.44 | 27.21 | 82.46% | 42.11% |
| gpt-4o | 10 | 21.73 | 25.28 | 85.96% | 40.35% |
| gpt-4o | 15 | 23.51 | 26.28 | 89.47% | 45.61% |
| gpt-4o-mini | 3 | 3.65 | 4.63 | 78.95% | 8.77% |
| gpt-4o-mini | 5 | 5.12 | 6.21 | 82.46% | 10.53% |
| gpt-4o-mini | 7 | 3.65 | 4.34 | 84.21% | 8.77% |
| gpt-4o-mini | 10 | 4.99 | 5.69 | 87.72% | 12.28% |
| gpt-4o-mini | 15 | 4.35 | 5.06 | 85.96% | 12.28% |
| gpt-4o-mini | 20 | 4.87 | 5.56 | 87.72% | 14.04% |

With the previous optimal parameters fixed, run the ablation on the value of $n$ and model. By Table 11, we see that the optimal combination in this testing group is GPT-4o with $n=15$. Fix this value for all future tests.

**Table 12: RAG and Combination Sampling Method Ablations**
| Combination | $m$ | $m^{\prime}$ | RAG | Improvement | Nonempty Improve. | Accuracy | Improved Acc. |
| --- | --- | --- | --- | --- | --- | --- | --- |
| best-of-n(refinement) | 3 | 5 | True | 33.78 | 33.78 | 100.0% | 50.0% |
| best-of-n(refinement) | 3 | 5 | False | 31.23 | 31.23 | 100.0% | 46.88% |
| best-of-n(refinement) | 5 | 3 | True | 31.85 | 31.85 | 100.0% | 50.0% |
| best-of-n(refinement) | 5 | 3 | False | 31.35 | 31.35 | 100.0% | 50.0% |
| refinement(best-of-n) | 3 | 5 | True | 32.66 | 51.32 | 63.64% | 48.48% |
| refinement(best-of-n) | 3 | 5 | False | 32.88 | 50.1 | 65.62% | 53.12% |
| refinement(best-of-n) | 5 | 3 | True | 34.88 | 57.56 | 60.61% | 54.55% |
| refinement(best-of-n) | 5 | 3 | False | 29.54 | 49.75 | 59.38% | 43.75% |
| best-of-n | N/A | 15 | True | 29.64 | 32.71 | 90.62% | 56.25% |
| best-of-n | N/A | 15 | False | 28.25 | 33.48 | 84.38% | 53.12% |

With the previous optimal parameters fixed, run the ablation on the combination methods and if RAG is enabled. By Table 12, we see that the optimal combination in this testing group is a $5$-step refinement with each iteration being a best-of-3 call, with RAG enabled.

### B.2 Additional Qualitative Examples

In this section, we provide qualitative examples demonstrating the improvements $\mathrm{ImProver}$ achieves in proof optimization.

##### Compfiles: Length Optimization

See (§4.3)

##### Compfiles: Readability Optimization

Consider Figure 5, in which a lemma from the 2019 IMO problem 1 (from the Compfiles dataset) is optimized for readability. This introduces multiple new hypotheses, which generalize a linear_property of the functions, and then reuses and instantiates that (and others, too) hypothesis throughout the proof, creating a significantly more declaritive, modular, and therefore readable proof.

Figure: Figure 5: Optimizing a lemma from IMO 2019 P1 for readability

##### MIL: Length Optimization

Consider Figure 6, which optimizes an exercise solution from MIL Chapter 8, Section 1 (Group theory) for length, eliminating simp calls and introducing proof terms into the structure of the proof to shorten it from $9$ tactic invocations to $7$.

Figure: Figure 6: Optimizing a lemma from the solutions of MIL CH08 S01 for length

##### MIL: Length Optimization 2

Consider Figure 6, which optimizes an exercise solution from MIL Chapter 8, Section 1 (Group theory) for length, converting a full tactic proof into a single proof term to shorten it from $28$ tactic invocations to $1$. Note that the model does not have access to the Lean commands that symbolically generate proof terms, and therefore generates and estimates the proof term entirely by itself.

Figure: Figure 7: Optimizing a lemma from MIL CH04 S01 solution for length

##### MIL: Readability Optimization

See (§4.3)

##### Mathlib: Length Optimization

Consider Figure 8, which optimizes a theorem in algebraic topology from mathlib for length, eliminating simp calls and combining tactics to shorten it from $3$ tactic invocations to $1$.

Figure: Figure 8: Optimizing a theorem from Mathlib/FundamentalGroupoid/InducedMaps for length

##### Mathlib: Readability Optimization

Consider Figure 9, a theorem from Mathlib that we optimize for readability.

This original proof carried a score of 0 0, as it does not contain any declarative statements. It is concise and efficient, however, it is difficult to understand and read.

After optimizing for readability, we see that the model did not change the structure of the proof. Rather, it added an intermediate declaration so that users can better understand the state after the convert. This intermediate tactic greatly helps in the understandability and clarity of the proof.

Figure: Figure 9: Optimizing a theorem from Mathlib/FundamentalGroupoid/SimplyConnected for readability

## Peer Reviews

confidence: 4
contribution: 3
initial_rating: 5
presentation: 4
questions: - Could the authors clarify under what criterion the mathematical branch of the dataset for testing the neural theorem proving effect was selected and whether they have evaluated the method on the entire dataset and other commonly used datasets?
- Could the author clarify whether they have tried any rule-based methods and compared their results to those produced by ImProver?
soundness: 3
strengths: This paper first discovers a new field of automated proof optimization, and conducts a pioneering attempt in this field, marking the first significant effort to use LLMs for enhancing formal proofs with respect to certain metrics in proof assistants like Lean. A notable strength of this work is its emphasis on the role of proof states in guiding LLMs. By introducing the Chain-of-States technique, which provides intermediate proof states to the LLM, the authors demonstrate an understanding of how contextual information can significantly improve the accuracy and efficiency of proof optimization.
summary: The paper introduces ImProver, a large language model (LLM) agent designed for automated proof optimization in the proof assistant Lean. ImProver adopts several LLM augmentation methods, including a Chain-of-States technique that provides intermediate proof states to LLM, retrieval methods, and sampling methods.

The paper defines three key metrics for evaluation: the Length Metric, which aims to minimize the number of tactic invocations; the Readability Metric, which favors a declarative haveproof style; and the Completion Metric, which measures proof correctness.

In experiments, the author compares ImProver with the baseline GPT-4o model on Mathematics in Lean (MIL), Compfiles, and Mathlib datasets. The results show that ImProver reduces the length of 35.44% of proofs compared to 8.31% for GPT-4o, and increases readability in 24.56% of proofs compared to 6.13% for GPT-4o. Proof completion was evaluated only on the selected MIL dataset, where ImProver achieved 39.13% successful proof generation compared to 21.73% for GPT-4o.
weaknesses: - The method proposed in this paper is well-suited for metrics that can be directly computed from the formal proof. However, this limits its applicability to more complex metrics such as readability. The paper defines readability as the ratio of explicitly typed have tactics to the total number of tactic invocations in line 130. This simple definition may lead to a proof with numerous unused have tactics being considered more readable than a normal proof. The reviewer considers readability to be a multifaceted metric, influenced by various factors including the use of underlines, the depth of proof terms, the naming of variables, appropriate comments within the proof, and other stylistic elements. These factors are challenging to quantify with a simple function, suggesting that the proposed method may not be effective for assessing readability or other nuanced aspects of proof quality.
- The reviewer suggests developing a combined metric that considers both length and readability for a more accurate assessment of proof quality in real applications, since improving in one metric may significantly sacrificing other metrics. Additional experiments should test whether the framework described in the paper can effectively balance and improve these combined metrics.
- The proof generation results in Table 7 are limited to specific selected datasets. The reviewer believes that ImProver's neural theorem proving results should also be evaluated on unselected datasets and more commonly used test sets, and compared with a wider range of models to provide a comprehensive assessment of the proposed method's performance.
- The comparison with GPT-4o, which lacks proper Lean 4 syntax capabilities, may not accurately reflect the effect of RAG or refinement policies of ImProver. More ablation studies could be conducted to demonstrate that the rise in performance is not solely due to the guidance for correct Lean 4 syntax in the prompt.
- The reviewer suggests that rule-based optimization methods for Lean, particularly for the length metric (e.g., using nested termwise proofs to replace tactic-based proofs), exist. The authors should compare ImProver with these methods to demonstrate its relative strengths.

---

confidence: 3
contribution: 2
initial_rating: 5
presentation: 2
questions: - It is possible to explain the benefits of solving the proof optimization problem with application domains (such as formal verification or mathematical education), references, and concrete examples that support the claim?
- I think it is important to incorporate some kind of random in using the best-of-n technique. Does the proposed approach ensure diversity in the LLM outputs when using the best-of-n technique? If yes, how it is achieved? Otherwise, how do you address the potential issue of deterministic outputs?
- Can you provide a detailed description of the input format for ImProver and GPT-4o in the experiment? Especially, does the input include the original proof from the dataset, a partial proof, or start with an empty proof?
- The paper claims ImProver can rewrite proofs so that they are more modular. Can you provide a clear definition of 'modular' in the paper?  It would also be helpful to give modular and non-modular examples.
- What does the paper mean by efficient proofs? (E.g., it says "These proofs are extremely efficient" in lines 266-267).
soundness: 3
strengths: + The paper tackles the proof optimization, which has not been considered yet in neural theorem proving, and proposes a (simple) approach to it.
+ The proposed approach can outperform the baseline, which simply queries to an LLM (GPT-4o).
summary: The paper tackles the proof optimization problem, which aims to optimize partly written proofs with respect to a given criterion (such as length and readability).
The paper also addresses the problem by querying to LLMs and ranking the outputs with the criterion.
weaknesses: - Because the proposed approach to the proof optimization (described in Section 3) is simple, I find the main contribution of the paper is in applying LLMs to proof optimization, a problem in theorem proving. When evaluating the paper from such a viewpoint, I admit the proof optimization problem may be worth studying, but I don't think the paper argues its value in a convincing manner. The second paragraph of Section 1 discusses the importance of the proof optimization, but there is no reference to support the argument. That is, there is no objective material to find the importance of the problem. Therefore, it is unclear and unconvincing what benefit is expected by solving the proof optimization problem.

- Some experimental setting and terminology are unclear (see the following questions).

Typos:

- l35: precision --> imprecision

---

confidence: 4
contribution: 4
initial_rating: 5
presentation: 4
questions: Idle musing, feel free to ignore: Do you have thoughts about the ceiling/floor of your proposed metrics - are there degenerate solutions? In particular, could `we evaluate this using the ratio of number of explicitly typed have tactics to total number of tactic invocations.` incentivize the model to generate a lot of superfluous `have` tactics to inflate this metric?
soundness: 4
strengths: The authors frame an interesting and potentially very impactful problem, propose a smart solution, and execute on that solution well. The paper is well-written and the results appear convincing to me.
summary: Authors are studying whether LLMs can optimize formal math proofs for additional criteria besides correctness, such as length and readability. They find that naively applying LLMs don’t perform great at this task, but that multiple interventions like augmenting the formal proof with comments, adding relevant context via retrieval, or selecting the best of N solutions, substantially improves performance. Finally, they ablate these interventions and find that each contributes substantially to the overall performance.
weaknesses: The authors could mention interactive proofs / prover-verifier games (https://arxiv.org/abs/2108.12099), where LLMs are trained to write informal math proofs to be maximally legible to an independent verifier, as related work.

I believe the caption of Figure 1 should read (left) instead of (right)?

For reproducibility, the authors should mention the exact version of GPT-4o they used for their experiments (gpt-4o-2024-08-06 ?)

I’m taking it on trust that “readability” defined as in the paper is a sensible definition - to someone not familiar with Lean, the "readability-optimized" version of the proof in Figure 3 is not actually a lot easier to parse than the other version.

---

confidence: 3
contribution: 2
initial_rating: 6
presentation: 3
questions: - Could the authors elaborate further on the “flat” and “structured” formats described in Section 3.1.2 and provide examples for clarity?
- When selecting parameters in the ablation study, why was the best parameter combination chosen based on improvement rather than accuracy? Could the authors discuss the trade-offs between optimizing for improvement versus accuracy, and how this choice might impact the practical applicability of ImProver?
soundness: 3
strengths: - As the first work in proof optimization, this paper defines novel and reasonable metrics to quantify the quality of Lean proofs.
- The paper integrates several advancements from the LLM community, including proof generation, retrieval, chain of thought (CoT) reasoning, and self-correction in code generation, for optimizing proofs. The inclusion of these methods is well-motivated, and the experiments are extensive. Furthermore, ImProver achieves notable performance without using models fine-tuned specifically for proof generation, showing its significant contributions to proof synthesis and optimization.
- The open-source code is well-structured and documented, facilitating easy adoption and use by the community.
summary: The paper proposes ImProver, a framework designed to optimize proofs based on various metrics, such as shortening proof length and enhancing human readability. The authors establish several performance metrics to evaluate the quality of improvements and conduct comprehensive case studies across representative benchmark datasets for an extensive analysis.
weaknesses: While the experimental results are comprehensive, their presentation could be improved, which is particularly important for a paper focused on advancing LLM applications in proof optimization. Specifically, in Section 4.2.1 on ablation testing:

- At line 450, the term “string list” is introduced without prior definition. Could the authors clarify the relationship between "string list" and the "flat" format mentioned earlier? This would help ensure consistency in terminology throughout the paper.
- Table 5 could be clarified further. Upon cross-checking, it appears that the best/worst values are based on configurations giving the highest “improvement” scores, whereas the last row presents the best scores across all configurations. It would be helpful to explicitly state this distinction in the main text to enhance clarity.

Meta-review: This paper concerns automated proof optimization and proposes ImProver, an LLM-based approach to rewriting proofs to meet user-defined metrics in Lean. The specific metrics considered in this work are length metric, readability metric, and completion metric. ImProver introduces Chain-of-states prompting, which makes internal proof state explicitly exposed to an LLM agent, and also leverages relatively standard techniques like retrieval and sampling (best of N solutions). The experimental evaluation shows that ImProver outperforms vanilla LLM-based approaches in terms of the proposed metrics. The problem of proof optimization is a new and important research problem, and there has been little research done by the neural theorem proving community previously. This paper proposes the first solution addressing neural theorem proof optimization. There are some concerns about whether the proposed metrics are meaningful for measuring readability of proofs, and whether the optimized proofs indeed have practical benefits. The contributions made in this work overweighs these concerns, which of course deserve further follow-up research works to address.

Decision: Accept (Poster)