# Steering LLMs for Formal Theorem Proving

arXiv: https://arxiv.org/abs/2502.15507 · HTML: https://mlsanity.com/paper/2502.15507/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 41 of its 57 references that are in the map.
- First posted on arXiv 21 Feb 2025.

## Builds on (most cited first, 30 of 41)

- [LoRA: Low-Rank Adaptation of Large Language Models](https://mlsanity.com/paper/2106.09685/) (2021)
- [Distributed Representations of Words and Phrases and their Compositionality](https://mlsanity.com/paper/1310.4546/) (2013)
- [Locating and Editing Factual Associations in GPT](https://mlsanity.com/paper/2202.05262/) (2022)
- [Sparse Autoencoders Find Highly Interpretable Features in Language Models](https://mlsanity.com/paper/2309.08600/) (2023)
- [Representation Engineering: A Top-Down Approach to AI Transparency](https://mlsanity.com/paper/2310.01405/) (2023)
- [Inference-Time Intervention: Eliciting Truthful Answers from a Language Model](https://mlsanity.com/paper/2306.03341/) (2023)
- [Steering Llama 2 via Contrastive Activation Addition](https://mlsanity.com/paper/2312.06681/) (2023)
- [Towards Understanding Sycophancy in Language Models](https://mlsanity.com/paper/2310.13548/) (2023)
- [Refusal in Language Models Is Mediated by a Single Direction](https://mlsanity.com/paper/2406.11717/) (2024)
- [Steering Language Models With Activation Engineering](https://mlsanity.com/paper/2308.10248/) (2023)
- [Discovering Language Model Behaviors with Model-Written Evaluations](https://mlsanity.com/paper/2212.09251/) (2022)
- [The Linear Representation Hypothesis and the Geometry of Large Language Models](https://mlsanity.com/paper/2311.03658/) (2023)
- [The Geometry of Truth: Emergent Linear Structure in Large Language Model Representations of True/False Datasets](https://mlsanity.com/paper/2310.06824/) (2023)
- [The Internal State of an LLM Knows When It's Lying](https://mlsanity.com/paper/2304.13734/) (2023)
- [Eliciting Latent Predictions from Transformers with the Tuned Lens](https://mlsanity.com/paper/2303.08112/) (2023)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Llemma: An Open Language Model For Mathematics](https://mlsanity.com/paper/2310.10631/) (2023)
- [Emergent Linear Representations in World Models of Self-Supervised Sequence Models](https://mlsanity.com/paper/2309.00941/) (2023)
- [Language Models Represent Space and Time](https://mlsanity.com/paper/2310.02207/) (2023)
- [In-Context Learning Creates Task Vectors](https://mlsanity.com/paper/2310.15916/) (2023)
- [Function Vectors in Large Language Models](https://mlsanity.com/paper/2310.15213/) (2023)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [Causal Mediation Analysis for Interpreting Neural NLP: The Case of Gender Bias](https://mlsanity.com/paper/2004.12265/) (2020)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning](https://mlsanity.com/paper/2402.06332/) (2024)

## Built on by (most cited first, 4 of 4)

- [GeoSteer: Faithful Chain-of-Thought Steering via Latent Manifold Gradients](https://mlsanity.com/paper/2601.10229/) (2026)
- [Whose Narrative is it Anyway? A KV Cache Manipulation Attack](https://mlsanity.com/paper/2511.12752/) (2025)
- [IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch](https://mlsanity.com/paper/2512.00997/) (2025)
- [VISPA: Pluralistic Alignment via Automatic Value Selection and Activation](https://mlsanity.com/paper/2601.12758/) (2026)

## Abstract (arXiv)

Recent advances in automated theorem proving use Large Language Models (LLMs) to translate informal mathematical statements into formal proofs. However, informal cues are often ambiguous or lack strict logical structure, making it hard for models to interpret them precisely. While existing methods achieve strong performance, little is known about how LLMs internally represent informal cues, or how these influence proof generation. To address this, we explore textitactivation steering, an inference-time intervention that identifies linear directions in residual activations associated with informal reasoning traces and adjusts them to improve proof construction without fine-tuning. This mechanism also yields interpretable information about how reasoning is internally encoded in the activation space of LLMs. We test our method for generating formal proofs from already-formalized theorems. Our contributions are twofold: (1) a novel activation-based intervention for guiding proof synthesis in LLMs; and (2) demonstration that this intervention improves performance under two decoding strategies (sampling and best-first search) without any further training.