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

Oct 5, 2026

Enhancing the mathematical reasoning capabilities of LLMs has drawn strong interest in math and computer science. Prior efforts improved natural-language (NL) and formal-language (FL) reasoning, but pure reinforcement learning often cannot add abilities absent from the base model. Integrating FL knowledge into NL math reasoning is hard because NL and FL differ in problem structure and reasoning format. This work proposes NL-FL HybridReasoning (NFL-HR) with NL-FL Problem Alignment, mixed problem input, and answer extraction, achieving high accuracy on MATH-500 and AMC benchmarks.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages27

Reading Time1 h 8 min

AccessFree to download

Abstract

1 Introduction

NL math reasoning

FL reasoning

Let’s Reason Formally: Natural-Formal Hybrid Reasoning Enhances LLM’s Math Capability Ruida Wang1 * , Yuxin Li2 * , Yi R. (May) Fung2 , Tong Zhang1 1University of Illinois Urbana-Champaign, 2Hong Kong University of Science and Technology Correspondence: [rwangbr@connect.ust.hk](rwangbr@connect.ust.hk), [ylinq@connect.ust.hk](ylinq@connect.ust.hk), [yrfung@ust.hk](yrfung@ust.hk), [tongzhang@tongzhang-ml.org](tongzhang@tongzhang-ml.org) Abstract Enhancing the mathematical reasoning capabilities of LLMs has garnered significant attention in both the mathematical and computer science communities. Recent works have made substantial progress in both Natural Language (NL) reasoning and Formal Language (FL) reasoning by leveraging the potential of pure Reinforcement Learning (RL) methods on base models. However, RL approaches struggle to impart new capabilities not presented in the base model (Yue et al., 2025), highlighting the need to integrate more knowledge like FL into NL math reasoning effectively. Yet, this integration is challenging due to inherent disparities in problem structure and reasoning format between NL and FL (Wang et al., 2024) . To address these challenges, we introduce NL-FL HybridReasoning (NFL-HR), an end-to-end framework designed to incorporate the FL expert into NL math problem-solving. To bridge the NL and FL input format gap, we propose the NL-FL Problem Alignment method, which reformulates the Question-Answering (QA) problems in NL as existence theorems in FL. Subsequently, the Mixed Problem Input technique we provide enables the FL reasoner to handle both QA and existence problems concurrently. Lastly, we mitigate the NL and FL output format gap in reasoning through an LLMbased Answer Extraction mechanism. Comprehensive experiments demonstrate that the NFLHR framework achieves 89.80% and 84.34% accuracy rates on the MATH-500 and the AMC benchmarks, surpassing the NL baseline by 4.60% and 4.82%, respectively. Notably, some problems resolved by our framework remain unsolved by the NL baseline model even under a larger number of trials. 1 Introduction The capability of performing rigorous mathematical reasoning has always been regarded as a cornerstone of human intelligence and a fundamental goal *First authors of machine learning systems (Newell and Simon, 1956) . Among these tasks, mathematical reasoning is considered crucial for evaluating the capabilities of Large Language Models (LLMs) . Recently, both academia and industry have been actively working on two branches of LLM math reasoning, namely Natural Language (NL) reasoning and Formal Language (FL) reasoning. In the NL math reasoning, taking advantage of the vast NL data during pre-training, researchers have been continuously making progress in the field during the last few years. Many works tried to enhance LLMs’ Math capability from various perspective (Hendrycks et al., 2021 ; LI et al., 2024 ; Rafailov et al., 2023 ; Wei et al., 2022) . Recent progress in pure Reinforcement Learning (RL) training on base models has notable success in solving IMO-level problems through reflection capability in Long Chain-of-Thought (CoT) (Guo et al., 2025) . However, the latest works have shown that while RL methods fail to introduce novel capabilities beyond the base model (Gandhi et al., 2025) . Consequently, integrating knowledge from other domains, such as FL reasoning, has emerged as a promising direction to enhance LLM’s mathematical reasoning abilities. On the other end, FL reasoning leverages the inherent verifiability of formal systems like Lean (De Moura et al., 2015 ; Moura and Ullrich, 2021), Coq (Coq, 1996), and Isabelle (Paulson, 1994) . They provide a rigorous framework for defining solutions and verifying their correctness. This reliability facilitates large-scale and risk-free data generation (Lin et al., 2025 ; Wang et al., 2025b ; Xin et al., 2024b ; Dong and Ma, 2025), which enables the use of synthetically generated

FAQs

What problem does NL-FL HybridReasoning (NFL-HR) address?

NFL-HR addresses the difficulty of incorporating formal-language (FL) knowledge into natural-language (NL) math reasoning, where NL and FL differ in structure and reasoning format.

How does NFL-HR align NL QA problems with FL existence theorems?

It uses NL-FL Problem Alignment to reformulate NL question-answering problems as existence theorems in FL, bridging the input-format gap.

What techniques help NFL-HR handle both NL and FL reasoning outputs?

NFL-HR employs a mixed problem input method for joint solving and an LLM-based Answer Extraction mechanism to mitigate the NL/FL output-format gap.

Oct 5, 2026

Upload by WPS_1790064749