Let's Reason Formally: Natural-Formal Hybrid Reasoning Enhances LLM's Math Capability

• Pure RL can advance math reasoning but may fail to impart capabilities absent from the base model, motivating integration of FL knowledge.Source: §1 · p. 1
• NL problems are often QA-style, whereas FL tasks are fixed-condition proof problems, and FL-oriented outputs can be poorly suited to answering NL questions directly.Source: §1 · p. 2
• NFL-HR translates NL QA into NL existence problems and FL existence theorems, has an FL reasoner address both forms, then extracts the implicit NL answer.Source: §1 · p. 2
• 89.80% on MATH-500 and 84.34% on AMC exceed the Qwen3-8B NL baseline by 4.60% and 4.82%, respectively.Source: §1 · p. 3

2.1.1 QA-existence problem translation

• Directly formalizing an NL QA question can require guessing an answer because FL proof tasks need a goal, and an incorrect guess can confuse the prover.Traditional formulations may put the known answer in the statement, which offers limited utility for deriving an unknown answer.Source: §2.1.1 · p. 3
• A few-shot-prompted LLM reformulates QA as an NL existence problem, which an autoformalizer translates into a Lean4 statement.The existence formulation shifts the task from finding a specific value to proving that a solution exists.Source: §2.1.1 · pp. 3–4, §2.1.2 · p. 4

2.1.2 Autoformalization

• Autoformalization produces a corresponding FL statement from the NL existence problem, mitigating the format gap and enabling the FL reasoner to address the NL question indirectly.Source: §2.1.2 · p. 4

2.2 FL Reasoner Problem Solving

• Mixed Problem Input pairs the NL QA question with its translated FL existence statement, using the prover’s Long CoT to address the question before generating the FL proof.The paper reports that the prover tends to address the NL problem first, even when it mismatches the FL statement.Source: §2.2 · p. 4

2.3 Answer Extraction

• Because the answer is implicit in the prover’s Long CoT and not formatted for verification, a general-purpose LLM extracts it and places it in a boxed answer block.For straightforward extraction, the general LLM is used without thinking mode, while normal CoT is allowed to check the answer.Source: §2.2 · p. 4, §2.3 · p. 5

3.1.1 Dataset

• Evaluation uses pass@16 on MATH-500 and 83 AMC-2022/2023 problems, with Qwen3-8B as the NL baseline.Qwen3-8B also handles format translation and answer extraction; Kimina-Autoformalizer and Kimina-Prover-Preview-7B provide formalization and FL proving.Source: §3.1.1 · p. 5, §3.1.2 · p. 5, §3.2 · p. 5

3.3 Main Results

• Under pass@16, NFL-HR achieves 89.80% on MATH-500 and 84.34% on AMC, outperforming the NL baseline (85.20% and 79.52%, respectively) by 4.60% and 4.82%, respectively.Source: Table 1 · p. 6, §3.3 · p. 6
• The NL baseline varies substantially by subject, while NFL-HR shows consistent and relatively high performance across domains.The paper notes that the baseline excels in algebra and number theory but falters in geometry and precalculus.Source: §3.3 · p. 6

3.4 Study on FL’s Unique Capability

• On the NL-unsolved subset (8.43% of AMC and 4.60% of MATH-500), NL scored 0% at pass@64, while NFL-HR solved all items at pass@16.The subset comprises problems solved by NFL-HR but not by the NL baseline in the main experiment.Source: Table 2 · p. 6, §3.4 · p. 6

3.5 Computation Cost Study

• NFL-HR uses approximately 850 additional tokens per query, while both systems average the same scale of GPU hours in real-time inference.The authors characterize the additional generation cost as a worthwhile trade-off for improved reasoning performance.Source: Table 3 · p. 7, §3.5 · p. 7

3.6.1 Drop existence alignment

• Removing existence alignment reduces accuracy by 4.42% and, on AMC, drops performance below pure NL reasoning.The ablation passes QA-style problems directly to the autoformalizer instead of first converting them to existence problems.Source: §3.6.1 · p. 7

3.6.2 Drop expert FL prover

• Replacing the specialized FL prover with Qwen3-8B lowers average performance by 2.55%, though the variant remains 2.17% above the NL baseline on average.The paper attributes the decrease to the general LLM’s lack of field-specific FL training.Source: §3.6.2 · p. 7

3.7 Case Study

• The case study reports successful QA-to-existence translation, Lean4 formalization and verification, proof generation, and answer extraction.The extracted answer is checked through chain-of-thought reasoning, which the paper says can potentially rectify minor discrepancies in FL reasoning.Source: §3.7 · pp. 7–8

4.1 Natural Math Reasoning

• Pure RL on base models has produced strong Long-CoT results, but studies suggest it refines existing abilities rather than adding capabilities beyond the base model.The discussion presents integration of diverse knowledge sources and reasoning paradigms as a research direction.Source: §4.1 · p. 8

4.2 Formal Math Reasoning

• FL expresses mathematical statements in first-order logic for verifiable reasoning, while prover research has advanced through retrieval, proof translation, formal-data annotation, and Long-CoT systems.The cited approaches include LeanDojo, TheoremLlama, DeepSeek-Prover, Goedel-Prover, STP, MA-LoT, and Kimina-Prover.Source: §4.2 · p. 8
• Few studies directly use FL models to strengthen NL reasoning; prior efforts mainly use formal verification for answer selection or incorporate FL-derived knowledge indirectly during RL.The discussion identifies disparities in problem formulation and reasoning paradigms as part of the integration challenge.Source: §4.2 · p. 8

• NFL-HR aligns NL question-answering problems with FL existence theorems, uses Mixed Problem Input, and extracts answers from FL reasoning.Source: §5 · p. 9
• 89.80% accuracy on MATH-500 and 84.34% on AMC are reported for NFL-HR.Source: §5 · p. 9
• NFL-HR surpasses the NL baseline across all MATH-500 subjects and solves some problems left unsolved by pure NL reasoners.Source: §5 · p. 9

• Pure RL training may not provide knowledge that is weak in the base model, motivating approaches that incorporate broader knowledge into NL reasoning.Source: §6 · p. 9
• NFL-HR is presented as a general setting for integrating expert knowledge from a specific field into reasoning.Source: §6 · p. 9
• The paper describes its contribution as a pipeline applicable beyond math reasoning to knowledge from different fields.Source: §6 · p. 9

Limitations

• FL verifiability is not properly used in the framework, and residual NL-FL format gaps may still hinder performance.Source: Limitations · p. 9

A Discussion of AI usage

• Copilot assisted code-writing and OpenAI models helped fix grammatical issues; the authors state that the ideas are original.Source: A Discussion of AI usage · p. 12

B Term chart

• Tab 5 provides explanations of the paper's terms, abbreviations, and corresponding tools.Source: B Term chart · p. 12

C.1 Problem format study

• The study replaces autoformalization and the FL prover with an NL solver to solve NFL-HR's existence problem.The results are reported as pass@16 in Table 6.Source: §C.1 · p. 12, Table 6 · p. 12
• Simply reformulating problems as existence-style proofs significantly reduces NL-model accuracy, rather than improving it.The authors attribute the reduction to Qwen3 not being specially trained to answer proof questions and conclude that NFL-HR's improvement comes from FL reasoning, not reformatting alone.Source: Table 6 · p. 12, §C.1 · p. 12

C.2 Additional Long CoT models

• With DeepSeek-R1-Distilled-8B-0528, NFL-HR consistently improves over pure NL reasoning, extending the comparison beyond Qwen3.Table 7 reports the comparison under pass@16.Source: §C.2 · p. 12, Table 7 · p. 12

C.3 Generalization of NFL-HR to other fields

• 26.50% versus 22.50% pass@16: NFL-HR outperforms the Qwen3-8B NL baseline on PhysReason-mini.The benchmark uses the first sub-question from each of 200 high-school-level competition problems, with images replaced by captions.Source: §C.3 · p. 12

D Details of models used

• The Lean4 FL reasoner uses RL-trained Lean4 data for Long CoT analysis and proof construction, and is reported to perform at state of the art across multiple theorem-proving benchmarks.The model was developed by the Numina and Kimi teams and introduced in Wang et al. (2025a).Source: D Details of models used · p. 12
• The autoformalizer was trained on problems from four theorem-proving datasets; it achieves 66% one-shot accuracy and over 90% Lean4 compilation success on a 1,000-problem human-curated test set.The 7B base model was fine-tuned as an autoformalizer, with expert iteration using Lean4 verification and LLM judgment (Wang et al., 2025a).Source: D Details of models used · pp. 12–13

E Discussion of verifiability of FL

• FL verifiability provides the FL reasoner’s step-by-step correctness foundation, but does not directly validate or correct NL-generated answers in this work.Direct use of FL to validate or correct NL answers is left for future work.Source: E Discussion of verifiability of FL · p. 13

F Motivation for randomly dropping FL results

• Randomly dropping some FL results lets the NL reasoner solve problems directly when FL reasoning is challenging or unsuitable.The stated motivation is robustness and generality across problem types.Source: F Motivation for randomly dropping FL… · p. 13
• Some probability problems make proving a probability value exists meaningless, while geometry answers in degrees can conflict with Lean4’s radians.These are examples of potential issues in alignment or formal reasoning.Source: F Motivation for randomly dropping FL… · p. 13
• Invalid Lean4 statements from the autoformalizer, or ill-posed NL-FL alignment, are also reasons to drop FL results and let the LLM answer directly.The passage presents this as a way to handle cases where alignment is ill-posed or less meaningful.Source: F Motivation for randomly dropping FL… · p. 13

G FL reasoner’s performance given different NL and FL problems

• The FL prover separately handles NL and FL inputs during Long CoT reasoning, even when the NL problem is unrelated to the FL problem.The authors describe this behavior as evidence of process robustness and as a foundation for Mixed Problem Input.Source: G FL reasoner’s performance given… · pp. 13, 15

H.1 QA-Existence problem translation prompt

• The QA-to-existence prompt recasts answer-seeking tasks as existence claims, with examples spanning polar coordinates, series, and a function-value sum.The template asks for a new translation following its examples.Source: §H.1 · p. 16

H.2 Autoformalization prompt

• The autoformalization prompt, described as mostly similar to Kimina-Autoformalizer’s prompt (Wang et al., 2025a), asks Lean 4 to combine theorems into a more advanced theorem.It supplies an intended theorem name and the NL existence problem.Source: §H.2 · p. 17

H.3 Prover generation prompt

• The prover-generation prompt pairs an NL QA problem with an FL existence statement to elicit Long CoT reasoning, an NL answer, and an FL proof.The prompt asks the model to solve the NL problem step by step in Lean 4 and supplies both inputs.Source: §H.3 · p. 17

H.4 Answer collection prompt

• The answer-collection prompt asks a general LLM to find the NL question’s answer in the prover’s Long CoT content.It provides the NL question and the prover’s Long CoT as inputs.Source: §H.4 · p. 17

I.1 QA-Existence problem translation example

• The translation examples turn a rectangular-to-polar QA task into an existence claim and also provide a series-sum QA-to-existence example.The polar version asks for a point in polar coordinates satisfying the stated range conditions.Source: §I.1 · p. 18
• The translation reframes a numerical QA request as proving that the desired quantity exists and has a specified property.Examples describe proving that a sum exists and is a common fraction, or that a requested conversion number exists.Source: §I.1 · pp. 19, 22

I.2 Autoformalization example

• The conversion problem is formalized as a Lean theorem asserting an x that relates 42 baps to daps and is a rational number.The statement encodes 42 * baps = x * daps and x = q for some q : ℚ.Source: §I.2 · p. 23

I.3 Prover generation example

• 42 baps convert to 70 yaps and then 40 daps under the stated rates.The prover-generation example uses 42 × (5/3) = 70 yaps and 70 × (4/7) = 40 daps.Source: §I.3 · p. 23
• The Lean prover returns 40 daps by proving 42 * baps = 40 * daps and supplying 40 as a rational witness.It uses `linarith` on the conversion equations for the equality and `norm_num` to verify the rational witness.Source: §I.3 · pp. 24–25

I.4 Answer collection example

• The answer-collection example extracts 40 daps from the long CoT by converting 42 baps to 70 yaps, then to daps.The conversions use 5/3 yaps per bap and 4/7 daps per yap.Source: §I.4 · pp. 26–27