LLM Library Learning Fails: A LEGO-Prover Case Study

• URL: http://arxiv.org/abs/2504.03048v1
• Date: Thu, 03 Apr 2025 21:53:51 GMT
• Title: LLM Library Learning Fails: A LEGO-Prover Case Study
• Authors: Ian Berlot-Attwell, Frank Rudzicz, Xujie Si,
• Abstract summary: We investigate LEGO-Prover, which purports to learn reusable lemmas for mathematical reasoning.<n>We find no evidence of the direct reuse of learned lemmas, and find evidence against the soft reuse of learned lemmas.<n>Our findings suggest that serious misconceptions exist as to the effectiveness of these techniques.
• Score: 20.25809428140996
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Recent advancements in the coding, reasoning, and tool-using abilities of LLMs have spurred interest in library learning (i.e., online learning through the creation, storage, and retrieval of reusable and composable functions, knowledge, checklists, or lemmas). Such systems often promise improved task performance through the automatic creation of broadly applicable tools, as well as superior computational performance through the caching of reasoning (i.e., the storage of generated tools). However, we find strong reason to be skeptical. We perform a deep dive into one such system, LEGO-Prover, which purports to learn reusable lemmas for mathematical reasoning. We find no evidence of the direct reuse of learned lemmas, and find evidence against the soft reuse of learned lemmas (i.e., reuse by modifying relevant examples). Crucially, we find that LEGO-Prover does not in fact improve over the simple baseline of prompting the model - the improvements in task accuracy vanish once computational cost is accounted for. Our findings suggest that serious misconceptions exist as to the effectiveness of these techniques, that a serious re-examination of the state of LLM-based library learning is required, and that we require much stronger standards for evaluation including behavioural analysis and ensuring that an equal computational budget is used for baselines.

Related papers

• R1-Searcher: Incentivizing the Search Capability in LLMs via Reinforcement Learning [87.30285670315334]
  textbfR1-Searcher is a novel two-stage outcome-based RL approach designed to enhance the search capabilities of Large Language Models. Our framework relies exclusively on RL, without requiring process rewards or distillation for a cold start. Our experiments demonstrate that our method significantly outperforms previous strong RAG methods, even when compared to the closed-source GPT-4o-mini.
  arXiv  Detail & Related papers  (2025-03-07T17:14:44Z)
• General Reasoning Requires Learning to Reason from the Get-go [19.90997698310839]
  Large Language Models (LLMs) have demonstrated impressive real-world utility.<n>But their ability to reason adaptively and robustly remains fragile.<n>We propose disangling knowledge and reasoning through three key directions.
  arXiv  Detail & Related papers  (2025-02-26T18:51:12Z)
• A Framework for Using LLMs for Repository Mining Studies in Empirical Software Engineering [12.504438766461027]
  Large Language Models (LLMs) have transformed Software Engineering (SE) by providing innovative methods for analyzing software repositories. Our research packages a framework, coined Prompt Refinement and Insights for Mining Empirical Software repositories (PRIMES) Our findings indicate that standardizing prompt engineering and using PRIMES can enhance the reliability and accuracy of studies utilizing LLMs.
  arXiv  Detail & Related papers  (2024-11-15T06:08:57Z)
• Library Learning Doesn't: The Curious Case of the Single-Use "Library" [20.25809428140996]
  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 experiments suggest that, rather than reuse, self-correction and self-consistency are the primary drivers of the observed performance gains.
  arXiv  Detail & Related papers  (2024-10-26T21:05:08Z)
• LLMs Are In-Context Bandit Reinforcement Learners [30.192422586838997]
  Large Language Models (LLMs) excel at in-context learning (ICL), a supervised learning technique that relies on adding annotated examples to the model context.<n>We investigate a contextual bandit version of in-context reinforcement learning (ICRL), where models learn in-context, online, from external reward, instead of supervised data.
  arXiv  Detail & Related papers  (2024-10-07T17:45:00Z)
• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  Large language models (LLMs) struggle with consistent and accurate reasoning. LLMs are trained primarily on correct solutions, reducing their ability to detect and learn from errors. We propose a novel collaborative method integrating Chain-of-Thought (CoT) and Program-of-Thought (PoT) solutions for verification.
  arXiv  Detail & Related papers  (2024-10-05T05:21:48Z)
• Optimized Feature Generation for Tabular Data via LLMs with Decision Tree Reasoning [53.241569810013836]
  We propose a novel framework that utilizes large language models (LLMs) to identify effective feature generation rules. We use decision trees to convey this reasoning information, as they can be easily represented in natural language. OCTree consistently enhances the performance of various prediction models across diverse benchmarks.
  arXiv  Detail & Related papers  (2024-06-12T08:31:34Z)
• LLM Inference Unveiled: Survey and Roofline Model Insights [62.92811060490876]
  Large Language Model (LLM) inference is rapidly evolving, presenting a unique blend of opportunities and challenges. Our survey stands out from traditional literature reviews by not only summarizing the current state of research but also by introducing a framework based on roofline model. This framework identifies the bottlenecks when deploying LLMs on hardware devices and provides a clear understanding of practical problems.
  arXiv  Detail & Related papers  (2024-02-26T07:33:05Z)
• How Can LLM Guide RL? A Value-Based Approach [68.55316627400683]
  Reinforcement learning (RL) has become the de facto standard practice for sequential decision-making problems by improving future acting policies with feedback. Recent developments in large language models (LLMs) have showcased impressive capabilities in language understanding and generation, yet they fall short in exploration and self-improvement capabilities. We develop an algorithm named LINVIT that incorporates LLM guidance as a regularization factor in value-based RL, leading to significant reductions in the amount of data needed for learning.
  arXiv  Detail & Related papers  (2024-02-25T20:07:13Z)
• Efficient Tool Use with Chain-of-Abstraction Reasoning [63.08202389132155]
  Large language models (LLMs) need to ground their reasoning to real-world knowledge.<n>There remains challenges for fine-tuning LLM agents to invoke tools in multi-step reasoning problems.<n>We propose a new method for LLMs to better leverage tools in multi-step reasoning.
  arXiv  Detail & Related papers  (2024-01-30T21:53:30Z)
• Self-Checker: Plug-and-Play Modules for Fact-Checking with Large Language Models [75.75038268227554]
  Self-Checker is a framework comprising a set of plug-and-play modules that facilitate fact-checking. This framework provides a fast and efficient way to construct fact-checking systems in low-resource environments.
  arXiv  Detail & Related papers  (2023-05-24T01:46:07Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.