Library Learning Doesn’t: The Curious Case of the Single-Use “Library”

Authors: ian  berlot-attwell
frank  rudzicz
xujie  si
Venue: NeurIPS_cc_2024_Workshop_MATH-AI
Published: 2024-09-25 16:55:07

Abstract: Advances in Large Language Models (LLMs) have spurred a wave of LLM library learning systems for mathematical reasoning.  These systems aim to learn a reusable library of *tools*, such as formal Isabelle lemmas or Python programs that are tailored to a family of tasks. Many of these systems are inspired by the human structuring of knowledge into reusable and extendable concepts, but do current methods actually learn reusable libraries of tools?

  We study two library learning systems for mathematics which both reported increased accuracy: LEGO-Prover and TroVE. We find that function reuse is extremely infrequent on miniF2F and MATH. Our followup ablation experiments suggest that, rather than reuse, self-correction and self-consistency are the primary drivers of the observed performance gains. Our code and data are available at https://github.com/ikb-a/curious-case.

Main paper: 
 introduction: 
 Mathematical progress is made by building with, and building upon, the tools of those who came before. Consequently, it is no surprise that there is research interest in developing systems that can automatically learn such reusable mathematical tools. Recently, LLMs have enabled new toollearning methods with improved performance [Wang et al., 2024a ,b, Zhang et al., 2024a , Yuan et al., 2024] -but are these systems truly learning generalized, reusable knowledge or is performance improved through other mechanisms? In this work, we study two prior systems: LEGO-Prover which aims to learn reusable formal Isabelle lemmas, and TroVE which aims to learn reusable Python functions. For both, our analysis of the model's behaviour reveals that direct reuse is negligible. Furthermore, we perform two ablation studies supporting our position that function reuse plays a limited role in these systems' improved mathematical reasoning. 
related work: 
 LLM library learning, i.e., creating and reusing tools, depends on LLMs' ability to use tools. Prior evaluations of tool-use (typically assuming tools as REST APIs) [Qu et al., 2024] included real-world queries [Yan et al., 2024] , dedicated test environments [Li et al., 2023] , and metrics ranging from LLM-as-a-judge [Guo et al., 2024] to tracking task-checkpoint completion [Lu et al., 2024] .Table 1 : Lemma reuse in LEGO-Prover released logs. Note that lemma reuse is very uncommon, and no lemma reused twice. For each split, we report the number of problems solved, the number of unique lemmas occurring in the PROVER's input prompts, the number of lemmas reused verbatim once, or more than once, and the number of lemmas whose name is reused once, or more than once. A lemma is reused N times if it appears in N + 1 solutions (i.e., the initial use, and then N reuses).Problems Solved Lemmas in Prompts 1 2+ 1 2+ valid+GPT 127 374 0 0 1 0 valid+Human 135 265 0 0 1 0 test+GPT 111 255 0 0 2 0 test+Human 122 339 1 0 2 0In contrast, the evaluation of library learning systems has been limited. Accuracy is the metric of choice [Wang et al., 2024a ,b, Zhang et al., 2024a , Yuan et al., 2024] , but cannot capture the extent or quality of reuse: an excellent library is useless to a weak reasoner, and a powerful reasoner can ignore a useless library and derive results from first principles. Prior attempts to evaluate library learning have been limited to static measures of individual functions such as cyclomatic complexity [McCabe, 1976 , Zhang et al., 2024a] and abstract syntax tree depth [Wang et al., 2024b] , or have answered specific questions such as the ease of human verification [Wang et al., 2024b] , accuracy under domain transfer [Zhang et al., 2024a , Qian et al., 2023] , or performance in the sub-problem of refactoring ground truth solutions [Lin et al., 2024] .In this study, we evaluate two library learning systems for mathematical reasoning: LEGO-Prover, and TroVE (see Sections 2.1 and 2.2). For a review of library learning systems, see Appendix A.LEGO-Prover consumes a set of proposed theorems to produce corresponding formal Isabelle [Paulson, 1994] proofs. It was evaluated on the miniF2F [Zheng et al., 2022] dataset: each problem was attempted 100 times, and the system obtained feedback from the Isabelle verifier after each attempt. LEGO-Prover was designed to perform library learning. Using the term skills in place of tools, Wang et al. [2024a] claimed that "LEGO-Prover enables LLMs to utilize existing skills retrieved from the library" and "[m]odular and reusable skills are constantly added to the library to enable tackling increasingly intricate mathematical problems." LEGO-Prover performs library learning via two LLM systems: 1) The PROVER which uses the library to create proofs, and 2) the EVOLVER which iteratively refines the library. They communicate through shared databases, such as the request db which stores proposed lemmas to be proven and added to library.TroVE is a "method for inducing a toolbox of reusable functions to use in solving programmatic tasks," designed to receive a stream of word problems without a ground truth or verifier [Wang et al., 2024b] . For each problem, it attempts to produce a Python program that prints the correct solution.TroVE's mathematical reasoning was evaluated with the MATH dataset Hendrycks et al. [2021] .Each problem is considered once: an LLM generates 15 solutions, and the best is selected based on self-consistency (i.e., majority vote) [Wang et al., 2023] . In generation, 5 solutions ignore the library and directly generate a program (SKIP mode), 5 create a reusable helper function for inclusion in the library (CREATE mode), and 5 use a function from the library (IMPORT mode). 
analysis of lego-prover: 
 We begin by analyzing the publicly released LEGO-Prover evaluation log files1 [Wang et al., 2024a] . These logs are a subset of the unreleased PROVER logs corresponding to the final attempts on the successfully solved problems. Note that LEGO-Prover was evaluated on 4 data splits, and learned over 20,000 lemmas overall [Wang et al., 2024a] .We find that only 1,233 lemmas (∼6%) are used in the final solving step (i.e., are inputs to the PROVER). Of these, exactly one lemma is reused by the PROVER, and it is reused once (i.e., appears verbatim in two solutions). As the PROVER may be adjusting a lemma (e.g., paraphrasing, commenting, etc...) we repeat the analysis, checking only for the lemma's name. Again, lemma reuse is rare, and no lemma is reused more than once (i.e., no lemma has its name appear in 3 or more solutions). See Table 1 for details. For an example of verbatim vs. name use, see Appendix B.Given these findings, there are only two possibilities by which LEGO-Prover may be performing reuse: 1) indirect reuse (e.g., the learned tools are useful, reusable exemplars, rather than directly used in the final solution), or 2) direct reuse occurs in the EVOLVER.Instead, we hypothesize that reuse is not significantly boosting performance. We propose that selfcorrection [Pan et al., 2023] via the request db is the main mechanism of action. Note that the PROVER populates the request db by: 1) adding lemmas that the LLM suggests may be helpful sub-steps, and 2) adding lemmas from solution attempts that Isabelle could not verify. The EVOLVER uses the request db to modify existing tools to "aid in solving requests", and to "resolv[e] decomposed sub-goals" using the library [Wang et al., 2024a] . Thus, the performance gains may be due to a combination of chain-of-thought [Wei et al., 2022] (through the PROVER's proposal of helpful lemmas for the EVOLVER to solve) and self-correction (through the EVOLVER's retrying of failed lemmas).To test whether any form of reuse is increasing performance, we ablate LEGO-Prover to remove cross-problem sharing: each theorem is solved with its own independent state and databases. E.g., in place of a global request db, each problem now has its own independent request db. We evaluate on a random size 12 subset of the validation split and use 50 attempts per problem. We perform our ablation using OpenAI's GPT-4o-mini as the original results were published using now deprecated versions of GPT-3.5-Turbo; see Appendix E for full details of the ablation. Running 2 trials, we find that the ablation's performance is strong, solving only 1 question less than the baseline (see Figure 1 ). Studying the problems solved by only the baseline, we find that only the simplest of the input lemmas are possibly used (namely a 2 ≥ 0 and ax 2 + bx + c = 0 ⇒ c = -(ax 2 + bx); see Appendix C). It is unclear as these facts are not treated as lemmas, and are given different justifications. This suggests that: 1) the LLM may be too weak if it needs examples of basic facts 2) the LLM struggles at reuse as it does not copy the given, verified, proofs.Question: For each theoretical result, does the paper provide the full set of assumptions and a complete (and correct) proof? 
analysis of trove: 
 As TroVE logs were not released, we re-ran TroVE on MATH, achieving accuracy within ±2% (absolute) of reported (see Appendix, Table 3 ). Note that the TroVE library also learns import statements; we ignore these in our analysis for two reasons. Firstly, our interest is in whether the system learns and reuses non-trivial tools, unlike statements such as "import math" and "from sympy import symbols". Secondly, as TroVE includes the entire library as part of the IMPORT prompt, and import statements are innately simple, it is impossible to determine whether an import statement is included in the LLM output due to reuse, or the LLM's innate knowledge. Given 3 successful reuses in 3,201 test questions, we believe that TroVE's improvements over the baselines are not due to function reuse. Instead, we believe that ensembling and self-consistency are responsible. To test this, we ablate the model by disabling IMPORT mode, but maintaining the 15 solution attempts: we generate 8 solutions ignoring the library (i.e., SKIP mode) and 7 attempting to create a helper function (i.e., CREATE mode). As in the original work we use CodeLlama-7b-Instruct-hf [Rozière et al., 2023] ; see Appendix F for the full ablation details. Ablating IMPORT mode prevents reuse as the library never appears in the model's input, thus also preventing library learning of import statements. As to why this ablation could still be performant, prior work established the benefits of self-consistency and increased sampling [Brown et al., 2024] , and it's known that library-less tool-creation can boost performance by forcing abstract reasoning [Yuan et al., 2024] .We evaluate our ablated model on the intermediate_algebra test split (reportedly the largest performance gain over non-reuse baselines), and the geometry, number, and count test splits. On the intermediate_algebra, number, and count splits, our ablation exceeds the baseline's performance, with the improvement being statistically significant on two splits (See Table 2 ). On only the geometry split does the base model perform slightly better, though the learned libraries only contains import statements. From this we can conclude that library learning import statements can be slightly beneficial, but only for certain domains. Typically, TroVE's library learning degrades its performance. 
conclusions: 
 In this study, we find that both TroVE and LEGO-Prover do not directly reuse the tools they learn. Furthermore, the results of our ablations suggest that their performance gains cannot be solely attributed to indirect reuse either.We intend that this paper be a call for the better understanding of the limitations of current library learning systems, and for improved evaluation. We show that accuracy is misleading in isolation: the system's reuse behaviour is paramount, and careful ablation is critical. Both papers studied made sensible claims as the created systems were deliberately designed for library learning and were tested against ablations that were not unreasonable -however they also relied heavily on accuracy as a metric instead of directly observing the systems' use of the library, and both chose ablations that in hindsight were too aggressive. It is clear that, particularly for ablations of library learning systems, minimal changes are preferable, and considerable thought should be put into other possible causes of improvements. There is a clear need for a broadly applicable framework for the evaluation of library learning specifically; this framework must rely on more than task accuracy and ablations to evaluate library learning and reuse.Finally, considering library learning for mathematics in general: are LLMs capable learning tools and performing direct, verbatim reuse? Given that the observed improvements do not come from direct reuse, would direct reuse actually improve systems for mathematical reasoning, or is it overly brittle making soft reuse desirable? These important questions follow from our findings, and should inform the design of future research into library learning systems.Question: Does the paper provide open access to the data and code, with sufficient instructions to faithfully reproduce the main experimental results, as described in supplemental material?Answer: [Yes] Justification: As explained in the previous question on reproducibility, we release our code along with the logs analyzed. Furthermore, the core TroVE and LEGO-Prover code bases are already publicly available, and can be easily modified to implement the ablations described.Guidelines:• The answer NA means that paper does not include experiments requiring code. • Providing as much information as possible in supplemental material (appended to the paper) is recommended, but including URLs to data and code is permitted. 
limitations & broader impact: 
 Due to resource constraints, our ablation studies could be more thorough. Most obviously, we only study two models, and on two datasets. The LEGO-Prover ablation is not ideal, as library learning is disadvantaged by operating on a subset of the questions; this was necessary due to resource constraints. Another limitation is that LEGO-Prover's databases are pre-loaded with the full dataset of problems; consequently, the EVOLVERs are exposed to other problem statements -note, however, that the impact on testing reuse is minimal. Firstly, the PROVER cannot attempt to solve any of these other problems, thus the request db cannot gain pending lemmas related to other problems. Secondly, under the ablated model, tasks cannot share lemmas -any performance gains would come from having access to other sample problems instead of reuse.While we demonstrate that the performance gains in mathematical reasoning seen by TroVE and LEGO-Prover cannot be attributed to the direct learning and reuse of tools, there is a very important but subtly different question which remains unanswered: whether these systems are at all capable of library learning. It is possible that these systems have the capacity to learn reusable functions and lemmas, but the datasets do not provide the opportunity. Manually inspecting the MATH dataset, our tentative conclusion is that the dataset is intrinsically not amenable to function learning with Python -we suspect the questions are too diverse, with the shared components already being captured by standard libraries. How this could be more formally demonstrated remains an important open question that is beyond the scope of this work. This work has no immediate societal impact, rather, it highlights current limitations and challenges assumptions in this field. However, deploying tool-learning systems may carry a security risk from executing LLM-generated code (we sandboxed TroVE). More generally, library learning systems are self-improving through code generation, an approach that has raised concerns [Zelikman et al., 2023] . Unexpected behaviours may develop, thus requiring sandboxing and monitoring, at the very least. designed to interact with a specific, complex environment (e.g., Wang et al. [2024c] , Tan et al. [2024] , Wu et al. [2024] , Zhang et al. [2024a] , Zhao et al. [2024] ).Generally, such systems access the library via in-context learning (ICL); some place the entire library in the context [Wang et al., 2024b , Zhang et al., 2024a] , whereas others first use a semantic-similarity retrieval step to allow for larger libraries. Yuan et al. [2024] in particular uses a retrieval system that incorporates a LLM-generated description of the tool to be retrieved; LEGO-Prover behaves similarly by having several phases where the system alternates between proposing useful tools to be added to the library, attempting to create these tools, and possibly retrieving these tools.These systems are typically bottom-up (iteratively developing a library over time), though a handful of top-down approaches exist. These top-down approaches instead decompose a high-level description of the tasks into reusable modules [Chen et al., 2024 , Kuan et al., 2024 , Zhao et al., 2024 , Zhang et al., 2024b] ; to the best of the authors' knowledge this approach is yet to be applied to mathematical reasoning.These LLM-based systems typically attempt to produce reusable tools via ICL: prompting the LLM to generate "reusable functions". In comparison, an older family of library learning work (e.g., Dreamcoder [Ellis et al., 2021] and LILO [Grand et al., 2024] ) instead frame library learning as a matter of compression. In principle a function that compresses a set of solutions must be broadly applicable, and in practice a high-level function reduces the symbolic search space for program induction. More generally, compression has been of long standing interest in the field of artificial intelligence. Rendell [1983] defined conceptual knowledge as the ability to compress a raw space of possibilities into useful classes, and there are long-standing connections between compression and inductive reasoning. Framing inductive reasoning as the task of capturing the underlying pattern in a provided substring for the purposes of prediction, Solomonoff [1964] formalized induction as Bayesian reasoning under a prior favouring low Kolmogorov complexity. In other words, formalizing the concept of Occam's razor -that the simplest solution, that which can be highly compressed into a short description, is more likely. For a recent treatise on the value of compression, specifically within the area of mathematical reasoning, see Bengio and Malkin [2024] .Turing our attention to mathematics, deep learning in general and LLMs in particular have found broad application in theorem proving [Li et al., 2024] . Considering library learning specifically, a very closely related branch of work considers the problem of refactoring a collection of groundtruth solutions into reusable components. ATG [Lin et al., 2024] and REFACTOR [Zhou et al., 2024] train models to extract reusable formal lemmas from a provided set of ground-truth formal proofs. Similarly, ReGAL [Stengel-Eskin et al., 2024] refactors ground-truth Python solutions for the MATH dataset into a reusable library. These systems are valuable and may represent a better first step towards reusable knowledge, but their dependence on ground-truth solutions prevents them from being conventional library learning systems. In comparison, LEGO-Prover attempts to learn reusable lemmas and produce formal proofs from only formal problem statements, and informal natural language proofs -furthermore, Wang et al. [2024a] demonstrated that the latter could be automatically generated by ChatGPT with only a small degradation in system performance. In contrast, Figure 3 is an example of name use, where the name of the input lemma appears in the solution. In this case, the contents of the lemma are similar, but have significant differences. Note that an instance of verbatim use would, necessarily, also be an instance of name use.Question: Does the paper specify all the training and test details (e.g., data splits, hyperparameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?Answer: [Yes] Justification: Hyperparameters are in Sections E and F, there is no training data, and the TroVE test set is the same as Wang et al. [2024b] , and the LEGO-Prover test set a subset of that used in Wang et al. [2024a] . The exact problems used in the subset are listed in the same section as the hyperparameters.Guidelines:• The answer NA means that the paper does not include experiments.• The experimental setting should be presented in the core of the paper to a level of detail that is necessary to appreciate the results and make sense of them. • The full details can be provided either with the code, in appendix, or as supplemental material. 
experiment statistical significance: 
 Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?Answer: [Yes] Justification: For the LEGO-Prover ablation, error regions of 1 standard deviation are displayed in Figure 1 , the caption states that the source of variation is the LLM output and race conditions within the system; the method used to compute mean and standard deviation (numpy) is stated in Appendix E. For the TroVE ablation, we report the mean and standard deviation in Justification: There are no human subjects, to the best of our knowledge there are no data concerns, or immediate societal impact or harms (the possible future risks from deploying tool-learning systems, and the precautions that should be taken in future research in selfimproving systems are outlined in Section 6), and to the best of our knowledge our work is reproducible and legal. Guidelines:• The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics.• If the authors answer No, they should explain the special circumstances that require a deviation from the Code of Ethics.• The authors should make sure to preserve anonymity (e.g., if there is a special consideration due to laws or regulations in their jurisdiction). 
broader impacts: 
 Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?Answer: [Yes] Justification: We do not anticipate any immediate societal impact or harms, but we do discuss the possible future risks from deploying tool-learning systems, and the precautions that should be taken in future research in self-improving systems in Section 6.Guidelines:• The answer NA means that there is no societal impact of the work performed.• If the authors answer NA or No, they should explain why their work has no societal impact or why the paper does not address societal impact. • Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations. • The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is a direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster. • The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology. • If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how a system learns from feedback over time, improving the efficiency and accessibility of ML). 
safeguards: 
 Question: Does the paper describe safeguards that have been put in place for responsible release of data or models that have a high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?Answer: [NA] Justification: We present ablations of already publicly available models (LEGO-Prover and TroVE), neither of which we believe has a higher risk for misuse than the constituent publicly available LLM.Guidelines:• The answer NA means that the paper poses no such risks.• Released models that have a high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere to usage guidelines or restrictions to access the model or implementing safety filters. • Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images. • We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make a best faith effort.12. Licenses for existing assets • We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere to the NeurIPS Code of Ethics and the guidelines for their institution. • For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review. 
 
 Appendix: A lemma is reused N times if it is used N + 1 times -i.e., if the lemma is used in N + 1 solutions.We performed two runs of the original model, in both cases it outperformed the ablation by solving one additional problem. We present the found proofs and input lemmas in Figures 4 and 6 . For improved legibility, we also provide a typeset approximation in Figures 5 and 7 . In addition to the Step 1: Expand the expression $(xy-1)^2+(x+y)^2$ to obtain $x^2+2xy+y^2+x^2y^2-2xy+1$.Step 2: Simplify the expression to $x^2+y^2+x^2y^2+1$.Step 3: Observe that all squares are nonnegative, so the minimum value of the expression is 1.Step 4: Show that the minimum value of 1 can be achieved when $x=y=0$. ## Problems Simplify $(a-1)(a+1)(a+2) -(a-2)(a+1).$ Show that it is a^3 + a^2.Step 1: Expand the expression $(a-1)(a+1)(a+2) -(a-2)(a+1)$ by multiplying the binomials.Step 2: Simplify the expression to obtain $(a^2-1) (a+2)-(a-2)(a+1)$.Step 3: Expand further to get $(a^3 + 2a^2 -a -2) -(a^2 -a -2)$.Step 4: Combine like terms to simplify the expression to $a^3 + a^2$.Step 5: Conclude that the simplified expression is equal to $a^3 + a^2$. show ?thesis using c0 c1 c2 by simp qed end ``F igure 3: Example of name reuse by the LEGO-Prover. Only the name of the input lemma needs to be reproduced exactly in the output. In this case, the body of the input lemma has been significantly adjusted. Note Figure 2 is also an example of name reuse, as the input lemma's name appears in the solution (in that particular case, along with the rest of the lemma). See table 3 for the best-of-five accuracies reported by TroVE, and achieved by our reproduction of their results.At the time of publication, the LEGO-Prover logs released by Wang et al. [2024a] and used in our analysis are available at https://github.com/wiio12/LEGO-Prover/blob/ 357672c7751cd0c84aff6bf72a3d1bf97614e81d/result/lego_result.zip.LEGO-Prover is built on OpenAI's GPT-3.5-Turbo and the 2022 release of the Isabelle proof assistant, specifically using its abilities as a proof verifier. Note that due to the deprecation of the LLMs originally used by LEGO-Prover (gpt-3.5-turbo-0301, gpt-3.5-turbo-0613, gpt-3.5-turbo-16k, gpt-3.5-turbo-16k-0613, gpt-3.5-turbo-16k, gpt-3.5-turbo-16k-0613), we upgrade the underlying LLM from GPT-3.5-Turbo to GPT-4o-mini.We use the default LEGO-Prover hyperparameters, except for the number of retry attempts which, following Wang et al. [2024a] 's ablations, we reduce to 50. See Table 4 for details.Note that the LEGO-Prover is initialized with a seed library of tools, and our ablation retains this initialization. The core claim we aim to disprove is that the model's performance gains predominantly come from reusable lemmas, and our ablation prevents any cross-task reuse.The specific 12 problems chosen uniformly at random for our ablation study are:aime_1991_p6.json, algebra_2varlineareq_xpeeq7_2xpeeq3_eeq11_xeqn4. json, amc12a_2008_p15.json, amc12a_2013_p8.json, amc12a_2021_p7.json, amc12b_2002_p3.json, amc12b_2003_p9.json, mathd_algebra_31.json, mathd_algebra_109.json, mathd_algebra_116.json, mathd_numbertheory_149.json, and numbertheory_sqmod4in01d.json Note that LEGO-Prover requires both the problem statement, and an informal natural language proof for conversion. We use the same human-generated informal proofs as Wang et al. [2024a] . The authors bundled said informal proofs inside of the miniF2F .json files listed above, available for download from https://github.com/wiio12/LEGO-Prover/tree/ have "lhs = 0" using assms by (metis eq) thus ?thesis by (simp add: eq) qed ###### useful skill 2: ###### lemma sqrt_limit_general: fixes x :: real assumes "n > 0" "k > 0" "k = sqrt(x + k)"shows "x = k^2 -k" proofhave "k^2 = x + k" using assms(3) by (smt (verit) assms( 2 finally show ?thesis by (simp add: field_simps) qed ###### useful skill 4: ###### lemma sqrt_limit_generalized: fixes x :: real assumes "k = sqrt(x + k)" "k > 0"shows "x = k^2 -k" proofhave "k^2 = x + k" using assms by (metis add.commute real_sqrt_ge_0_iff real_sqrt_ge_zero real_sqrt_gt_0_iff real_sqrt_pow2 verit_comp_simplify1(3) zero_le_mult_iff zero_le_square)hence "x = k^2 -k" by simp thus ?thesis by auto qed Useful skill 1: ∀a, b, c, k, x ∈ R : ax 2 + bx + c = 0 ⇒ c = -(ax 2 + bx) Demonstrates: assms, simp, (metis eq), (simp add: eq) Useful skill 2:∀x ∈ R : n > 0, k > 0 k = √ x + k ⇒ x = k 2 -k Demonstrates:assms, (smt (verit) assms( 2) less eq real def real sqrt le iff real sqrt pow2 iff real sqrt zero), auto Useful skill 3:∀a, b ∈ R : √ a - √ b = (a -b)/( √ a + √ b) Demonstrates:(metis add.left cancel add cancel right right add le same cancel2 assms( 1) assms( 2) cancel comm monoid add class.diff cancel dual order.eq iff eq divide eq mult.commute nonzero mult div cancel right real sqrt eq zero cancel iff real sqrt ge 0 iff real sqrt le 0 iff real sqrt zero), (smt (verit) assms( 1) assms(2) divide cancel right real sqrt le mono real sqrt less mono real sqrt mult self square diff square factored), (simp add: field simps) have "?E = 1" when "x = 0" and "y = 0" using that by auto (* Step 5: Conclude that the least possible value of \( E \) is \( 1 \). *) thus ?thesis by sos qed (* formal statement copy from the input *) theorem amc12a_2021_p7: fixes x y ::real shows "1 \<le> ((x * y) -1)^2 + (x + y)^2" apply (auto simp:algebra_simps power2_eq_square) using expression_nonneg by sos end Figure 6 : LEGO-Prover input lemmas (left) and found proof (right). The proof proves that ∀x, y ∈ R : 1 ≤ (xy -1) 2 + (x + y) 2 . See Figure 7 for a typeset approximation, and commentary of LEGO-Prover's use (and failure to use) the input lemmas.Useful skill 4: ∀x ∈ R : k = √ x + k, k > 0 ⇒ x = k 2 -2 -13x + k = 0 k = 13x -2x 2 Method: simp x 2 = ((13 - √ 131)/4) 2 Method: blast x 2 = (13 - √ 131) 2 /Output Proof Useful skill 1: ∀a ∈ R : a 2 ≥ 0 Demonstrates: (simp add: power2 eq square), (simp add: mult nonneg nonneg) Useful skill 2: ∀a ∈ R : a 2 ≥ 0 Demonstrates: sos, auto Useful skill 3: ∀x, y ∈ R : x 2 + y 2 ≥ 0 Demonstrates: simp Useful skill 4: ∀x, y ∈ R : x 2 + y 2 ≥ 0 Demonstrates: auto, (simp add: add nonneg nonneg), simp Define Lemma expression nonneg:∀x, y ∈ R : (xy -1) 2 + (x + y) 2 ≥ 1 Proof of Lemma: Let E = (xy -1) 2 + (x + y) 2 (xy -1) 2 = (x 2 y 2 -2xy + 1) (x + y) 2 = x 2 + 2xy + y 2 E = (x 2 y 2 -2xy + 1) + (x 2 + 2xy + y 2 ) E = x 2 y 2 + x 2 + y 2 + 1 Method: sos x 2 y 2 ≥ 0 x 2 ≥ 0 y 2 ≥ 0 Method: auto E ≥ 1 Method: sos E = 1 when x, y = 0 Method: autoLemma expression nonneg follows using method sos Define theorem amc12a 2021 p7: ∀x, y ∈ R : 1 ≤ (xy -1) 2 + (x + y) 2 Proof: Follows Lemma. Method: sos, applying (auto simp:algebra simps power2 eq square) 2Figure 7 : Typeset approximation of LEGO-Prover input lemmas (left) and found proof (right). See Figure 6 for the original Isabelle lemmas and proof. The proof proves that ∀x, y ∈ R : 1 ≤ (xy -1) 2 + (x + y) 2 . Skills 1 and 2 are the same; the fact that x 2 ≥ 0 is used, though the exact proof differs from the lemmas. Skills 3 & 4 are also the same, though they do not seem to be used. 357672c7751cd0c84aff6bf72a3d1bf97614e81d/data/full_data/valid at the time of publication.Note that the mean and standard deviation in Figure 1 are calculated using Python 3.8.9, numpy 1.22.2, numpy.mean() and numpy.std().Our experiments were run on an internal cluster, running one trial at a time. Each trial used 180 GB of RAM, 50 CPU cores, OpenAI credits, and ran within 24 hours. We upper bound the total compute time required to run our LEGO-Prover experiments at 96 hours. The full project required more compute than the experiments reported as one trial failed due to an out-of-memory error. Based on Wang et al. [2024a] 's estimate of $300 per trial, we estimate the cost in OpenAI credits of our experiments to be $7.38 per trial as we run half the number of attempts and one twentieth the number of questions. Under this estimate, the total cost of all our experiments is ∼$30.Our code is modified from the released LEGO-Prover code base, available at https://github. com/wiio12/LEGO-Prover [Wang et al., 2024b] , released under an MIT License. Evaluation is done using the miniF2F Zheng et al. [2022] dataset, available at https://github.com/openai/ miniF2F/tree/main, which was released under the Apache License Version 2.0.Our code is documented and released, alongside the generated LEGO-Prover logs. It is a minor modification to the existing code base, and there is no training stage or new limitations. The code is released under the same license as the parent repository.TroVE uses CodeLlama-7b-Instruct-hf [Rozière et al., 2023] interacting with the Python3 interpreter. We use the hyperparameters specified in the paper, outlined in Table 5 . The same hyperparameters are used for the ablation, and our reproduction of baseline TroVE.The mean and standard deviation of our 5 experiment runs are reported in Table 2 . They are calculated using Python 3.8.9, numpy 1.22.2, numpy.mean() and numpy.std(). The 2-sided t-test reported the Our experiments were run on an internal cluster, running up to 4 trials at once. Each trial used 1 Nvidia A40 GPU, 64 GB of RAM, 16 CPU cores, and ran within 12 hours. Smaller datasets completed more quickly. We upper bound the total compute time required to run our TroVE experiments at 480 hours.The full project required more compute than the experiments reported as we also tried running TroVE with quantized CodeLlama, CodeLlama 13B and 70B, and GPT-4o-mini.Our code is modified from the released TroVE code base, available at https://github.com/ zorazrw/trove [Wang et al., 2024b] , which was released under the CC-BY-SA-4.0 license. Evaluation is done using the MATH Hendrycks et al. [2021] dataset, available at https://github.com/ hendrycks/math, which was released under an MIT License.Our code is documented and released, alongside the generated TroVE logs. It is a minor modification to the existing code base, and there is no training stage or new limitations. The code is released under the same license as the parent repository.We also ran baseline TroVE using the larger CodeLlama 13B model, and found similar results with very little direct function use. The key difference with the 7B model was that a single function was learned for the geometry split, but it was never reused in a correct solution.We also attempted to run baseline TroVE using the 70B model, however we discarded the results as the LLM's ethical safeguards were frequently tripped (e.g., giving reasons such as "it is not appropriate or ethical to provide assistance with academic assignments or graded exercises").NeurIPS Paper Checklist Guidelines:• The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper. • The authors are encouraged to create a separate "Limitations" section in their paper.• The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be. • The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on a few datasets or with a few runs. In general, empirical results often depend on implicit assumptions, which should be articulated. • The authors should reflect on the factors that influence the performance of the approach.For example, a facial recognition algorithm may perform poorly when image resolution is low or images are taken in low lighting. Or a speech-to-text system might not be used reliably to provide closed captions for online lectures because it fails to handle technical jargon. • The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size. • If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness. • While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, a worse outcome might be that reviewers discover limitations that aren't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an important role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.38th Conference on Neural Information Processing Systems (NeurIPS 2024).https://github.com/wiio12/LEGO-Prover/blob/357672c7751cd0c84aff6bf72a3d1bf97614e81d/ result/lego_result.zip 



Reviews: review: title: title: Very good paper provide a critical view on two prior work on library learning for math problem solving
main_review: main_review: The paper investigates the role of library reuse in two prior works, LEGO-prover for mini2f and TroVE for MATH, and found that there is actually very little library reuse in the logs or their reproduced runs. Furthermore, they show that they can ablate the model by removing the library reuse components and still get roughly equal or better performance in the case of TroVE. This demonstrates that the performance gains of the two prior works can be achieved without library reuse. The paper (1) provides concrete evidence that little library reuse occurs in the two prior works by examining the provided logs or reproduced runs, and (2) ablates the model while still achieving competitive performance, showing that the gain may not come from library reuse at all but the self-consistency and the helper function style or problem decomposition methods. This work provides a critical and important investigation into library learning for math problem-solving.
Typo correction: line 69 lemm -> lemma
title: title: Important new findings and insights in library learning systems
main_review: main_review: Summary: 
The paper studies two library learning systems and introduces new findings suggesting that function reuse is extremely infrequent on miniF2F and MATH. Through ablation experiments, the authors further suggest that the primary drivers of the observed performance gains are self-correction and self-consistency, rather than function reuse.

Strengths:
- New, important findings that could have a significant impact on future research. 
- The ablation experiments provide valuable insights into what contributes to improved performance in these library-learning systems.

Opportunities for improvement:
- The authors could mention which underlying LLM was used for the ablations in the main part of the paper. They could also discuss the impact of the underlying LLM and conduct experiments with different model sizes to assess whether function reuse could be beneficial for certain models.

Final remark:
The paper presents strong, impactful findings with clear evidence that self-correction and self-consistency are key factors in performance gains, rather than function reuse. Given the importance of these results and the clear writing style, I opt for a rating of 8.
title: title: Review
main_review: main_review: # Summary

The paper examines the claims that "library learning largely improves performance" made respectively by two previous works, LEGO-Prover and TROVE as a math problem solver, and finds out:

1. Lemma/Tool reuse rarely occurs in solutions generated by these 2 prover/math problem solvers
2. There is little to no effect of ablating reuse on the performance of these 2 prover/math problem solvers

# Strengths

## Originality

The paper identifies a potentially unsound claim in prior works that was overlooked. It would have been great if the prior works had included their own ablation studies to attribute and explain the performance gain.

## Quality

Results of the ablation experiments are convincing.

## Clarity

The paper gives a friendly summary of LEGO-Prover and TROVE, and clear descriptions of the ablation experiments.

## Significance

The paper serves as a message to the community encouraging researchers to conduct thorough ablation studies on their own work. More importantly, as mentioned in the paper, the ablation studies are constrained by available resources (original log for TROVE, the set of the ablation test set, etc.), so it should be read, discussed, and even challenged by more people, especially authors of the two prior works.


# Weaknesses

## Quality

1. It would be better to include a comparison between LEGO-Prover/TROVE and the cases where tool re-usage is the key to performance gain. **In what ways are they different such that their attributions of performance gain differ? In what ways are they similar such that the original authors believed that tool reuse was the key factor?** Answers to these questions will help further researchers avoid certain pitfalls and design systems that better leverage library learning.

2. **Do the problems in MiniF2F and MATH really require reuse? What if they are just so diverse that previously discovered lemma/tool is rarely applicable?** While the answer to this question won't change the observation that the 2 prior works may have overstated the contribution of reuse in their tasks, it will provide the 2 prior works a fair assessment of the effectiveness of their library learning modules.  For example, if there are only 5% of the problems that can benefit from reuse, then a 4% reuse rate shouldn't be considered low.


# Questions
 
1. Following up on bullet point 2 of Weaknesses, here is a slightly beyond-the-scope, but more important question about the evaluation process of all library learning papers: **If not MiniF2F/MATH, what's a good evaluation benchmark for library learning systems? How can we ensure enough data diversity and enough occurrences of reuse at the same time?**