ImProver: Agent-Based Automated Proof Optimization

Thank you for your review and your feedback on our paper. We have taken this into account to improve the quality and rigor of our work. Attached below is a point-by-point response to your comments and questions.

1. Terminology and Presentation

Could the authors clarify the relationship between "string list" and the "flat" format mentioned earlier?

Could the authors elaborate further on the “flat” and “structured” formats described in Section 3.1.2 and provide examples for clarity?

We have clarified terms like “string list” and “flat format” to ensure consistent usage of such terms throughout the paper. Namely, a “flat” format is equivalent to outputting a “string list,” and a “structured” format is equivalent to a “string tree”. For example, a "string list" would be of the general form ["tactic 1", "tactic 2", ...], whereas a "string tree" would be of the general form:

[("tactic 1", [
	("tactic 1a",[...]), 
	("tactic 1b",[...]), 
	...]
 ), 
 ("tactic 2", [...])
...]

2. Experimental Clarity

It would be helpful to explicitly state this distinction in the main text to enhance clarity.

When selecting parameters in the ablation study, why was the best parameter combination chosen based on improvement rather than accuracy? [...]

The ablation process and the “improvement”-based selection have been explicitly justified and clarified in our revision (section 4.1.1) to account for the reviewer’s feedback and ensure a clear presentation of our experimental process.

Specifically, we justify the use of the improvement score for the selection of the “best” parameter combination or model, as this improvement score represents the expected improvement in the metric score – accounting for possible errors in the generation. This is preferable to the other possible performance metrics, such as accuracy, as it prioritizes both correctness, as well as large improvements in metric scores. Indeed, improvement penalizes incorrect generations and adds additional weight to greater improvements in the metric score, whereas accuracy and nonzero accuracy solely describe the correctness of generations. This is useful in benchmarking the improvements of generation abilities between the base model and ImProver. Conversely, nonempty improvement ignores incorrect submissions, describing the ability of the model to improve a given theorem, assuming correct generations. Improvement amalgamates all of this, rewarding correct and significant improvements and discouraging incorrect generations.

Thank you for your suggestions, comments, and feedback. We deeply appreciate your review and have attached below a full response to your questions and feedback.

1. Related Work

The authors could mention interactive proofs/prover-verifier games

As per the reviewer’s suggestion, we have added a greater elaboration in the Related Work section, including a discussion on interactive proofs and prover-verifier games, noting that Lean constitutes a sound verifier in the context of Interactive Proof Systems.

2. Figure

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

We have revised the caption to fix the error and any other obfuscations.

3. GPT Version

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

In our revision, we have now included the GPT version explicitly in our initial description of ImProver (Section 4.1).

4. Readability and Degenerate Solutions

I’m taking it on trust that “readability” defined as in the paper is a sensible definition

We appreciate the feedback on the intuitiveness of our readability metric, as the concept of what constitutes a "readable" proof is quite complex and isn't so simple as to be defined as a simple ratio of have tactics. Indeed, when initially defining readability in section 3.1, we wrote that readability is defined as the declarativity of the proof -- a notion that doesn't perfectly align with the intuition of what constitutes a readable proof.

As such, to ensure clarity on this point, we have renamed the “readability metric” to the “declarativity metric”, which has a more objective definition as per [1, 2] that is well-modeled by the ratio-based scoring function. We’ve additionally included side-by-side examples of proofs written in a declarative and non-declarative style to qualitatively describe the metric (these examples are a subset of the examples forwarded to the model itself). We justify this change by the definition of the readability metric , and note that as the model prompt [Appendix A.2] itself is unchanged by this renaming, this change is purely syntactic, and has no effect on the model behavior.

[...] Are there degenerate solutions?

Your concern for degenerate solutions is quite valid. We acknowledge that the metric is simplistic and subject to potential gaming (e.g., through excessive use of have tactics). However, it serves as a starting point for exploring proof optimization capabilities. We have added clarifications that the tested metrics are simplistic in definition and designed to evaluate the model’s adaptability and performance, with the intention of extending this work to more nuanced metrics.

Moreover, in our revised submission, we explicitly discuss how examples guide the model in avoiding trivial solutions, such as the superfluous have tactics you mentioned. Although this empirically generates data that is free of these degenerate solutions, there is an underlying issue of scalability with this multi-shot based methodology, as for more complex metrics, large example sets become harder to construct and the possible edge cases where a degenerate solution may occur increases. To account for this, we discuss incorporating LLM-based scoring into metrics, which is natively supported in the ImProver framework.

References:

[1] Serge Autexier and Dominik Dietrich. A tactic language for declarative proofs. In Matt Kaufmann and Lawrence C. Paulson (eds.), Interactive Theorem Proving, pp. 99–114, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg.

[2] Freek Wiedijk. Formal proof sketches. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani (eds.), Types for Proofs and Programs, pp. 378–393, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. ISBN 978-3-540-24849-1.

We greatly appreciate your feedback and comments on our submission. We have made revisions based on this feedback, and have included below a response to each of your comments and questions.

1. Importance of Proof Optimization

[...] Therefore, it is unclear and unconvincing what benefit is expected by solving the proof optimization problem.

We have expanded the introduction to provide a more compelling argument for the value of proof optimization, supported by explicit references and applications to education, research, and training machine learning models.

Specifically, we discuss the utility of proof optimization for increasing the understanding and decreasing external dependencies for better maintainability [1] for large libraries like Mathlib, as well as creating well-structured datasets for training ML models. Additionally, since the original submission, ImProver has shown to be invaluable for both these applications – having already made contributions to public Lean datasets (references removed for anonymity, but will be included in a final camera-ready version) – as well as currently being used to fine-tune and apply policy optimization for building a powerful neural theorem proving model.

2. Diversity in Best-of-N Outputs

I think it is important to incorporate some kind of random in using the best-of-n technique.

In our revision, we clarify in the experimental setup (Section 3.2.3) that temperature settings are used to ensure diverse outputs during the best-of-N selection process.

3. Input Format

Can you provide a detailed description of the input format for ImProver and GPT-4o in the experiment?

We have added a detailed description of the input formats for ImProver and GPT-4o, including examples to appendix A.1 and section 4.1. Note that the original proof is always included in the input prompt, as well as all relevant contextual information – although the ImProver prompt is heavily augmented with additional information such as dependencies, RAG, and chain-of-states.

4. Modular Proofs

Can you provide a clear definition of 'modular' in the paper?

We acknowledge that the “modularity” of a proof was not adequately defined, as it was intended as an alias for readability and declarativity. We have revised this to consistently describe the notion as “declarative” throughout the submission, as well as properly describe and give side-by-side comparisons of declarative and nondeclarative proofs [Appendix A.3].

5. Efficient Proofs

What does the paper mean by efficient proofs?

We acknowledge that the notion of “efficient proofs” was subjective and poorly defined, and was moreover redundant to the description of the Mathlib dataset as having concise and generalized proofs. The claim of “efficient” proofs has since been removed, now simply describing the proofs within Mathlib as being concise and generalized with many external dependencies.

References:

[1] https://leanprover-community.github.io/contribute/index.html

(1/2) Thank you for your in-depth feedback and review of our work. It has been incredibly helpful in improving the robustness and clarity of our paper. Below is a point-by-point response to each of your questions and comments.

1a. Readability Metric:

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.

We appreciate the reviewer's concern about the complexity of defining readability, and acknowledge that defining a readability metric in its full generality is more complex than the ratio of “have” tactics, involving many subjective and stylistic factors that may be difficult to quantify. Indeed, the goal of many formalizers is to generate “efficient” or “elegant” proofs – metrics that are exceedingly difficult to define and quantify, and therefore difficult to optimize for with a simple function.

However, as building good metrics is left as a user-level task, we take advantage of the fact that in applications where proofs need to be optimized to some specific standard, a general measure of a “readable” or “efficient” proof is not necessary, as we simply need to conform to some more strictly defined notion of what the optimal proof style is. For example, in training ML models on Lean data, it is valuable to explicitly construct the proof argument and structure in a declarative manner, and in making large libraries like Mathlib, it is valuable to have proofs be as concise as possible and use dependencies (lemmas) from the library rather than internal subproofs (haves).

With this in mind, we acknowledge that the metric is simplistic and subject to potential gaming (e.g., through excessive use of have tactics). However, it serves as a starting point for exploring proof optimization capabilities. We have added clarifications that the tested metrics are simplistic in definition and designed to evaluate the model’s adaptability and performance, with the intention of extending this work to more nuanced metrics. Additionally, we are currently testing an additional metric based on the number of external dependencies of an inputted proof, which we hope to include in the next revision by the end of the discussion period to better highlight the proof optimization capabilities of ImProver over arbitrary metrics.

Moreover, to ensure clarity on this point, we have renamed the “readability metric” to the “declarativity metric”, which has a more objective definition as per [1, 2] that is well-modeled by the ratio-based scoring function. We’ve additionally included side-by-side examples of proofs written in a declarative and non-declarative style to qualitatively describe the metric (these examples are a subset of the examples forwarded to the model itself). We justify this change by the definition of the readability metric , and note that as the model prompt [Appendix A.2] itself is unchanged by this renaming, this change is purely syntactic, and has no effect on the model behavior.

Additionally, we have further emphasized the flexibility of our approach, empowering users to define their own metrics and incorporating LLM-based scoring. This facilitates experimentation with complex, human-intuitive definitions of readability.

1b. Degenerate Solutions:

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 potential for degenerate solutions is a valid concern. In our revised submission, we explicitly discuss how examples guide the model in avoiding trivial solutions, such as generating excessive have tactics in the declarativity metric. Although this empirically generates data that is free of these degenerate solutions, there is an underlying issue of scalability with this multi-shot based methodology, as for more complex metrics, large example sets become harder to construct and the possible edge cases where a degenerate solution may occur increases. To account for this, we discuss incorporating LLM-based scoring into metrics, which is natively supported in the ImProver framework.

Thank you again to all reviewers for your suggestions and feedback on our work. We have now submitted a new revision containing the results of the aforementioned "ongoing experiments". We look forward to your feedback and discussion on how to continue to ensure the robustness and quality of our work. We also have attached point-by-point responses to reviewer comments that are relevant to the changes made in this revision.

Revisions

• Implemented and tested a "mixed metric" which is a more complex metric that aims to optimize for both length and declarativity at the same time.
• Tested ImProver's theorem proving performance on MiniF2F
• Moved all qualitative results to appendix B.3

Edits

For the sake of transparency, we note that the previous comment has been edited; initially we intended to implement a dependency metric rather than a mixed metric, but after more reflection between the two, we changed our minds to implement the latter. Dependency is certainly a valuable problem to tackle, and we plan to pursue it in more detail in future works. However, for this paper, we believe that reviewer 5mDw's suggestion of a mixed metric is more relevant and useful. Additionally, our initial plans for testing theorem proving was to use the miniCTX benchmark, but we have revised to now use the miniF2F benchmark instead.