Technische Samenvatting: Evaluatie van SageMath-geaugmenteerde LLM-agenten voor computationele en experimentele wiskunde

Probleemstelling

Recente vooruitgang in AI voor wiskunde heeft zich voornamelijk gericht op autoformalisatie (het vertalen van natuurlijke taal naar formele bewijstaal zoals Lean of Coq) en geautomatiseerd bewijsleveren. Hoewel deze benaderingen goudmedailleprestaties in competities hebben behaald en specifieke open problemen hebben opgelost, negeren ze grotendeels de rol van Computer Algebra Systemen (CAS) in de bredere workflow van wiskundig onderzoek.

In computationele en experimentele wiskunde (bijv. combinatorische commutatieve algebra, grafentheorie, eindige groepentheorie) gebruiken onderzoekers routinematig CAS-tools zoals SageMath om hypothesen te verkennen, kandidaten te valideren en tegenvoorbeelden te zoeken. De centrale vraag van dit werk is: In welke mate verbetert verifieerbare symbolische feedback van een CAS de prestaties van frontier LLM's op onderzoeksniveau in de wiskunde, en hoe vormt dit hun gedrag in een agentic setup?

Methodologie

Experimentele Opstelling

De auteurs stellen een ReAct-stijl agentic setup voor waarbij LLM's iteratief interageren met twee tools:

1. SageMath: Een open-source CAS die een verenigde Python-interface biedt aan systemen zoals GAP, Singular en PARI/GP. De agent genereert code, voert deze uit in een geïsoleerde sandbox en ontvangt verifieerbare output.
2. Context7: Een tool die actuele documentatie en codevoorbeelden biedt om hallucinaties met betrekking tot API-signatures en modulepaden te beperken.

De studie evalueert 15 frontier modellen (inclusief GPT-5.5, Claude Opus 4.7/4.8, Qwen 3.7-Max, DeepSeek varianten, en anderen) op een gecureerde subset van 133 problemen op onderzoeksniveau afgeleid van de RealMath benchmark. De dataset is verfijnd om alleen problemen te bevatten met algoritmisch verifieerbare oplossingen (numeriek of symbolische expressies) die geschikt zijn voor SageMath.

Evaluatieprotocol

De evaluatie vergelijkt twee condities voor elk model:

1. Tool-Free Baseline: Direct redeneren zonder externe tools.
2. Tool-Augmented Agentic Setting: Iteratief redeneren met toegang tot SageMath en Context7 (beperkt tot 15 tool-calls per probleem).

Validatiepipeline:
Om de complexiteit van symbolische equivalentie aan te pakken, wordt een hybride validatiepipeline gebruikt:

• Symbolische Validator: Vergelijkt de output van het model met de grondwaarheid met behulp van SymPy. Als het verschil vereenvoudigt tot nul, wordt het antwoord geaccepteerd.
• LLM-as-a-Judge: Gegevens die door de symbolische validator worden afgewezen, worden opnieuw geëvalueerd door drie frontier LLM's (Claude Opus 4.7, GPT-5.5, Gemini 3.5 Flash) via meerderheidsstemming om mathematisch equivalente maar structureel verschillende expressies te vangen.

Belangrijkste Bijdragen

1. Tool-Use Agentic Evaluatie: Een empirische studie die aantoont dat toegang tot een CAS de prestaties op problemen van onderzoeksniveau aanzienlijk verbetert. De studie isoleert het effect van verifieerbare symbolische feedback door middel van gecontroleerde ablatie.
2. Benchmark Verfijning: Een verfijning van de RealMath benchmark, waarbij een meerfasige post-processing pipeline is geïntroduceerd om te filteren op computationele problemen en een LLM-ondersteund normalisatieproces voor uitvoerbare symbolische verificatie.
3. Fout- en Gedragsanalyse: Een granulair onderzoek naar executiefouten, hersteldynamiek en tool-call traces, wat onderscheidende gedragspatronen onthult tussen effectieve en ineffectieve agenten.

Resultaten

Prestatiewinst

• Algehele Verbetering: Tool-toegang verbeterde de solve rate van elk geëvalueerd model, met een gemiddelde winst van +9,7 procentpunten (pp).
• Bereik van Winsten: De winsten varieerden aanzienlijk, van +1,5 pp (Kimi K2.7) tot +27,8 pp (Qwen 3.7-Max, stijgend van 42,1% naar 69,9%).
• Open vs. Gesloten Modellen: Open-weight modellen behaalden gemiddeld aanzienlijk meer winst (+15,3 pp) vergeleken met gesloten frontier modellen (+6,5 pp), voornamelijk door zwakkere tool-free baselines. Echter, CAS-toegang verkleinde de prestatiekloof tussen open en gesloten modellen.
• Top Performers: GPT-5.5 behaalde de hoogste solve rate van 75,2% met het laagste tokengebruik onder de tool-enabled configuraties. Opus 4.8 volgde met 73,7%.

Efficiëntie en Tokengebruik

• Token Inefficiëntie: Hogere tokenuitgave correleerde niet met hogere nauwkeurigheid. Tool-enabled configuraties varieerden van ~34k tot ~556k tokens per probleem.
• Efficiëntie Inversie: Op problemen die oplosbaar waren door alle modellen in de tool-free setting, waren de open-weight modellen het meest token-efficiënt. Echter, op problemen die alleen met tools oplosbaar waren, werden gesloten modellen (GPT-5.5, Opus 4.7/4.8) het meest efficiënt, terwijl open-weight modellen onderaan de ranglijst zakten.

Gedragspatronen

• Bimodale Trace Lengtes: Agentic runs zijn sterk bimodaal. Sterke modellen (Opus 4.7, GPT-5.5) lossen problemen doorgaans op binnen de eerste 3–4 tool-interacties, waarbij ze tools primair gebruiken voor verificatie. Zwakkere modellen putten vaak het volledige budget van 15 calls uit, zoekend naar oplossingen via computationele stappen.
• Hersteldynamiek: Het vermogen om te herstellen van mislukte tool-calls varieerde meer dan de ruwe foutpercentages. Sterke modellen herstelden van fouten in 69–77% van de gevallen, terwijl zwakkere modellen (bijv. Sonnet 5) slechts 16% van de tijd herstelden.
• Fouttypen: De dominante foutmodus was TypeError (786 instanties), wat wijst op onjuiste afhandeling van het Sage-objectensysteem in plaats van syntactische fouten. NameError kwam veel voor bij modellen die er niet in slaagden de interpreter-status over calls heen te behouden.

Domeinspecifieke Bevindingen

• Combinatoriek: Zag de grootste gemiddelde winst (+18,7 pp), consistent met volwassen SageMath-ondersteuning.
• Groepentheorie: Bleef de moeilijkste categorie; hoewel winsten werden waargenomen, overschreed geen enkel model een solve rate van 44%, en tool-toegang verlaagde soms de scores voor specifieke modellen (bijv. GPT-5.5).
• Antwoordtypen: Modellen presteerden over het algemeen beter op numerieke problemen dan op symbolische expressies. Tool-toegang verkleinde deze kloof aanzienlijk voor modellen die zwak zijn in symbolische manipulatie (bijv. Qwen won +36 pp op expressies).

Betekenis en Claims

De auteurs beweren dat CAS-geaugmenteerde agenten een veelbelovende richting vormen voor het assisteren van wiskundigen bij computationele exploratie. De studie demonstreert dat:

1. Verifieerbare Feedback Cruciaal is: Toegang tot een CAS stelt agenten in staat om redeneringen te verfijnen door middel van iteratieve experimenten, waardoor ze de loop van computationeel-wiskundig onderzoek effectief emuleren.
2. Conjectuurontdekking: De casestudy van een twisted torus knot probleem illustreert dat agenten de kernaspecten van de workflow van een wiskundige kunnen reproduceren: het berekenen van intermediaire objecten, het identificeren van patronen, het formuleren van conjecturen en het valideren daarvan over parameters heen.
3. Stap naar Automatisering: Dit werk wordt gepresenteerd als een stap naar geautomatiseerde conjectuurontdekking, wat suggereert dat uitvoerbare symbolische computation de praktische redeneerkracht van frontier modellen aanzienlijk kan uitbreiden voorbij puur bewijsleveren.

Het artikel concludeert dat hoewel huidige systemen beperkt zijn bij problemen die diep theoretisch inzicht of gespecialiseerde hedendaagse kennis vereisen, de geobserveerde winsten aangeven dat de integratie van LLM's met symbolische engines een levensvatbaar pad is voor de vooruitgang van experimentele wiskunde.