Technical Summary: Evaluating SageMath-Augmented LLM Agents for Computational and Experimental Mathematics

Problem Statement

Recent advances in AI for mathematics have predominantly focused on autoformalization (translating natural language to formal proof languages like Lean or Coq) and automated theorem proving. While these approaches have achieved gold-medal performance on competitions and resolved specific open problems, they largely overlook the role of Computer Algebra Systems (CAS) in the broader workflow of mathematical research.

In computational and experimental mathematics (e.g., combinatorial commutative algebra, graph theory, finite group theory), researchers routinely use CAS tools like SageMath to explore hypotheses, validate candidates, and search for counterexamples. However, the integration of these symbolic engines into agentic Large Language Model (LLM) workflows remains underexplored. The central question of this work is: To what extent does verifiable symbolic feedback from a CAS improve the performance of frontier LLMs on research-level mathematics, and how does it shape their behavior in an agentic setup?

Methodology

Experimental Setup

The authors propose a ReAct-style agentic setup where LLMs interact iteratively with two tools:

1. SageMath: An open-source CAS providing a unified Python interface to systems like GAP, Singular, and PARI/GP. The agent generates code, executes it in an isolated sandbox, and receives verifiable output.
2. Context7: A tool providing up-to-date documentation and code examples to mitigate hallucinations regarding API signatures and module paths.

The study evaluates 15 frontier models (including GPT-5.5, Claude Opus 4.7/4.8, Qwen 3.7-Max, DeepSeek variants, and others) on a curated subset of 133 research-level problems derived from the RealMath benchmark. The dataset was refined to include only problems with algorithmically verifiable solutions (numerical or symbolic expressions) suitable for SageMath.

Evaluation Protocol

The evaluation compares two conditions for each model:

1. Tool-Free Baseline: Direct reasoning without external tools.
2. Tool-Augmented Agentic Setting: Iterative reasoning with access to SageMath and Context7 (capped at 15 tool calls per problem).

Validation Pipeline:
To handle the complexity of symbolic equivalence, a hybrid validation pipeline is employed:

• Symbolic Validator: Compares model output against ground truth using SymPy. If the difference simplifies to zero, the answer is accepted.
• LLM-as-a-Judge: Cases rejected by the symbolic validator are re-evaluated by three frontier LLMs (Claude Opus 4.7, GPT-5.5, Gemini 3.5 Flash) via majority voting to catch mathematically equivalent but structurally different expressions.

Key Contributions

1. Tool-Use Agentic Evaluation: An empirical study demonstrating that access to a CAS significantly improves performance on research-level problems. The study isolates the effect of verifiable symbolic feedback through controlled ablation.
2. Benchmark Refinement: A refinement of the RealMath benchmark, introducing a multi-stage post-processing pipeline to filter for computable problems and an LLM-assisted normalization process for executable symbolic verification.
3. Error and Behavioral Analysis: A granular analysis of execution failures, recovery dynamics, and tool-call traces, revealing distinct behavioral patterns between effective and ineffective agents.

Results

Performance Gains

• Overall Improvement: Tool access improved the solve rate of every evaluated model, with an average gain of +9.7 percentage points (pp).
• Range of Gains: Gains varied significantly, from +1.5 pp (Kimi K2.7) to +27.8 pp (Qwen 3.7-Max, rising from 42.1% to 69.9%).
• Open vs. Closed Models: Open-weight models gained significantly more on average (+15.3 pp) compared to closed frontier models (+6.5 pp), largely due to weaker tool-free baselines. However, CAS access narrowed the performance gap between open and closed models.
• Top Performers: GPT-5.5 achieved the highest solve rate of 75.2% with the lowest token usage among tool-enabled configurations. Opus 4.8 followed with 73.7%.

Efficiency and Token Usage

• Token Inefficiency: Higher token expenditure did not correlate with higher accuracy. Tool-enabled configurations ranged from ~34k to ~556k tokens per problem.
• Efficiency Inversion: On problems solvable by all models in the tool-free setting, open-weight models were the most token-efficient. However, on problems solvable only with tools, closed models (GPT-5.5, Opus 4.7/4.8) became the most efficient, while open-weight models dropped to the bottom of the ranking.

Behavioral Patterns

• Bimodal Trace Lengths: Agentic runs are strongly bimodal. Strong models (Opus 4.7, GPT-5.5) typically solve problems within the first 3–4 tool interactions, using tools primarily for verification. Weaker models often exhaust the full 15-call budget, searching for solutions through computation.
• Recovery Dynamics: The ability to recover from failed tool calls varied more than raw failure rates. Strong models recovered from failures 69–77% of the time, whereas weaker models (e.g., Sonnet 5) recovered only 16% of the time.
• Error Types: The dominant failure mode was TypeError (786 instances), reflecting incorrect handling of Sage's object system rather than syntax errors. NameError was common in models that failed to maintain interpreter state across calls.

Domain-Specific Findings

• Combinatorics: Saw the largest mean gain (+18.7 pp), consistent with mature SageMath support.
• Group Theory: Remained the hardest category; while gains were observed, no model exceeded a 44% solve rate, and tool access sometimes lowered scores for specific models (e.g., GPT-5.5).
• Answer Types: Models generally performed better on numerical problems than symbolic expressions. Tool access significantly narrowed this gap for models weak in symbolic manipulation (e.g., Qwen gained +36 pp on expressions).

Significance and Claims

The authors claim that CAS-augmented agents represent a promising direction for assisting mathematicians in computational exploration. The study demonstrates that:

1. Verifiable Feedback is Critical: Access to a CAS allows agents to refine reasoning through iterative experimentation, effectively emulating a computational-mathematics research loop.
2. Conjecture Discovery: The case study of a twisted torus knot problem illustrates that agents can reproduce key elements of a mathematician's workflow: computing intermediate objects, identifying patterns, formulating conjectures, and validating them across parameters.
3. Step Toward Automation: This work is presented as a step toward automated conjecture discovery, suggesting that executable symbolic computation can substantially extend the practical reasoning capabilities of frontier models beyond pure theorem proving.

The paper concludes that while current systems are limited on problems requiring deep theoretical insight or specialized contemporary knowledge, the observed gains indicate that integrating LLMs with symbolic engines is a viable path for advancing experimental mathematics.