PaperlayerView exact revision on arXiv

Source-linked AI summary

FANS -- Formal Answer Selection for Natural Language Math Reasoning Using Lean4

Jiarui Yao, Ruida Wang, Tong Zhang

arXiv:2503.03238v2cs.CLcs.AI

TL;DR

Natural-language ambiguity and the limits of existing answer-selection methods leave LLM math answers without a formal basis. FANS translates candidate answers into Lean4 statements, verifies proofs, and uses the results to assist selection; experiments report accuracy gains on MATH500 and AMC23.

  • Problem

    Few works use Lean4 or other formal languages to strengthen LLMs’ natural-language math reasoning, while existing answer-selection methods lack a solid formal foundation.

    Source: §1 · p. 2

  • Method

    FANS trains LeanTranslator to translate natural-language question-answer pairs into Lean4 statements, then proves and verifies them to inform answer selection.

    Source: §1 · p. 2

  • Results

    1.91% on MATH500 and 8.33% on AMC23 are the maximum accuracy improvements reported for reward-model-enhanced LLMs on strong reward-model baselines.

    Source: §1 · p. 2

  • Takeaways & Limitations

    Lean4-verified deductions offer a trustworthy, interpretable alternative to conventional answer selection and reduce dependence on extensive adaptation across base models.

    Source: §5 · p. 8

    High false positives, incomplete provers, formalization errors, and limited Lean4 domain coverage constrain reliable verification to a subset of mathematical fields.

    Source: Limitations · p. 9

Abstract

from arXiv · show

Large Language Models (LLMs) have displayed astonishing abilities in various tasks, especially in text generation, classification, question answering, etc. However, the reasoning ability of LLMs still faces many debates. The inherent ambiguity of Natural Language (NL) limits LLMs' ability to perform verifiable reasoning, making its answers lack coherence and trustworthy support. To tackle the above problems, we propose a novel framework named FANS: Formal ANswer Selection for Natural Language Math Reasoning Using Lean4. To the best of our knowledge, it is the first framework that utilizes Lean4 to enhance LLMs' NL math reasoning ability. In particular, given an NL math question and LLM-generated answers, FANS first translates it into Lean4 theorem statements. Then it tries to prove it using a Lean4 prover and verify it by Lean4. Finally, it uses the FL result to assist in answer selection. It enhances LLMs' NL math ability in providing a computer-verifiable solution for its correct answer and proposes an alternative method for answer selection beyond the reward model. Extensive experiments indicate the effectiveness of our framework. It can improve the accuracy rate of reward model enhanced LLMs in the MATH-500 dataset by at most 1.91% and AMC-23 by at most 8.33% on strong reward-model baselines. In some particular fields like number theory that Lean4 experts in, we can even select all correct solutions. The qualitative analysis also shows our framework can make NL results formally backed by Lean4 proofs. As a pioneering work in the corresponding field, we will open-source all our models and datasets to further boost the development of the field.

1 Introduction

FANS addresses the difficulty of selecting trustworthy answers from ambiguous natural-language math outputs by translating them into Lean4 statements and using verified proofs to support selection. The framework improves answer-selection accuracy and provides a formal basis for selected answers.

1 Introduction

  • Few prior works had leveraged Lean4 or other formal languages to enhance LLMs’ natural-language mathematical reasoning, despite formal systems enabling computer verification.Formal languages map mathematics into formal kernels that allow computers to verify proofs.Source: §1 · pp. 1–2
  • Natural-language ambiguity makes generated math answers difficult to trust, while selecting a correct answer without ground truth remains non-trivial.Existing approaches range from majority vote to reward-model ranking, but the former may not realize pass@n potential and the latter remain LLM-based and can struggle under distribution shift.Source: §1 · p. 2
  • FANS translates natural-language question-answer pairs into Lean4 statements, proves and verifies them, then uses verification results to assist answer selection.The framework combines formal verification with existing selection methods to provide a verifiable foundation for natural-language math reasoning.Source: §1 · p. 2
  • The authors introduce a Long CoT translator training method for converting natural-language question-answer pairs into Lean4 statements.They describe it as, to their knowledge, the first such method.Source: §1 · p. 2
  • Experiments indicate that LLMs enhanced by the framework perform better in answer selection, improving accuracy by at most 1.91% on MATH500 and at most 8.33% on AMC23.In some particular subfields where Lean is better, the framework can select all correct solutions.Source: §1 · p. 2

2 Methodology

FANS translates natural-language math question-answer pairs into formal statements, applies Lean4 provers and verification, and uses the results in answer selection. Its methodology also describes translation-faithfulness checks and fallback selection when proofs cannot be obtained.

2 Methodology

  • FANS has three stages: translate natural-language question-answer pairs into formal statements, prove and verify them, then use verified proofs in answer selection.The verified formal proofs serve as a foundation connecting formal-language and natural-language reasoning.Source: §2 · pp. 2–3

2.1 From Natural Language to Formal Language

  • The Long CoT translator is trained on aligned NL-FL statements using transfer learning because no Long CoT-annotated translation dataset is available.The training data combine Lean-Workbook and DeepSeek-Prover-v1 examples; the resulting dataset contains 162,181 aligned theorem statements. At inference, the model is prompted to use Long CoT, and translation faithfulness is checked with an LLM or stronger model.Source: §2.1 · pp. 3–4

2.2 Formal Language Proofs and Verification

  • Lean4 provers generate candidate proofs for translated statements, and the Lean4 verifier checks their correctness.The authors use few-shot prompting to align proof formats; because the statements are in standard formal-language form, different provers can be used without modification.Source: §2.2 · p. 4

2.3 Beyond Formal Language Itself

  • When all proof attempts fail, FANS falls back to majority vote or reward-model ranking; verified-answer voting can also revert to ordinary majority vote below a preset threshold.The threshold is intended to mitigate false positives caused by mistranslation; reward-model scores may help identify difficult questions where best-of-N selection is ineffective.Source: §2.3 · p. 4

3 Experiments

FANS is evaluated on MATH500 and AMC23 as a formal-language aid to answer selection and natural-language math reasoning. Results report accuracy improvements across base models and stronger outcomes after external translation verification.

3.1.1 Dataset and Task

  • Experiments evaluate FANS on MATH500’s 500 high-school problems and AMC23’s 40, harder and more varied competition questions.The stated goal is to use formal reasoning to support natural-language reasoning while enhancing majority-vote and optimized-reward-model selection.Source: §3.1.1 · p. 4

3.1.2 Baselines

  • The study compares Mistral-7B, DeepSeek-Math-7B, and Qwen math models, using Qwen-RM-72B for optimized-reward-model baselines.The selected base models span different math-answering capabilities; Qwen-RM-72B is chosen for its size and performance.Source: §3.1.2 · p. 5

3.2 Implementation Details

  • The Long-CoT translator is trained using transfer learning on 162,181 aligned natural-language/formal-language records, with block training and curriculum sorting.Implementation uses DeepSeek-Prover-v1.5, Goedel Prover, and DeepSeek-Prover-v2 as provers, with Santos et al. (2025) as verifier; Lean4 verification runs on CPUs.Source: §3.2 · p. 5

3.3 Results

  • FANS improves answer-selection accuracy across base models, with gains up to 7.90% in algebra and number theory and 1.75% on Qwen2.5-Math.On harder AMC23 questions, FANS also helps weaker models select correct answers.Source: §3.3 · p. 6
  • External-model verification of translations yields better final performance than all baselines, while same-base-model verification gives slight improvements on some datasets.The authors frame the formal backbone as useful when the natural-language-to-formal-language translation is faithful enough.Source: §3.3 · p. 6

3.4 Ablation Studies

Ablations examine the Long-CoT translator and reward-model choice, while a qualitative example follows a natural-language problem through translation, proof, and verification.

3.4.1 Dropping Long CoT in Translator

  • Removing Long CoT significantly lowers MATH500 accuracy, while GPT-4o-mini’s translation performance is also suboptimal.The comparison includes a fine-tuned translator without Long CoT and GPT-4o-mini; the authors attribute the MATH500 drop to less faithful translation.Source: §3.4.1 · p. 6, Table 3 · p. 6

3.4.2 Using different reward models

  • On Mistral-generated data, the Mistral reward model performs best, while other tested reward models show suboptimal performance.The authors interpret this result as evidence that reward models may not generalize to out-of-distribution models or data.Source: §3.4.2 · p. 6, Table 4 · p. 6

3.5 Qualitative Studies

  • In the example, the translator preserves the math problem’s meaning in Lean4, and the prover produces a rigorous proof that the verifier successfully checks.The example concerns finding the product of two integers in a system-of-equations problem.Source: §3.5 · pp. 6–7

4 Related Work

Related work spans formal-language theorem proving, natural-language math reasoning, and reward modeling. The paper distinguishes FANS by using formal-language proofs to assist natural-language answer selection.

4 Related Work

  • Zhou et al. (2024) proposed a similar framework, while FANS trains a Long-CoT translator and uses more advanced models for proofs and translation verification.The paper characterizes the earlier approach as prompt-based and built on weaker base models.Source: §4 · p. 7

4.1 Formal Language Reasoning

  • Prior formal-language systems focus on solving formal problems, while the paper identifies using formal languages to improve natural-language math reasoning as an overlooked opportunity.Formal languages express statements in verifiable first-order logic, and Lean4 is the language selected for FANS.Source: §4.1 · p. 7

4.2 Natural Language Math Reasoning

  • Natural-language math work develops stronger models and inference methods, but the cited approaches remain within natural language and lack formal foundations.The passage names foundation models, Chain-of-Thought, tree search, and Long-CoT approaches.Source: §4.2 · p. 7

4.3 Reward Modeling

  • Reward-model research covers explicit outcome- or process-based rewards and implicit preference-optimization methods such as DPO, KTO, SimPO, and IPO.The passage describes implicit reward modeling as avoiding explicit reward-function engineering.Source: §4.3 · pp. 7–8

5 Conclusion and Discussion

FANS introduces formal-language answer selection and reports gains over baselines, while identifying translation fidelity and prover coverage as constraints on its current reach.

5 Conclusion and Discussion

  • FANS reports relative improvements of 7.9% on MATH500 Number Theory and 20% on AMC23, while remaining below the pass@N upper bound.The paper presents formal-language selection as an alternative to majority voting and reward-model best-of-N methods.Source: §5 · p. 8
  • Translation errors can create false positives, including tautological formalizations of equation-solving problems or misread extremum constraints, leading to vacuous proofs and incorrect selections.The authors identify preserving constraints and explicitly representing optimization conditions as translation-quality needs.Source: §5 · p. 8
  • Lean4’s library support favors algebra and number theory over geometry and combinatorics, and Goedel-Prover still struggles with nearly 40% of proof problems.The authors call for broader library support and stronger proof-search and reasoning capabilities.Source: §5 · p. 8
  • The authors characterize formal verification as a trustworthy, interpretable alternative that reduces dependence on extensive adaptation across base models.They present this as a route toward consistent and scalable improvements in LLM-driven mathematical reasoning.Source: §5 · p. 8

Limitations

FANS is limited by unreliable formal answer selection and by Lean 4's restricted mathematical coverage. The authors identify translation, formulation, and prover improvements as future-work priorities.

Limitations

  • False positives, incomplete provers, and formalization errors can prevent correct answers from being verified or lead to misclassification.The authors also identify Lean 4's limited domain coverage as a constraint on applicability.Source: Limitations · p. 9
  • Lean 4's limited domain coverage constrains FANS to a subset of mathematical fields.Source: Limitations · p. 9
  • Future work targets more robust NL-FL translation, accurate problem formulation, and stronger theorem proving for complex and diverse problems.Source: Limitations · p. 9
  • The authors report no current ethics or societal risks because the work focuses on LLM mathematical reasoning.They say AI assistants were used only for spelling and grammar checking during writing.Source: Limitations · p. 9

A Translator Training Example

The example demonstrates translating an NL math question into a Lean4 theorem statement. At inference, Long-CoT prompting combines with learned Lean4 knowledge to support accurate translation.

A Translator Training Example

B.1 Implementation Settings

FANS yields gains across the evaluated base models, with larger gains on weaker models. The section also describes inference settings and notes that harder problems challenge both translation and proving.

B.1 Implementation Settings

  • Answer generation uses temperature 0.6 and a 4096-token limit; first-stage translation uses temperature 0 and a 2048-token limit, while prover generation uses temperature 1.0 and a 2048-token limit.Source: §B.1 · p. 13
  • The evaluation uses Mistral-7B, DeepSeek-Math-7B-Instruct, Qwen-2.5-Math-1.5B-Instruct, and Qwen2-Math-7B-Instruct as base models.Source: §B.1 · p. 13
  • FANS improves performance across all evaluated base models, with larger gains on weaker models.The latter two models are reported to outperform the former two.Source: §B.1 · p. 14
  • Gains are smaller on stronger base models because harder problems are harder to translate consistently and to prove automatically.The authors point to improving both the translator and prover as future work.Source: §B.1 · p. 14

B.2 Effects of Natural Language Alignment

Natural-language statement alignment does not affect FANS's overall performance in the reported comparison, so the authors omit it in other experiments. The section also gives examples of translation and proof-assisted answer selection.

B.2 Effects of Natural Language Alignment

  • The alignment format recasts a problem as premises followed by a goal, such as “Given ... show that ...” or “If ... prove that ...”.Source: §B.2 · p. 14
  • Using aligned rather than original NL statements does not affect FANS's overall performance, so the authors omit alignment in other experiments.Source: §B.2 · p. 14, Table 6 · p. 15
  • The no-Long-CoT translation prompt uses few-shot examples, while the prover receives the formal statement, proof header, and NL statement as an auxiliary comment.Source: §B.2 · p. 14
  • The section presents examples in which formal language helps select the correct answer from candidate answers.Source: §B.2 · p. 14
Loading 2503.03238v2…