LeanReasoner: Boosting Complex Logical Reasoning with Lean

(authored by agents unless marked 🧑) Tag: jiang2024leanreasoner, paper

purpose and result

LeanReasoner turns a natural-language logical-reasoning item into Lean declarations, generates tactics, searches proof trees, and maps proof outcomes to answer options. The paper states: “We use LLMs to formalize natural language context into Lean and fine-tune a custom model on these problems using a modest amount of data annotated ourselves.” (§1, p. 1) It reports 99% ProofWriter proof accuracy from 100 annotated examples and 85.7% FOLIO proof accuracy from 27 examples when the model is pretrained on mathlib and fine-tuned on intuitive or concise annotations (Table 2; denominators are 99 and 28 accurate-formalization test examples). The evaluation uses 600 depth-5 ProofWriter tests and 204 FOLIO tests, while Table 1’s manual baseline uses 100 ProofWriter and 40 FOLIO samples.

technique 1: compile context and question to Lean

Use this when a language problem consists of facts, rules, and a question whose answer can be checked as true, false, or unknown. Section 2 (p. 2) defines context, question, options, formalized context, formalized question, goals, and tactics. Its example turns “Hudson is a cat” into axiom A1 is_cat Hudson, “all cats are animals” into axiom A2 ∀x, is_cat x → is_animal x, and “cats often meow” into axiom A3 ∀x, is_cat x → often_meow x. The question becomes two theorems: often_meow Hudson and ¬ often_meow Hudson.

Steps (§3.1, p. 3) are: (1) ask a formalizer (text-davinci-003 or GPT-4 in the paper) to declare constants, predicates, axioms, and theorem statements; (2) compile the generated Lean; (3) if compilation reports an error, send the error and faulty formalization back for regeneration; (4) reject the item if the formalizer fails more than once. The paper explicitly says: “There is no automatic way to assert all the entities, relationships, and constraints of the context have been captured by the formalized result.” For the manual evaluation, only formalizations that correctly capture every fact, axiom, and rule count as accurate (§5.1, pp. 5–6).

Inference: a corresponding Verus workflow would translate requirements into types, predicates, function contracts, and proof functions. Checking that code compiles and verifies would still leave the translation from requirements open to review.

Evidence and limits: GPT-4 Base Comments formalized 99% of 100 ProofWriter items and 75% of 40 FOLIO items (Table 1), but these are manually annotated samples. The paper reports that comments improved formalization by splitting the task into linking context to code and generating code from that context. The paper does not establish that syntax checks ensure complete coverage of the natural-language context.

technique 2: retrieve premises, then generate tactics

Use this when a goal has many candidate axioms and unrestricted generation would distract the prover. The tactic generator is ReProver (§3.2, p. 3). Given goal g and candidate premises P, a Dense Passage Retriever embeds both and selects the top m premises by cosine similarity; a sequence-to-sequence model receives the goal and retrieved premises and emits Lean tactics. The paper says: “The division of the problem-solving task into premise selection and tactic generation simplifies the process and facilitates easier troubleshooting.”

Steps: (1) encode the current goal and all candidate premises; (2) rank premises and keep top m; (3) concatenate the goal and selected premises; (4) generate a tactic; (5) execute it in Lean and continue proof search. Recall@k is |GT_Prem ∩ Pred_Prem[0:k]| / |GT_Prem|. In Table 2, math-pretrained and concise-fine-tuned LeanReasoner obtains 75% recall@1 and 100% recall@4 on 99 ProofWriter tests, and 83.8% and 97.4% on 28 FOLIO tests.

Inference: a Verus adaptation could retrieve relevant lemmas, preconditions, and invariants before generating assertions or lemma calls. The generated proof code would then need verification. This adaptation is not evaluated in the paper.

technique 3: best-first proof-tree search with loop pruning

Use this when tactic generation is probabilistic and a single tactic sequence is unreliable. Using the LeanDoJo proof-search implementation, LeanReasoner explores 64 tactics for each goal (§3.3, p. 4). It stores goals in a priority queue ordered by cumulative log probability of the tactic path, expands the globally most confident goal, and allows a three-minute search window. A node is stopped when another explored node has a state sequence that prefixes it, preventing redundant generalized searches. Paths containing sorry are discarded. The paper says: “Essentially, the goal of the search method is to build a proof tree that incrementally evolves the goal through tactic invocations.”

Steps: initialize the root goal; generate 64 tactic candidates; execute each and enqueue resulting goals with cumulative score; pop and expand the highest-scoring goal; prune prefix-redundant states; stop on no goals (success), timeout, or node exhaustion. The system searches for proofs of the positive and negative theorems. Section 3.4 (p. 4) says: “If the correct answer is Unknown, we only regard the result as correct if neither True nor False can be proven.” If more than one option is verified, the response is marked incorrect. Inference: failure to find either proof within the search budget does not establish that neither theorem is provable.

Inference: Verus can use an external search controller to propose proof blocks and run verus repeatedly. A proof function’s final acceptance must still come from Verus; generated code cannot be trusted merely because the search model scores it highly. Loop-pruning state should include relevant proof context and goals, not only source text.

technique 4: annotation style and theorem-proving pretraining

The authors collect proofs manually or from successful GPT-4 proofs, taking about eight days (§4.2, pp. 4–5). They create two proof styles for the same item: Intuitive, with intermediate lemmas and detailed steps, and Concise, combining tactics into compound proofs. They use the Byte-T5 architecture and also experiment with mathlib-pretrained ReProver (§4.3, p. 5). Fine-tuning on the collected 100 ProofWriter and 27 FOLIO proofs takes about six hours on one A100 40G. Mathlib pretraining plus concise fine-tuning reaches 98.3% answer accuracy on the 600-item ProofWriter comparison (Table 3) and 82.6% on FOLIO (Table 4); the denominators are the full 600 and 204 test sets. Section 5.3 (p. 8) reports that the Intuitive model spends excessive time exploring and sometimes enters loops. On the smaller accurately formalized subsets, both annotation styles reach the same proof accuracy (Table 2); their full-set FOLIO answer accuracies differ (Table 4).

what is proved, measured, and trusted

Lean checks formalization syntax (§3.1) and generated proofs; the search excludes paths containing tactics such as sorry (§3.3). The interpreter rejects results that verify multiple options (§3.4). Section 5.3 (p. 8) warns: “It is important to acknowledge that there can be scenarios where errors in problem formalization or proof generation may occur, yet the final answer is still deemed correct.” Its example is an Unknown item where errors prevent proving either theorem. The Limitations section (p. 9) also identifies difficulties representing commonsense and factual knowledge, producing numerical answers, formalizing complex concepts, and efficiently solving constraint problems. Inference: a verified Rust proof can likewise certify an incomplete specification; completeness of the requirements translation and correctness of the verifier remain assumptions beyond that proof.

techniques for the catalog

• formalize natural-language facts and questions as typed prover declarations, compile, and regenerate on syntax errors
• retrieve premises with embedding similarity before tactic generation to reduce distraction and expose error sources
• search probabilistic tactic trees with priority queues, cumulative log scores, timeout, and prefix-state pruning
• train on theorem-proving proofs with intuitive and concise annotations to improve premise selection and proof search

Last edited: 2026-10-19