Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning

• URL: http://arxiv.org/abs/2502.13834v3
• Date: Thu, 27 Feb 2025 04:24:25 GMT
• Title: Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning
• Authors: Zenan Li, Zhaoyu Li, Wen Tang, Xian Zhang, Yuan Yao, Xujie Si, Fan Yang, Kaiyu Yang, Xiaoxing Ma,
• Abstract summary: Large language models (LLMs) can prove mathematical theorems formally by generating proof steps within a proof system.<n>We introduce a neuro-symbolic tactic generator that synergizes the mathematical intuition learned by LLMs with domain-specific insights encoded by symbolic methods.<n>We evaluate our framework on 161 challenging inequalities from multiple mathematics competitions.
• Score: 27.562284768743694
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large language models (LLMs) can prove mathematical theorems formally by generating proof steps (\textit{a.k.a.} tactics) within a proof system. However, the space of possible tactics is vast and complex, while the available training data for formal proofs is limited, posing a significant challenge to LLM-based tactic generation. To address this, we introduce a neuro-symbolic tactic generator that synergizes the mathematical intuition learned by LLMs with domain-specific insights encoded by symbolic methods. The key aspect of this integration is identifying which parts of mathematical reasoning are best suited to LLMs and which to symbolic methods. While the high-level idea of neuro-symbolic integration is broadly applicable to various mathematical problems, in this paper, we focus specifically on Olympiad inequalities (Figure~1). We analyze how humans solve these problems and distill the techniques into two types of tactics: (1) scaling, handled by symbolic methods, and (2) rewriting, handled by LLMs. In addition, we combine symbolic tools with LLMs to prune and rank the proof goals for efficient proof search. We evaluate our framework on 161 challenging inequalities from multiple mathematics competitions, achieving state-of-the-art performance and significantly outperforming existing LLM and symbolic approaches without requiring additional training data.

Related papers

• Enhancing the Geometric Problem-Solving Ability of Multimodal LLMs via Symbolic-Neural Integration [57.95306827012784]
  We propose GeoGen, a pipeline that can automatically generate step-wise reasoning paths for geometry diagrams. By leveraging the precise symbolic reasoning, textbfGeoGen produces large-scale, high-quality question-answer pairs. We train textbfGeoLogic, a Large Language Model (LLM), using synthetic data generated by GeoGen.
  arXiv  Detail & Related papers  (2025-04-17T09:13:46Z)
• Lemmanaid: Neuro-Symbolic Lemma Conjecturing [4.583367875081881]
  We present the first steps towards a practical neuro-symbolic lemma conjecturing tool, Lemmanaid. We train an LLM to generate lemma templates that describe the shape of a lemma, and use symbolic methods to fill in the details. We compare Lemmanaid against an LLM trained to generate complete lemma statements as well as previous fully symbolic conjecturing methods.
  arXiv  Detail & Related papers  (2025-04-07T11:30:36Z)
• Challenging the Boundaries of Reasoning: An Olympiad-Level Math Benchmark for Large Language Models [86.45058529521258]
  OlymMATH is a novel Olympiad-level mathematical benchmark designed to rigorously test the complex reasoning capabilities of LLMs. OlymMATH features 200 meticulously curated problems, each manually verified and available in parallel English and Chinese versions.
  arXiv  Detail & Related papers  (2025-03-27T11:20:17Z)
• Formalizing Complex Mathematical Statements with LLMs: A Study on Mathematical Definitions [8.135142928659546]
  We introduce two novel resources for autoformalization, collecting definitions from Wikipedia (Def_Wiki) and arXiv papers (Def_ArXiv) We evaluate a range of LLMs, analyzing their ability to formalize definitions into Isabelle/HOL. Our findings reveal that definitions present a greater challenge compared to existing benchmarks, such as miniF2F.
  arXiv  Detail & Related papers  (2025-02-17T17:34:48Z)
• MathFimer: Enhancing Mathematical Reasoning by Expanding Reasoning Steps through Fill-in-the-Middle Task [49.355810887265925]
  We introduce MathFimer, a novel framework for mathematical reasoning step expansion. We develop a specialized model, MathFimer-7B, on our carefully curated NuminaMath-FIM dataset. We then apply these models to enhance existing mathematical reasoning datasets by inserting detailed intermediate steps into their solution chains.
  arXiv  Detail & Related papers  (2025-02-17T11:22:24Z)
• One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs [57.48325300739872]
  Leveraging mathematical Large Language Models for proof generation is a fundamental topic in LLMs research.<n>We argue that the ability of current LLMs to prove statements largely depends on whether they have encountered the relevant proof process during training.<n>Inspired by the pedagogical method of "proof by counterexamples" commonly used in human mathematics education, our work aims to enhance LLMs' ability to conduct mathematical reasoning and proof through counterexamples.
  arXiv  Detail & Related papers  (2025-02-12T02:01:10Z)
• Large Language Models for Mathematical Analysis [3.7325315394927023]
  This work addresses critical gaps in mathematical reasoning and contributes to advancing trustworthy AI.<n>We developed the DEMI-MathAnalysis dataset, comprising proof-based problems from mathematical analysis topics.<n>We also designed a guiding framework to rigorously enhance LLMs' ability to solve these problems.
  arXiv  Detail & Related papers  (2024-12-28T20:37:55Z)
• System-2 Mathematical Reasoning via Enriched Instruction Tuning [13.672967091915181]
  Enriched Instruction Tuning (EIT) is a method that enriches existing human-annotated mathematical datasets by synergizing human and AI feedback.<n>EIT achieves an accuracy of 84.1% on GSM8K and 32.5% on MATH, surpassing state-of-the-art fine-tuning and prompting methods.
  arXiv  Detail & Related papers  (2024-12-22T10:49:27Z)
• Unraveling Arithmetic in Large Language Models: The Role of Algebraic Structures [3.181878085746691]
  Large language models (LLMs) have demonstrated remarkable mathematical capabilities, largely driven by chain-of-thought (CoT) prompting. We propose that LLMs learn arithmetic by capturing algebraic structures, such as emphCommutativity and emphIdentity properties. Our findings indicate that leveraging algebraic structures can enhance the LLMs' arithmetic capabilities, offering insights into improving their arithmetic performance.
  arXiv  Detail & Related papers  (2024-11-25T10:23:11Z)
• LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
  We present LeanAgent, a novel lifelong learning framework for formal theorem proving. LeanAgent continuously generalizes to and improves on ever-expanding mathematical knowledge. It successfully proves 155 theorems previously unproved formally by humans across 23 diverse Lean repositories.
  arXiv  Detail & Related papers  (2024-10-08T17:11:24Z)
• GSM-Plus: A Comprehensive Benchmark for Evaluating the Robustness of LLMs as Mathematical Problem Solvers [68.77382332826167]
  Large language models (LLMs) have achieved impressive performance across various mathematical reasoning benchmarks. One essential and frequently occurring evidence is that when the math questions are slightly changed, LLMs can behave incorrectly. This motivates us to evaluate the robustness of LLMs' math reasoning capability by testing a wide range of question variations.
  arXiv  Detail & Related papers  (2024-02-29T15:26:14Z)
• Evaluating LLMs' Mathematical and Coding Competency through Ontology-guided Interventions [47.83142414018448]
  We focus on two popular reasoning tasks: arithmetic reasoning and code generation. We introduce (i) a general ontology of perturbations for math and coding questions, (ii) a semi-automatic method to apply these perturbations, and (iii) two datasets. We show a significant performance drop across all the models against perturbed questions.
  arXiv  Detail & Related papers  (2024-01-17T18:13:07Z)

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.