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

• URL: http://arxiv.org/abs/2503.03238v1
• Date: Wed, 05 Mar 2025 07:34:53 GMT
• Title: FANS -- Formal Answer Selection for Natural Language Math Reasoning Using Lean4
• Authors: Jiarui Yao, Ruida Wang, Tong Zhang,
• Abstract summary: We propose a novel framework named FANS: Formal ANswer Selection for Natural Language Math Reasoning Using Lean4.<n>It is the first framework that utilizes Lean4 to enhance LLMs' NL math reasoning ability.<n>It enhances LLMs' NL math ability in providing a computer-verifiable solution for its correct answer.
• Score: 9.732905760042193
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• CLR-Bench: Evaluating Large Language Models in College-level Reasoning [17.081788240112417]
  Large language models (LLMs) have demonstrated their remarkable performance across various language understanding tasks. We present CLR-Bench to comprehensively evaluate the LLMs in complex college-level reasoning.
  arXiv  Detail & Related papers  (2024-10-23T04:55:08Z)
• GIVE: Structured Reasoning of Large Language Models with Knowledge Graph Inspired Veracity Extrapolation [108.2008975785364]
  Graph Inspired Veracity Extrapolation (GIVE) is a novel reasoning method that merges parametric and non-parametric memories to improve accurate reasoning with minimal external input.<n>GIVE guides the LLM agent to select the most pertinent expert data (observe), engage in query-specific divergent thinking (reflect), and then synthesize this information to produce the final output (speak)
  arXiv  Detail & Related papers  (2024-10-11T03:05:06Z)
• TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts [26.98890165420689]
  TheoremLlama is an end-to-end framework that trains a general-purpose Lean4 expert. Our framework achieves cumulative accuracies of 36.48% and 33.61% on MiniF2F-Valid and Test datasets respectively.
  arXiv  Detail & Related papers  (2024-07-03T15:36:18Z)
• Perception of Knowledge Boundary for Large Language Models through Semi-open-ended Question Answering [67.94354589215637]
  Large Language Models (LLMs) are widely used for knowledge-seeking yet suffer from hallucinations. In this paper, we perceive the LLMs' knowledge boundary (KB) with semi-open-ended questions (SoeQ) We find that GPT-4 performs poorly on SoeQ and is often unaware of its KB. Our auxiliary model, LLaMA-2-13B, is effective in discovering more ambiguous answers.
  arXiv  Detail & Related papers  (2024-05-23T10:00:14Z)
• Can LLMs Master Math? Investigating Large Language Models on Math Stack Exchange [25.419977967846144]
  Large Language Models (LLMs) have demonstrated exceptional capabilities in various natural language tasks. This paper explores the current limitations of LLMs in navigating complex mathematical problem-solving.
  arXiv  Detail & Related papers  (2024-03-30T12:48:31Z)
• LogicAsker: Evaluating and Improving the Logical Reasoning Ability of Large Language Models [63.14196038655506]
  We introduce LogicAsker, a novel approach for evaluating and enhancing the logical reasoning capabilities of large language models (LLMs) Our methodology reveals significant gaps in LLMs' learning of logical rules, with identified reasoning failures ranging from 29% to 90% across different models. We leverage these findings to construct targeted demonstration examples and fine-tune data, notably enhancing logical reasoning in models like GPT-4o by up to 5%.
  arXiv  Detail & Related papers  (2024-01-01T13:53:53Z)
• Supervised Knowledge Makes Large Language Models Better In-context Learners [94.89301696512776]
  Large Language Models (LLMs) exhibit emerging in-context learning abilities through prompt engineering. The challenge of improving the generalizability and factuality of LLMs in natural language understanding and question answering remains under-explored. We propose a framework that enhances the reliability of LLMs as it: 1) generalizes out-of-distribution data, 2) elucidates how LLMs benefit from discriminative models, and 3) minimizes hallucinations in generative tasks.
  arXiv  Detail & Related papers  (2023-12-26T07:24:46Z)
• The ART of LLM Refinement: Ask, Refine, and Trust [85.75059530612882]
  We propose a reasoning with refinement objective called ART: Ask, Refine, and Trust. It asks necessary questions to decide when an LLM should refine its output. It achieves a performance gain of +5 points over self-refinement baselines.
  arXiv  Detail & Related papers  (2023-11-14T07:26:32Z)
• Knowing What LLMs DO NOT Know: A Simple Yet Effective Self-Detection Method [36.24876571343749]
  Large Language Models (LLMs) have shown great potential in Natural Language Processing (NLP) tasks. Recent literature reveals that LLMs generate nonfactual responses intermittently. We propose a novel self-detection method to detect which questions that a LLM does not know that are prone to generate nonfactual results.
  arXiv  Detail & Related papers  (2023-10-27T06:22:14Z)
• LaGR-SEQ: Language-Guided Reinforcement Learning with Sample-Efficient Querying [71.86163159193327]
  Large language models (LLMs) have recently demonstrated their impressive ability to provide context-aware responses via text. This ability could potentially be used to predict plausible solutions in sequential decision making tasks pertaining to pattern completion. We introduce LaGR, which uses this predictive ability of LLMs to propose solutions to tasks that have been partially completed by a primary reinforcement learning (RL) agent.
  arXiv  Detail & Related papers  (2023-08-21T02:07:35Z)
• Statistical Knowledge Assessment for Large Language Models [79.07989821512128]
  Given varying prompts regarding a factoid question, can a large language model (LLM) reliably generate factually correct answers? We propose KaRR, a statistical approach to assess factual knowledge for LLMs. Our results reveal that the knowledge in LLMs with the same backbone architecture adheres to the scaling law, while tuning on instruction-following data sometimes compromises the model's capability to generate factually correct text reliably.
  arXiv  Detail & Related papers  (2023-05-17T18:54:37Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.