Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

O-Forge: An LLM + Computer Algebra Framework for Asymptotic Analysis

Ayush Khaitan, Vijay Ganesh

TL;DR

The paper tackles verification bottlenecks in AI-assisted mathematics by focusing on asymptotic inequalities and proposing the O-Forge framework, which couples frontier LLMs with a CAS to decompose domains into subproblems and verify each piece using quantifier elimination in $Resolve$. Its main contributions are an end-to-end tool and workflow, demonstrated on two case studies, showing that decomposition-guided verification can render difficult estimates tractable for symbolic solvers. This work highlights a path for AI to support research-level mathematics by automating both the discovery of helpful decompositions and the rigorous verification of each subproblem, potentially reducing the time researchers spend on tedious checks. Overall, O-Forge represents a pragmatically verifiable step toward integrating AI into professional mathematical practice.

Abstract

Large language models have recently demonstrated advanced capabilities in solving IMO and Putnam problems; yet their role in research mathematics has remained fairly limited. The key difficulty is verification: suggested proofs may look plausible, but cannot be trusted without rigorous checking. We present a framework, called LLM+CAS, and an associated tool, O-Forge, that couples frontier LLMs with a computer algebra systems (CAS) in an In-Context Symbolic Feedback loop to produce proofs that are both creative and symbolically verified. Our focus is on asymptotic inequalities, a topic that often involves difficult proofs and appropriate decomposition of the domain into the "right" subdomains. Many mathematicians, including Terry Tao, have suggested that using AI tools to find the right decompositions can be very useful for research-level asymptotic analysis. In this paper, we show that our framework LLM+CAS turns out to be remarkably effective at proposing such decompositions via a combination of a frontier LLM and a CAS. More precisely, we use an LLM to suggest domain decomposition, and a CAS (such as Mathematica) that provides a verification of each piece axiomatically. Using this loop, we answer a question posed by Terence Tao: whether LLMs coupled with a verifier can be used to help prove intricate asymptotic inequalities. More broadly, we show how AI can move beyond contest math towards research-level tools for professional mathematicians.

O-Forge: An LLM + Computer Algebra Framework for Asymptotic Analysis

TL;DR

The paper tackles verification bottlenecks in AI-assisted mathematics by focusing on asymptotic inequalities and proposing the O-Forge framework, which couples frontier LLMs with a CAS to decompose domains into subproblems and verify each piece using quantifier elimination in . Its main contributions are an end-to-end tool and workflow, demonstrated on two case studies, showing that decomposition-guided verification can render difficult estimates tractable for symbolic solvers. This work highlights a path for AI to support research-level mathematics by automating both the discovery of helpful decompositions and the rigorous verification of each subproblem, potentially reducing the time researchers spend on tedious checks. Overall, O-Forge represents a pragmatically verifiable step toward integrating AI into professional mathematical practice.

Abstract

Large language models have recently demonstrated advanced capabilities in solving IMO and Putnam problems; yet their role in research mathematics has remained fairly limited. The key difficulty is verification: suggested proofs may look plausible, but cannot be trusted without rigorous checking. We present a framework, called LLM+CAS, and an associated tool, O-Forge, that couples frontier LLMs with a computer algebra systems (CAS) in an In-Context Symbolic Feedback loop to produce proofs that are both creative and symbolically verified. Our focus is on asymptotic inequalities, a topic that often involves difficult proofs and appropriate decomposition of the domain into the "right" subdomains. Many mathematicians, including Terry Tao, have suggested that using AI tools to find the right decompositions can be very useful for research-level asymptotic analysis. In this paper, we show that our framework LLM+CAS turns out to be remarkably effective at proposing such decompositions via a combination of a frontier LLM and a CAS. More precisely, we use an LLM to suggest domain decomposition, and a CAS (such as Mathematica) that provides a verification of each piece axiomatically. Using this loop, we answer a question posed by Terence Tao: whether LLMs coupled with a verifier can be used to help prove intricate asymptotic inequalities. More broadly, we show how AI can move beyond contest math towards research-level tools for professional mathematicians.
Paper Structure (13 sections, 11 equations, 1 figure)

This paper contains 13 sections, 11 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Contributions.
  3. Acknowledgements
  4. Framework: LLM-proposed decomposition + CAS verification
  5. An exploration of asymptotic analysis with O-Forge
  6. Implementation
  7. Empirical Evaluation
  8. Related Work
  9. Limitations and Future Work
  10. Reproducibility
  11. Conclusion
  12. Use of LLMs in Paper preparation
  13. Appendix: Minimal Usage

Figures (1)

  • Figure 1: Workflow: The user inputs a conjectured estimate in LaTeX or natural language; a frontier LLM proposes a domain decomposition; a CAS (Resolve) performs quantifier elimination to rigorously verify the required inequalities.