Proving Olympiad Algebraic Inequalities without Human Demonstrations

• URL: http://arxiv.org/abs/2406.14219v2
• Date: Thu, 31 Oct 2024 03:24:06 GMT
• Title: Proving Olympiad Algebraic Inequalities without Human Demonstrations
• Authors: Chenrui Wei, Mengzhou Sun, Wei Wang,
• Abstract summary: We propose AIPS, an Algebraic Inequality Proving System capable of autonomously generating complex inequality theorems. On a test set of 20 Olympiad-level inequality problems, AIPS successfully solved 10, outperforming state-of-the-art methods. One theorem was selected as a competition problem in a major city 2024 Mathematical Olympiad.
• Score: 3.3466865213133836
• License:
• Abstract: Solving Olympiad-level mathematical problems represents a significant advancement in machine intelligence and automated reasoning. Current machine learning methods, however, struggle to solve Olympiad-level problems beyond Euclidean plane geometry due to a lack of large-scale, high-quality datasets. The challenge is even greater in algebraic systems, which involve infinite reasoning spaces within finite conditions. To address these issues, we propose AIPS, an Algebraic Inequality Proving System capable of autonomously generating complex inequality theorems and effectively solving Olympiad-level inequality problems without requiring human demonstrations. During proof search in a mixed reasoning manner, a value curriculum learning strategy on generated datasets is implemented to improve proving performance, demonstrating strong mathematical intuitions. On a test set of 20 International Mathematical Olympiad-level inequality problems, AIPS successfully solved 10, outperforming state-of-the-art methods. Furthermore, AIPS automatically generated a vast array of non-trivial theorems without human intervention, some of which have been evaluated by professional contestants and deemed to reach the level of the International Mathematical Olympiad. Notably, one theorem was selected as a competition problem in a major city 2024 Mathematical Olympiad.

Related papers

• Large Language Models for Mathematical Analysis [3.7325315394927023]
  This work addresses critical gaps in mathematical reasoning and contributes to advancing trustworthy AI. We developed the DEMI-MathAnalysis dataset, comprising proof-based problems from mathematical analysis topics. We also designed a guiding framework to rigorously enhance LLMs' ability to solve these problems.
  arXiv  Detail & Related papers  (2024-12-28T20:37:55Z)
• Proposing and solving olympiad geometry with guided tree search [63.824930029019995]
  We introduce TongGeometry, a Euclidean geometry system supporting tree-search-based guided problem proposing and solving. TongGeometry discovers 6.7 billion geometry theorems requiring auxiliary constructions, including 4.1 billion exhibiting geometric symmetry. TongGeometry solved all International Mathematical Olympiad geometry in IMO-AG-30, outperforming gold medalists for the first time.
  arXiv  Detail & Related papers  (2024-12-14T04:20:47Z)
• MathGAP: Out-of-Distribution Evaluation on Problems with Arbitrarily Complex Proofs [80.96119560172224]
  MathGAP generates problem statements and chain-of-thought reasoning traces according to specifications about their arithmetic proof structure. Using MathGAP, we find that LLMs show a significant decrease in performance as proofs get deeper and wider.
  arXiv  Detail & Related papers  (2024-10-17T12:48:14Z)
• Omni-MATH: A Universal Olympiad Level Mathematic Benchmark For Large Language Models [63.31878920079154]
  We propose a benchmark specifically designed to assess large language models' mathematical reasoning at the Olympiad level. Unlike existing Olympiad-related benchmarks, our dataset focuses exclusively on mathematics and comprises a vast collection of 4428 competition-level problems with rigorous human annotation. Our experimental results show that even the most advanced models, OpenAI o1-mini and OpenAI o1-preview, struggle with highly challenging Olympiad-level problems, with 60.54% and 52.55% accuracy, highlighting significant challenges in Olympiad-level mathematical reasoning.
  arXiv  Detail & Related papers  (2024-10-10T14:39:33Z)
• Evaluating Large Vision-and-Language Models on Children's Mathematical Olympiads [74.54183505245553]
  A systematic analysis of AI capabilities for joint vision and text reasoning is missing in the current scientific literature. We evaluate state-of-the-art LVLMs on their mathematical and algorithmic reasoning abilities using visuo-linguistic problems from children's Olympiads. Our results show that modern LVLMs do demonstrate increasingly powerful reasoning skills in solving problems for higher grades, but lack the foundations to correctly answer problems designed for younger children.
  arXiv  Detail & Related papers  (2024-06-22T05:04:39Z)
• OlympicArena: Benchmarking Multi-discipline Cognitive Reasoning for Superintelligent AI [73.75520820608232]
  We introduce OlympicArena, which includes 11,163 bilingual problems across both text-only and interleaved text-image modalities. These challenges encompass a wide range of disciplines spanning seven fields and 62 international Olympic competitions, rigorously examined for data leakage. Our evaluations reveal that even advanced models like GPT-4o only achieve a 39.97% overall accuracy, illustrating current AI limitations in complex reasoning and multimodal integration.
  arXiv  Detail & Related papers  (2024-06-18T16:20:53Z)
• Mathify: Evaluating Large Language Models on Mathematical Problem Solving Tasks [34.09857430966818]
  We introduce an extensive mathematics dataset called "MathQuest" sourced from the 11th and 12th standard Mathematics NCERT textbooks. We conduct fine-tuning experiments with three prominent large language models: LLaMA-2, WizardMath, and MAmmoTH. Our experiments reveal that among the three models, MAmmoTH-13B emerges as the most proficient, achieving the highest level of competence in solving the presented mathematical problems.
  arXiv  Detail & Related papers  (2024-04-19T08:45:42Z)
• OlympiadBench: A Challenging Benchmark for Promoting AGI with Olympiad-Level Bilingual Multimodal Scientific Problems [62.06169250463104]
  We present OlympiadBench, an Olympiad-level bilingual multimodal scientific benchmark, featuring 8,476 problems from Olympiad-level mathematics and physics competitions. The best-performing model, GPT-4V, attains an average score of 17.97% on OlympiadBench, with a mere 10.74% in physics. Our analysis orienting GPT-4V points out prevalent issues with hallucinations, knowledge omissions, and logical fallacies.
  arXiv  Detail & Related papers  (2024-02-21T18:49:26Z)

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.