PaperlayerView exact revision on arXiv

Source-linked AI summary

Efficient Proof Generation for Lean Statements with Multiple Candidate Answers

Pengzhen Lin, Ke Zhang, Maziar Raissi, Zhouxing Shi

arXiv:2610.34490v1cs.CLcs.AIcs.LG

TL;DR

When answers are unknown, proving candidates one by one repeats costly work. Joint proof selects or proposes answers and generates proofs together; it matches per-candidate proof success with about one sixth of the prover output tokens while flagging unfaithful formalizations. Its faithfulness signal is limited to problems with a unique answer and can miss some incorrect translations.

  • Problem

    For answer-construction problems, the correct answer is unknown, yet common proof-generation workflows assume it is known and repeated candidate-wise proof calls are costly.

    Source: §1 · p. 1

  • Method

    A trained prover handles multiple candidates in one call, declaring answers it can prove, generating a shared proof, and proposing new answers when needed.

    Source: §1 · p. 1

  • Results

    On common math benchmarks, joint proof matches per-candidate proof success with about one sixth of the prover output tokens and flags at least 6.1% of formal statements as unfaithful.

    Source: §1 · p. 2

  • Takeaways & Limitations

    For unique-answer problems, two distinct answers accepted by Lean provide a checkable signal that the formal translation is wrong.

    Source: §5 · p. 8

    Efficiency weakens when candidate changes require fundamentally different logical structures, and faithfulness checks can miss incorrect translations that entail only one answer or overlook another valid answer.

    Source: Limitations · pp. 8–9

Abstract

from arXiv · show

In formal systems such as Lean 4, efficiently finding answers to mathematical problems and generating verifiable proofs is an important task in automated mathematical reasoning. In the traditional way where an upstream solver provides multiple candidate answers, the common workflow requires searching for proofs for each candidate separately, incurring redundant computational cost. To this end, we propose a joint proof framework that integrates candidate answer selection, answer supplementation, and formal proof generation into a unified reasoning process. At its core is a trained prover that selects given or proposes new answers and generates a proof for at least one answer in a single call. Joint proof can also reuse generated proofs to check for faithfulness errors. For problems with a unique answer, if two distinct answers both obtain verifiable proofs under the same formal statement, this confirms the statement does not faithfully preserve the original problem semantics. On MATH-500, AMC 2023, and AIME 2024/2025/2026, our framework achieves the same formal proof success rate as per-candidate proof generation with about one sixth of the token cost, and identifies at least 6.1% of the formalized statements as unfaithful without requiring additional judges. Our model and code are available at https://github.com/Linppz/Gobble-Prover.

1 Introduction

Answer-construction problems leave the correct answer unknown, while the usual candidate-by-candidate workflow repeats costly formalization and proof calls. The proposed joint framework handles candidates together, can propose new answers, and uses multiple accepted answers to flag some unfaithful formalizations.

1 Introduction

  • Answer-construction problems ask for answers not known in advance, a setting that remains understudied because much proof-generation work assumes the answer is already known.In the standard assumed-known setup, the theorem statement already contains the ground-truth answer.Source: §1 · p. 1
  • The trained prover handles all candidates in one call, selects candidates it can prove, and can propose new answers when none works.It can also produce one proof that covers several candidates; Lean checks only the answers the prover declares.Source: §1 · p. 1
  • The prover is trained with supervised fine-tuning followed by reinforcement learning to list provable answers and write reusable proofs.The reinforcement-learning reward is higher when two or more distinct answers pass Lean.Source: §1 · pp. 1–2
  • For k candidates, Figure 1 shows prover and Lean calls falling from O(k) to O(1) by combining candidates in a joint proof task.The original workflow formalizes and attempts a proof separately for each candidate, leaving repeated calls even when one formal statement is reused.Source: §1 · p. 1, Figure 1 · p. 2
  • Joint proof matches per-candidate proof success on common math benchmarks with about one sixth of the prover output tokens and flags at least 6.1% of formal statements as unfaithful.The faithfulness signal uses two distinct Lean-accepted answers for a problem with a unique answer.Source: §1 · pp. 1–2

2 Related Work

Related work covers Lean theorem provers, approaches to answer-construction problems, and methods for detecting unfaithful formalizations. The paper positions joint proof as combining answer selection and proof generation while using multiple accepted answers as a reference-free faithfulness signal.

Formal theorem provers

  • Lean provers generally receive statements with answers already specified, whereas this prover receives an empty answer slot and multiple candidates and learns to select or discover provable answers.Prior systems commonly train with supervised fine-tuning and expert iteration, then refine with reinforcement learning using Lean-verifier rewards.Source: §2 · p. 2

Proving answer-construction problems

  • Existing answer-construction approaches either prove each candidate separately or let the prover fill a blank, which can permit answers that merely restate the problem condition.The proposed method combines candidates in one prover call and constrains new-answer proposals to integers or decimals of the same type, blocking that restatement shortcut without a reference answer.Source: §2 · p. 2

Faithfulness of formalization

  • Faithfulness checks include reference-based metrics, LLM judges, and reference-free symptom checks, while joint proof uses two accepted answers to flag unfaithful translations for unique-answer problems.The passage characterizes this signal as limited in coverage but easy to interpret.Source: §2 · pp. 2–3

3 Method

The method replaces separate proof attempts for candidate answers with a joint prover workflow. It defines how candidate answers are formed and formalized, how one proof and declared answer list are checked, and how the prover is trained to produce them.

3.1 Preliminaries

  • For answer-construction problems, an upstream solver samples and deduplicates candidates, and the task is to identify the correct answer if present.The ground-truth answer is initially unknown; the pipeline then formalizes candidate answers and asks a prover to prove them in Lean.Source: §3.1 · p. 3
  • Per-candidate proof generation calls the prover separately for each candidate statement, while a reusable formal statement template can replace the candidate with an answer slot.The formalizer creates a statement asserting that a candidate answers the problem; Lean’s well-formedness check does not itself prove that statement.Source: §3.1 · p. 3

3.2 Joint Proof Framework for Multiple Candidates

  • The declared list identifies values the prover predicts its proof will verify, while out-of-set answers can supplement candidates when they are integers or finite decimals.Only the first c valid declared values are kept for Lean checks; otherwise, the allowed out-of-set answer set is empty.Source: §3.2 · pp. 3–4
  • The joint framework uses a constant number of prover calls and at most c Lean calls, versus k calls for both per-candidate stages.The prover receives a reusable template and candidate set, then generates one proof and a declared list of answers predicted to pass Lean.Source: §3.2 · pp. 3–4
  • For a problem expected to have one answer, two distinct values passing Lean under the same template flag it as unfaithful.Training uses supervised fine-tuning followed by reinforcement learning, whose reward favors multiple distinct declared values passing with the same proof.Source: §3.2 · p. 4, §3.3 · pp. 4–5

3.3 Training

  • For SFT, answer masking and perturbed candidate sets produce template-based examples, and retained proofs receive inferred Passes lists as targets.The training data mixes these examples with existing data to preserve ordinary proving ability.Source: §3.3 · p. 4

4 Experiments

Across answer selection and unfaithfulness detection, joint proof reduces prover and verification costs while identifying formal statements that admit multiple answers. Ablations examine the roles of answer coverage, verification limits, and training.

4.1 Experimental Settings

  • Evaluation uses 630 problems from MATH-500, AMC 2023, and AIME 2024–2026, with eight upstream responses per problem and up to eight prover calls per pipeline.The answer-selection setup uses Gemma-3-4B and Qwen3.5 solvers, GPT-5.6 Sol formalization, and Gobble-Prover models with their base provers as per-candidate baselines.Source: §4.1 · p. 5, §4.2 · p. 5

4.2 Answer Selection

  • Joint proof outperforms per-candidate accuracy across solvers; for Qwen3.5-0.8B, the 1.7B pair scores 40.5% versus 34.6%, and end-to-end accuracy is 59.8% versus 55.6%.The end-to-end comparison uses majority voting when no value passes Lean after eight attempts; majority voting alone reaches 52.9%.Source: §4.2 · p. 6
  • At 16.4K tokens, joint proof reaches per-candidate final accuracy versus 104.7K tokens, and uses 45% of baseline Lean verification time.The comparison pools both prover pairs; the 45% figure holds even when verifying all declared values.Source: §4.2 · p. 6, Figure 3 · p. 7

4.3 Unfaithfulness Detection

  • Across the two-prover union, 46% of statements pass Lean and 5.4% are flagged; pooling runs yields 6.1% flagged templates, with harder datasets showing larger unfaithful shares among accepted statements.Both judges labeled 187 of 225 flagged statements unfaithful; when told that two values pass Lean, they changed the 17 faithful verdicts to unfaithful.Source: §4.3 · p. 6, Figure 4 · p. 7

4.4 Ablation Study

  • On MATH-500 with StepFun formalizations and correct answers in every candidate set, SFT raises declaration rates from below 2% to 75–83%, then RL raises Lean acceptance rates to 29.712% and 30.86%.SFT-only acceptance rates are 20.905% and 20.947% for the 1.7B and 4B lineages; RL pushes declaration rates to 98–100%.Source: §4.4 · p. 7
  • At 0% candidate coverage with top-2 verification, exploration raises Lean pass rate from 6.6% to 22.3%; at 100% coverage, its gain shrinks to 1.8 points.The results support the design of proposing answers beyond the upstream candidate set.Source: §4.4 · p. 8
  • With exploration enabled, top-2 verification cuts Lean calls by 6.7–7.2×, while Lean pass rate falls 1.6–2.3 points and detection rate falls 1.0–1.4 points.The ablation compares sending the first two declared values with sending all candidates and proposed values.Source: §4.4 · p. 8
  • At 100% candidate coverage, untrained Leanstral nearly matches the trained prover’s pass rate, 34.0% versus 35.7%, but flags fewer statements, 1.9% versus 2.7%.The authors attribute its lower detection rate to lacking reward for proving two values with one proof.Source: §4.4 · p. 8

5 Conclusion

The framework combines answer selection and proof generation for multiple candidates in one prover call. It reduces token usage and verification cost, while using multiple Lean-accepted answers as a signal of unfaithful formalization.

5 Conclusion

  • A trained prover declares which candidate answers it can prove and generates the corresponding proof in a single pass.The framework targets efficient identification of mechanically verifiable answers after an upstream solver attempts a natural-language problem.Source: §5 · p. 8
  • The joint proof approach reduces both token usage and verification cost compared with handling candidate answers separately.The prover declares the candidates it can prove and generates their proof in one pass.Source: §5 · p. 8
  • For single-answer problems, Lean accepting two distinct values under the same formal statement signals that the formal translation is wrong.The framework turns semantic faithfulness into a checkable signal.Source: §5 · p. 8

Limitations

The method works best when candidate substitutions make small, local changes, and its unfaithfulness check has defined limits. The appendices describe answer masking, handling answers at multiple positions, and construction of the filtered problem data.

Limitations

  • The efficiency advantage fades when candidates require fundamentally different logical structures, and the method can miss unfaithful translations or problems without a single correct answer.A negative detection result alone does not guarantee that a formalization is faithful.Source: Limitations · pp. 8–9

A.1 Template Construction

  • The template construction masks the evaluation answer as <candidate>, allowing multiple answers to be substituted into the same formal problem template.The formalization consists of the evaluation answer and the formal problem template.Source: §A.1 · p. 12

A.2 Answers Occupying Multiple Positions

  • For answers occupying multiple positions, tuple components receive separate slots, while repeated occurrences of one value are all replaced by that candidate.The statement outside the slots stays unchanged, and the prover’s proof is attached as is.Source: §A.2 · p. 12

B.1 Problem Filtering and Answer Processing

  • From 50k sampled NuminaMath-LEAN problems, filtering for unique answers yielded approximately 36k formal statements, with answer locations found by regex or assisted localization.Training distractors were generated by perturbing correct numeric or string answers; evaluation distractors were likewise perturbed, including the candidate used for the incorrect-answer statement.Source: §B.1 · p. 12

B.2 Proof Sampling and Filtering

Appendix B describes proof-sample filtering, prompts for candidate and direct-proof tasks, construction of declared passing-answer lists, and training configuration. Multiple-choice prompts ask the prover to keep the formal statement fixed while producing a proof and declaring candidate values for Lean checking.

B.2 Proof Sampling and Filtering

  • Each base model sampled approximately 10k formal statements with eight samples per statement; outputs were retained only if at least one candidate passed Lean compilation.Complete outputs containing non-target languages were removed, at most two verified outputs per formal statement were kept, and 8-gram deduplication was applied.Source: §B.2 · p. 12

Prompt For Multiple-Choice Question (8 opt example)

Prompt For Multiple-Choice Question (4 opt example)

  • The 4-option prompt uses the same choose-or-propose format and asks the prover to keep the statement unchanged while completing its proof.As in the 8-option example, the first two declared Passes values are substituted and compiled with the unchanged proof.Source: Prompt For Multiple-Choice Question (4… · pp. 13–14

Prompt for regular direct proof problem

B.3 Passes List Construction

  • For SFT, a language model extracts candidate values the prover considered likely to pass, and that list is appended to the original output as the training target.Passes-list lengths were distributed across different sizes, and a randomly selected transition sentence introduced the declaration.Source: §B.3 · p. 14

Fixed transitions before the Passes line

B.4 Data Composition and Training Configuration

  • Each model’s training set contained 90% multiple-choice problems and 10% standard proofs, with candidate counts split evenly across 4, 8, 12, and 16.Ten percent of multiple-choice problems had no correct candidate; training used SFT followed by 200 GRPO steps, with LoRA in both stages.Source: §B.4 · p. 15

C.1 Per-Dataset Results

Table 3 breaks down Figure 3 accuracy by dataset for each prover and upstream solver. Its caption defines a solved problem as one whose ground-truth answer Lean accepts, under a limit of at most eight attempts.

C.1 Per-Dataset Results

  • Each AIME set contains 30 problems, so one problem changes its accuracy by 3.3 points.This sets the granularity for interpreting per-dataset AIME results.Source: §C.1 · p. 15
  • Table 3 reports accuracy (%) by dataset for each prover and upstream solver, with results for all 630 problems together.A problem counts as solved when Lean accepts its ground-truth answer; the table setting allows at most eight attempts per problem.Source: Table 3 · p. 15, §C.1 · p. 15
  • The table identifies Gemma-3-4B and Qwen3.5-0.8B/2B/9B as the upstream solvers represented.The caption describes accuracy by dataset for each prover and upstream solver.Source: Table 3 · p. 15

C.2 Majority-Vote Fallback

Lean-first selection matches or improves on majority voting, while the detection analyses report unfaithful formalizations across datasets, prover sizes, and a frontier autoformalizer. Detection is more frequent on harder problems, and the frontier-formalizer experiment flags 11 of 626 problems.

C.2 Majority-Vote Fallback

  • Lean-first selection matches or improves on majority voting for every solver, with gains of 6.6–6.9 points for Qwen3.5-0.8B and 0.2–0.6 points for Qwen3.5-9B.Only 0.7–1.2% of Lean-accepted values differ from ground truth across the four provers.Source: §C.2 · pp. 15–16, Table 4 · p. 16

D.1 Detection by Dataset

  • Table 5 reports Lean-pass and unfaithfulness-detection rates by dataset and autoformalizer, but the supplied text gives no per-cell values.The accompanying prose says Table 5 lists the numbers plotted in Figure 4.Source: Table 5 · p. 16, §D.1 · p. 16

D.2 Detection per Prover

  • Both Gobble-Provers have 40% Lean pass rates, while Gobble-Prover-4B detects unfaithfulness at 4.8% versus 3.6% for Gobble-Prover-1.7B.Source: §D.2 · p. 16

D.3 Detection with a Frontier Autoformalizer

  • With GPT-5.6 Sol formalizations, the prover union flags 11 of 626 problems (1.8%); Figure 6 indicates unfaithful formalizations occur more often on harder problems.The individual rates are 1.3% for Gobble-Prover-4B and 1.0% for Gobble-Prover-1.7B.Source: §D.3 · p. 16, Figure 6 · p. 16

D.4 LLM-as-Judge Evaluation

The evaluation pools flagged templates and asks two LLM judges to assess whether they preserve the source problem’s meaning. The supplied passages describe the judge setup and prompt, but do not report verdict outcomes.

D.4 LLM-as-Judge Evaluation

  • The evaluation pools flagged templates and has Gemini 3.7 Flash and GPT-6 Astra independently judge whether each template faithfully represents its natural-language problem.Table 6 organizes detection by statement origin and reports solved, unfaithful, and unfaithful-to-solved rates, without supplied cell values.Source: §D.4 · p. 16, Table 6 · p. 17

D.4.1 Evaluation Settings and Prompts

  • The judges receive the natural-language problem and corresponding Lean statement, then assess semantic changes such as missing assumptions, altered values, domains, quantifiers, or task.Source: §D.4.1 · p. 17
  • The prompt permits faithful equivalent reformulations, treats candidate placeholders and unfinished proofs as non-errors by themselves, and allows an uncertain verdict when context prevents judgment.Judges must return a JSON verdict of faithful, unfaithful, or uncertain, with a discrepancy for unfaithful cases.Source: §D.4.1 · p. 17

D.4.2 Results

This section reports judge verdicts and manual analyses of flagged statements, focusing on mismatches that can make formal statements incorrect or admit multiple answers. It also gives the reported Lean acceptance entry (576, 1200) and an example in which a contradictory premise makes any answer acceptable without determining x at the new point.

D.4.2 Results

  • 187 of 225 flagged statements were judged unfaithful by both reviewers (83.1%), interjudge agreement was 90.7%, and both later changed their 17 shared faithful verdicts to unfaithful.Gemini initially labeled 188 records unfaithful and 37 faithful; GPT labeled 207 unfaithful, 17 faithful, and one uncertain.Source: Table 8 · p. 18, §D.4.2 · p. 18

D.4.3 Case Analysis

  • The case analysis manually examines examples that models considered faithful but the proposed method did not.Source: §D.4.3 · p. 18

Natural Language Problem

  • Lean accepted 115 and 125 for the school-subject problem and 1 and 504 for the sequence, whose formal hypotheses respectively impose a population contradiction and an extra-index inconsistency.The school problem confuses the total population with the union taking at least one subject; the sequence conditions include k = 0, contradicting strict increase.Source: Natural Language Problem · pp. 18–19
  • Lean accepted 10 and 11 when the formal statement replaced the inverse condition with t + 2 ≡ 1 (mod 23), and 63 and 67 when the rotation formula retained the original x-coordinate.The latter formalization excludes the required fourth-quadrant intersection.Source: Natural Language Problem · pp. 18–19
  • Lean accepted 235 and 236 for a list encoded as a finite set, which cannot capture frequencies and selects a median from the set, and 1 and 2 for an unconstrained polynomial remainder.The polynomial statement omits the requirement that the remainder have lower degree than the divisor.Source: Natural Language Problem · p. 19
  • The square formalization’s equal-distance condition contradicts the prescribed products, while the complex-number case replaces a custom operation with ordinary multiplication, reducing its hypothesis to 0 = 40.Lean accepted 104 and 105 for the square case and 0 and 25 for the complex-number case.Source: Natural Language Problem · pp. 19–21
  • The natural-valued function conditions have no solution, the root-and-logarithm implication can hold vacuously, and the asymptote formalization states function values rather than limiting behavior.The function equations require f(2) = −1, and the root statement’s implication is satisfied when its antecedent is false.Source: Natural Language Problem · pp. 20–21
  • The vector-projection statement uses componentwise operations instead of inner products and omits a prescribed coordinate, while the walk problem mixes hours and minutes.The decimal statement also replaces the repeating-decimal series with a constant summand, omitting successive place values.Source: Natural Language Problem · pp. 20–21
  • 576, 1200 is the reported “Answer Accepted by Lean” entry.Source: Natural Language Problem · p. 21
  • The code assumes both y=15 and y=3, making its premise contradictory so any number is accepted and the answer is not unique.Source: Natural Language Problem · p. 21
  • Because the antecedent contradicts the calibration hypothesis for any q, the implication holds without determining x at the new point.Source: Natural Language Problem · p. 21

E.1 Full Per-Dataset Results

The candidate-set study finds nearly unchanged solve and detection rates across sizes 6, 8, and 12. The accompanying ablation setup evaluates untrained provers and specifies a Leanstral prompt that permits candidate analysis and write-in answers.

E.1 Full Per-Dataset Results

  • The ablation removes problems with multiple correct answers; for Kimina-Prover-Distill-1.7B, it extracts each proof body and tests candidates against the given template.Kimina does not provide a declared answer list and often modifies the template, so any compiling candidate counts as passed and two distinct compiling candidates count as unfaithful.Source: §E.1 · p. 21

E.2 Prompt for Leanstral 1.5

  • The Leanstral prompt asks the model to inspect eight candidates plus a possible write-in, declare up to two values, and attach one proof that is tested unchanged.The prompt awards a point if at least one declared value compiles and an additional point if two mathematically distinct values compile.Source: §E.2 · pp. 21–22
  • The prompt forbids proof bypasses such as sorry and requires a proof plan before the Lean code.Source: §E.2 · p. 22
  • Solve rates and unfaithful-statement detection rates are almost the same across candidate sets of 6, 8, and 12.The study uses Gobble-Prover-4B at pass@8 on MATH-500 StepFun, with the correct answer always included.Source: Figure 7 · p. 23

F Robustness Tests

Robustness tests find that the prover can recover answers without candidates, remains stable across candidate-set sizes, and retains nearly all ordinary proving ability.

Without candidates

  • 26.1% of formal statements pass Lean with no candidates, below 35.7% with correct candidates but above 22.3% with only incorrect candidates.Manual review found the prover did not copy the problem condition as its answer.Source: F Robustness Tests · p. 23

Candidate set size

  • Lean pass rates remain nearly flat at 35.4%, 34.8%, and 34.9% with 6, 8, and 12 candidates, respectively.Six candidates were unseen during training.Source: F Robustness Tests · p. 23

Proving capability

  • On miniF2F, pass@32 changes by only 0.0 and −1.3 points for the 1.7B and 4B provers, respectively.Training data retain problems requiring a direct proof to prevent erosion of ordinary proving ability.Source: F Robustness Tests · p. 23

Evaluation setup

  • Both base and fine-tuned models were evaluated with Lean 4.26 and the same Mathlib version, with partial lemma-name fix-ups before verification.The evaluation used a 30,000-token generation limit, temperature 1.0, and top-p 0.95.Source: F Robustness Tests · p. 23
Loading 2610.34490v1…