Steering LLMs for Formal Theorem Proving

• URL: http://arxiv.org/abs/2502.15507v4
• Date: Sat, 21 Jun 2025 05:24:27 GMT
• Title: Steering LLMs for Formal Theorem Proving
• Authors: Shashank Kirtania, Arun Iyer,
• Abstract summary: Large Language Models (LLMs) have shown promise in proving formal theorems using proof assistants like Lean.<n>We observe that the LLM is capable of predicting the correct tactic; however, it faces challenges in ranking it appropriately within the set of candidate tactics.<n>We use activation steering to guide LLMs responses to improve the generations at the time of inference.
• Score: 0.29465623430708915
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large Language Models (LLMs) have shown promise in proving formal theorems using proof assistants like Lean. However, current state of the art language models struggles to predict next step in proofs leading practitioners to use different sampling techniques to improve LLMs capabilities. We observe that the LLM is capable of predicting the correct tactic; however, it faces challenges in ranking it appropriately within the set of candidate tactics, affecting the overall selection process. To overcome this hurdle, we use activation steering to guide LLMs responses to improve the generations at the time of inference. Our results suggest that activation steering offers a promising lightweight alternative to specialized fine-tuning for enhancing theorem proving capabilities in LLMs, particularly valuable in resource-constrained environments.

Related papers

• LLM Post-Training: A Deep Dive into Reasoning Large Language Models [131.10969986056]
  Large Language Models (LLMs) have transformed the natural language processing landscape and brought to life diverse applications. Post-training methods enable LLMs to refine their knowledge, improve reasoning, enhance factual accuracy, and align more effectively with user intents and ethical considerations.
  arXiv  Detail & Related papers  (2025-02-28T18:59:54Z)
• LLM-Powered Preference Elicitation in Combinatorial Assignment [17.367432304040662]
  We study the potential of large language models (LLMs) as proxies for humans to simplify preference elicitation (PE) in assignment.<n>We propose a framework for LLM proxies that can work in tandem with SOTA ML-powered preference elicitation schemes.<n>We experimentally evaluate the efficiency of LLM proxies against human queries in the well-studied course allocation domain.
  arXiv  Detail & Related papers  (2025-02-14T17:12:20Z)
• CogSteer: Cognition-Inspired Selective Layer Intervention for Efficiently Steering Large Language Models [37.476241509187304]
  Large Language Models (LLMs) achieve remarkable performance through pretraining on extensive data. The lack of interpretability in their underlying mechanisms limits the ability to effectively steer LLMs for specific applications. In this work, we investigate the mechanisms of LLMs from a cognitive perspective using eye movement measures.
  arXiv  Detail & Related papers  (2024-10-23T09:40:15Z)
• Zero-shot Model-based Reinforcement Learning using Large Language Models [12.930241182192988]
  We investigate how pre-trained Large Language Models can be leveraged to predict in context the dynamics of continuous Markov decision processes. We present proof-of-concept applications in two reinforcement learning settings: model-based policy evaluation and data-augmented off-policy reinforcement learning.
  arXiv  Detail & Related papers  (2024-10-15T15:46:53Z)
• In-Context Learning with Reinforcement Learning for Incomplete Utterance Rewriting [33.89176174108559]
  In-context learning of large language models (LLMs) makes predictions only based on instructions augmented with a few examples. Existing example selection methods for ICL utilize sparse or dense retrievers and derive effective performance. We propose our policy-based reinforcement learning framework for example selection (RLS), which consists of a language model (LM) selector and an LLM generator.
  arXiv  Detail & Related papers  (2024-08-23T12:32:12Z)
• Q*: Improving Multi-step Reasoning for LLMs with Deliberative Planning [53.6472920229013]
  Large Language Models (LLMs) have demonstrated impressive capability in many natural language tasks. LLMs are prone to produce errors, hallucinations and inconsistent statements when performing multi-step reasoning. We introduce Q*, a framework for guiding LLMs decoding process with deliberative planning.
  arXiv  Detail & Related papers  (2024-06-20T13:08:09Z)
• From Words to Actions: Unveiling the Theoretical Underpinnings of LLM-Driven Autonomous Systems [59.40480894948944]
  Large language model (LLM) empowered agents are able to solve decision-making problems in the physical world. Under this model, the LLM Planner navigates a partially observable Markov decision process (POMDP) by iteratively generating language-based subgoals via prompting. We prove that the pretrained LLM Planner effectively performs Bayesian aggregated imitation learning (BAIL) through in-context learning.
  arXiv  Detail & Related papers  (2024-05-30T09:42:54Z)
• One Token Can Help! Learning Scalable and Pluggable Virtual Tokens for Retrieval-Augmented Large Language Models [67.49462724595445]
  Retrieval-augmented generation (RAG) is a promising way to improve large language models (LLMs)<n>We propose a novel method that involves learning scalable and pluggable virtual tokens for RAG.
  arXiv  Detail & Related papers  (2024-05-30T03:44:54Z)
• Improve Temporal Awareness of LLMs for Sequential Recommendation [61.723928508200196]
  Large language models (LLMs) have demonstrated impressive zero-shot abilities in solving a wide range of general-purpose tasks. LLMs fall short in recognizing and utilizing temporal information, rendering poor performance in tasks that require an understanding of sequential data. We propose three prompting strategies to exploit temporal information within historical interactions for LLM-based sequential recommendation.
  arXiv  Detail & Related papers  (2024-05-05T00:21:26Z)
• PANDA: Preference Adaptation for Enhancing Domain-Specific Abilities of LLMs [49.32067576992511]
  Large language models often fall short of the performance achieved by domain-specific state-of-the-art models. One potential approach to enhance domain-specific capabilities of LLMs involves fine-tuning them using corresponding datasets. We propose Preference Adaptation for Enhancing Domain-specific Abilities of LLMs (PANDA) Our experimental results reveal that PANDA significantly enhances the domain-specific ability of LLMs on text classification and interactive decision tasks.
  arXiv  Detail & Related papers  (2024-02-20T09:02:55Z)
• Are Large Language Models Good Prompt Optimizers? [65.48910201816223]
  We conduct a study to uncover the actual mechanism of LLM-based Prompt Optimization. Our findings reveal that the LLMs struggle to identify the true causes of errors during reflection, tending to be biased by their own prior knowledge. We introduce a new "Automatic Behavior Optimization" paradigm, which directly optimize the target model's behavior in a more controllable manner.
  arXiv  Detail & Related papers  (2024-02-03T09:48:54Z)
• LLMRec: Benchmarking Large Language Models on Recommendation Task [54.48899723591296]
  The application of Large Language Models (LLMs) in the recommendation domain has not been thoroughly investigated. We benchmark several popular off-the-shelf LLMs on five recommendation tasks, including rating prediction, sequential recommendation, direct recommendation, explanation generation, and review summarization. The benchmark results indicate that LLMs displayed only moderate proficiency in accuracy-based tasks such as sequential and direct recommendation.
  arXiv  Detail & Related papers  (2023-08-23T16:32:54Z)
• PRISMA-DFLLM: An Extension of PRISMA for Systematic Literature Reviews using Domain-specific Finetuned Large Language Models [0.0]
  This paper proposes an AI-enabled methodological framework that combines the power of Large Language Models (LLMs) with the rigorous reporting guidelines of the Preferred Reporting Items for Systematic Reviews and Meta-Analyses (PRISMA) By finetuning LLMs on domain-specific academic papers that have been selected as a result of a rigorous SLR process, the proposed PRISMA-DFLLM reporting guidelines offer the potential to achieve greater efficiency, reusability and scalability.
  arXiv  Detail & Related papers  (2023-06-15T02:52:50Z)

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.