Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers

This paper introduces Strat2Rocq, a framework that extracts and formalizes proof strategies from large language models as lemmas to augment symbolic provers like CoqHammer, significantly improving their automated theorem proving success rates while also benefiting LLM-based proof agents.

The Gist

Here is an explanation of the paper "Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers" using simple language and creative analogies.

The Big Picture: The "Smart Intern" vs. The "Strict Librarian"

Imagine you are trying to solve a very difficult math puzzle. You have two tools:

1. The Strict Librarian (Symbolic Prover): This is a computer program (like CoqHammer) that is incredibly logical, precise, and secure. It never makes mistakes, but it's a bit rigid. It follows rules step-by-step. If it doesn't have a specific rule in its library to solve a puzzle, it gets stuck, even if the answer is obvious to a human. It's like a librarian who will only find a book if you give them the exact ISBN number; if you describe the plot, they can't help.
2. The Smart Intern (Large Language Model/LLM): This is an AI (like Claude or o3-mini) that is incredibly creative and intuitive. It can look at a puzzle and instantly say, "Oh, I know this! It's just like that other puzzle we solved last week!" It has a "gut feeling" for the solution. However, it can be unreliable (it might lie or make up facts), it's expensive to run, and you can't always trust it with your company's secret code.

The Problem:
The Librarian is safe and cheap but gets stuck easily. The Intern is smart but risky and expensive. Usually, to solve hard problems, you need to hire the Intern to do the work, which costs money and risks leaking secrets.

The Solution (Strat2Rocq):
The authors asked: "Can we take the Intern's 'gut feelings' and turn them into a new set of rules for the Librarian?"

They built a system called Strat2Rocq. It acts like a translator or a teacher. It watches the Smart Intern solve problems, figures out how it solved them, and then writes those "aha!" moments down as official, verified rules (lemmas) that the Strict Librarian can understand and use forever.

---

How It Works: The Two-Step Process

Step 1: The "Study Session" (Offline Mining)

Imagine the Strict Librarian is sitting in a quiet room with a stack of 2,000 math problems.

1. The Intern Solves: The Smart Intern is brought in to solve these problems. It doesn't just give the answer; it explains its thought process in plain English (e.g., "First, I realized that multiplying by 1 doesn't change anything, so I can skip that step.").
2. The Translation: The system listens to the Intern's explanation. It spots the clever shortcuts the Intern used.
3. The Rulebook Update: The system takes those shortcuts and turns them into formal, mathematical laws (lemmas). It's like taking the Intern's "secret trick" and printing it on a page in the Librarian's official rulebook.
   • Example: If the Intern realizes that A + B + C is the same as C + B + A without needing to check every single letter, the system writes a new rule: "You can swap the order of addition."

This happens offline. It's a one-time setup. The Intern does the heavy lifting once, and the result is a permanent upgrade for the Librarian.

Step 2: The "Exam" (Online Proving)

Now, a user brings a new problem to the Strict Librarian.

• Before: The Librarian tries to solve it using only its old, rigid rules. It gets stuck.
• After: The Librarian opens its rulebook. Thanks to the "Study Session," it now has the new rules extracted from the Intern. It sees the new problem, applies the "Int's trick," and solves it instantly!

Crucially, no Intern is needed during the exam. The Librarian does all the work using the new rules. This means it's fast, cheap, and secure.

---

Why This Is a Big Deal

1. It's Cheaper and Safer: You don't need to pay for expensive AI services every time you want to verify software code. You just use the upgraded Librarian.
2. It Keeps Secrets Safe: Companies with confidential code (like banks or defense contractors) can't send their code to public AI servers. With this method, they can upgrade their local tools without ever sending their data to the cloud.
3. It's a "Win-Win":
   • For the Librarian: It got smarter. The paper shows it solved 13.4% more problems than before.
   • For the Intern: Even the Intern got a boost! When the Intern tried to solve problems again, having access to these new rules helped it succeed 4% more often. It's like the Intern reading its own study notes and getting smarter.

The "Side Effect" Discovery

The researchers found something cool: The "tricks" they extracted weren't just for the Librarian. They were also helpful for the Intern itself. It turns out that even a super-smart AI can benefit from having a structured list of its own best strategies.

Summary Analogy

Think of Strat2Rocq as a Master Chef (the LLM) teaching a Robot Kitchen (the Symbolic Prover).

• The Robot is great at chopping vegetables perfectly but doesn't know how to make a complex sauce.
• The Master Chef makes the sauce, explaining the secret ingredients and timing.
• The system records the Chef's recipe and programs it into the Robot.
• Now, the Robot can make the sauce perfectly every time, without needing the Chef to be in the kitchen. The Robot is faster, cheaper to run, and the recipe stays safe in the kitchen.

The paper proves that by "distilling" the intelligence of AI into the rules of traditional software, we can make our tools safer, faster, and much more capable.

Technical Summary

Here is a detailed technical summary of the paper "Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers."

1. Problem Statement

The paper addresses the limitations of current approaches in automated theorem proving (ATP) for software verification:

• Symbolic Provers: Traditional tools like CoqHammer are cost-effective, secure, and run locally but often lack the "intuition" or high-level strategies required to solve complex theorems without human intervention.
• Large Language Models (LLMs): LLM-based proof agents have shown strong capabilities but suffer from high computational costs, latency, and security risks (especially for confidential codebases). They also require online interaction, making them unsuitable for resource-constrained or security-sensitive environments.
• The Gap: There is a need to combine the security and efficiency of symbolic provers with the strategic reasoning capabilities of LLMs. The core research question is: Can the internal proof strategies of LLMs be extracted and formalized to enhance purely symbolic provers without requiring online LLM interaction during the proving phase?

2. Methodology: Strat2Rocq

The authors propose Strat2Rocq, a two-stage framework designed to distill LLM reasoning into formal lemmas that a symbolic prover can utilize.

Stage 1: Offline Lemma Mining

This stage occurs once on a training dataset of theorems.

1. Natural Language (NL) Proof Generation: For each theorem in the training set, the system prompts an LLM (e.g., Claude 3.7 Sonnet or o3-mini) to generate a step-by-step natural language proof. The prompt includes type definitions, function definitions, and the surrounding script context to ensure accuracy.
2. Generalization and Formalization: The system prompts the LLM to:
   • Identify atomic steps in the NL proof.
   • Generalize these steps into reusable mathematical properties (lemmas).
   • Formalize these lemmas and their proofs in Rocq (the language of Coq).
3. Iterative Repair: Since LLMs often produce incorrect formalizations, a Proof Agent is employed. This agent iteratively attempts to compile and prove the generated lemmas. If errors occur, it uses specific repair modules (categorized by error type) to prompt the LLM to fix the lemma or proof until it is valid or a round limit is reached.

Stage 2: Online Theorem Proving

This stage occurs when a user attempts to prove a new theorem.

• Context Augmentation: The extracted, verified lemmas from Stage 1 are inserted into the context of the target theorem.
• Symbolic Proving: A purely symbolic prover (CoqHammer) attempts to prove the theorem using the augmented context.
• Key Mechanism: CoqHammer uses a built-in KNN-based lemma selection mechanism to retrieve relevant lemmas from the expanded context. Crucially, the number of retrieved lemmas is fixed, ensuring that adding thousands of new lemmas does not degrade the prover's efficiency.
• No Online LLM: The actual proving process relies entirely on the symbolic prover; the LLM is not involved in the online phase.

3. Key Contributions

1. Novel Research Problem: The paper defines the problem of extracting internal LLM proof strategies to enhance symbolic provers, bridging the gap between neural and symbolic approaches.
2. Strat2Rocq Framework: A practical implementation that converts LLM-generated natural language reasoning into verified, formal lemmas in Rocq.
3. Performance Enhancement: Empirical validation showing that these extracted lemmas significantly boost the success rate of state-of-the-art symbolic provers.
4. Dual Utility: The extracted lemmas not only help symbolic provers but also improve the performance of LLM-based proof agents by providing a richer knowledge base for retrieval-augmented generation (RAG).

4. Experimental Results

The framework was evaluated on a benchmark of 2,394 theorems from open-source Rocq projects (CompCert, Ext-Lib, Coq-Art, Vfa) using 3-fold cross-validation.

• Symbolic Prover Improvement (CoqHammer):

  • Strat2Rocq increased the proof success rate of CoqHammer by 13.41% on average.
  • The improvement was most significant on CompCert (a real-world certified C compiler), where success rates rose by 17.75%.
  • The extracted lemmas helped CoqHammer solve theorems that previously required induction (which CoqHammer cannot perform) by reducing them to commutativity or other standard library properties.

• LLM Agent Improvement:

  • When the extracted lemmas were used to augment an LLM proof agent (via RAG), the agent's success rate improved by 4.00%.
  • Token usage decreased by 5.87% because the enhanced CoqHammer could solve more theorems independently, reducing the need for LLM calls.

• Ablation Studies:

  • NL Generation Importance: Skipping the Natural Language proof generation step and asking the LLM to generate lemmas directly resulted in a 63.56% drop in extracted lemmas and a 6.21% drop in proving performance. This confirms that NL reasoning acts as a crucial intermediate step for strategy extraction.
  • Model Agnosticism: The approach works with different backend LLMs (Claude 3.7 and o3-mini). Combining lemmas from both models yielded even higher performance, suggesting their internal strategies are complementary.

5. Significance

• Security and Cost: Strat2Rocq allows organizations to leverage the "intelligence" of LLMs without exposing confidential code to external APIs or incurring high inference costs during the verification process. The heavy lifting is done offline; the online process is purely local and symbolic.
• Explainability: By extracting LLM strategies as formal lemmas, the framework provides a symbolic approximation of how LLMs "think" about proofs. This offers a new avenue for interpreting LLM behavior in formal reasoning.
• Scalability: The method demonstrates that symbolic provers can be significantly enhanced by a static library of distilled knowledge, making them more robust for industrial-strength software verification.