Stel je voor dat je een complex wiskundig probleem probeert op te lossen, maar in plaats van een briljante maar soms overmoedige genie te vragen, vraag je het aan een zeer georganiseerde, licht rigide, maar ongelooflijk eerlijke bibliothecaris.

Dat is de kern van het idee achter AXIOM, een nieuw systeem dat is ontworpen om wiskundige redeneringen uit te voeren met een "trust-first" (vertrouwen eerst) mentaliteit. Hier is hoe het werkt, uitgelegd aan de hand van eenvoudige concepten en analogieën.

Het Probleem: De "Zelfverzekerd Onjuiste" Genie

Huidige AI-modellen (zoals de modellen waarmee je chat) zijn als briljante studenten die ervan houden om te gokken. Als ze het antwoord niet weten, verzinnen ze gewoon iets en presenteren ze dat met totale zelfverzekerdheid. In de wiskunde is dit gevaarlijk, omdat een fout antwoord er precies hetzelfde uitziet als een goed antwoord voor de gebruiker. Je hebt geen manier om te weten of de AI liegt of gewoon hallucineert.

De AXIOM Oplossing: De "Gespecialiseerde Assemblagelijn"

AXIOM probeert niet een genie te zijn die alles vanuit het niets oplost. In plaats daarvan fungeert het als een uiterst efficiënte fabrieksassemblagelijn met vier strikte regels:

1. De Sorter (De Regex Router)

Wanneer een vraag binnenkomt, gaat deze niet direct naar de AI. Eerst komt het door een Sorter. Denk aan dit als een postkamerbediende die naar de vorm van de envelop kijkt.

Als de brief lijkt op een "eenvoudige rekenkundige" notitie, wordt deze naar de Fast Lane gestuurd.
Als het eruitziet als een "algebra" notitie, gaat het naar het Algebra Station.
Als de vorm niet overeenkomt met een bekende categorie, stempelt de bediende het direct als "Onbekend" en stopt het proces. Het gokt nooit.

2. De Translator (De AI als een "Rewriter")

Als de brief een station bereikt, vraagt het de AI niet om het probleem op te lossen. In plaats daarvan fungeert de AI als een Translator.

Oude manier: "Hier is een tekstprobleem, los het alsjeblieft op." (De AI raadt de stappen).
AXIOM Manier: "Hier is een tekstprobleem. Schrijf het hersen alsjeblieft om naar dit specifieke, nauwe formaat dat onze rekenmachine begrijpt."
De AI is strikt verboden om de wiskunde zelf te doen. Het ruimt alleen de zin op zodat de volgende stap het perfect kan lezen.

3. De Calculator (De Deterministische Engine)

Zodra de AI het probleem heeft herschreven, geeft het het door aan een Calculator (een computer algebra systeem). Dit is een robot die nooit gokt, nooit moe wordt en nooit hallucineert.

Het neemt het herschreven probleem en voert de berekeningen uit.
Als het het probleem kan oplossen, geeft het het antwoord.
Als het dat niet kan (misschien is de wiskunde te vreemd of is de input iets afwijkend), dan stopt het en zegt: "Ik kan dit niet verifiëren."

4. De "Eerlijkheidsregel" (Abstaining)

Dit is het belangrijkste deel. In de meeste systemen, als de calculator faalt, probeert het systeem toch nog te gokken. In AXIOM is zeggen "ik weet het niet" een geldig, gestructureerd antwoord.
Als een onderdeel van de lijn faalt (de Sorter herkende de vorm niet, de Translator kon het niet herschrijven, of de Calculator kon het niet oplossen), geeft het systeem een duidelijke boodschap uit: "Ik onthoud mij van een antwoord" (I am abstaining). Het geeft nooit een zelfverzekerd fout antwoord.

De Resultaten: Snelheid en Veiligheid

Het paper rapporteert enkele indrukwekkende statistieken uit tests van dit systeem:

Nul Zelfverzekerde Fouten: Over duizenden tests heen, gaf het systeem nooit een fout antwoord dat leek op een goed antwoord. Als het een antwoord gaf, was het geverifieerd.
Hoge Nauwkeurigheid: Op standaard wiskundetoetsen haalde het ongeveer 94% van de vragen goed.
Snelheid: Voor simpele wiskunde (zoals "2 + 2") slaat het de AI-translator volledig over en lost het dit op in 1 milliseconde (sneller dan je kunt knipperen). Voor moeilijkere zaken is het nog steeds sneller dan een standaard AI vragen om "stap voor stap na te denken".
Kosten: Omdat het de AI niet vraagt om lange essays te schrijven of te gokken, kost het bijna niets om te draaien.

De "Forward Dynamic": Beter Worden Zonder te Breken

De auteurs benadrukken dat dit systeem is ontworpen om te groeien.

Stel dat het systeem een nieuw type wiskundig probleem tegenkomt dat het niet kent. In plaats van stilzwijgend te falen of te gokken, logt het: "Ik zag deze vorm, maar ik heb geen station voor deze vorm."
De ontwikkelaars kunnen dan een nieuw "Station" (een nieuwe regel) bouwen specif kind aan die vorm.
Omdat elk station geïsoleerd is, breekt het toevoegen van een nieuw station nooit de oude stations. Het is als het toevoegen van een nieuwe rijstrook aan een snelweg; het veroorzaakt geen verkeersopstoppingen in de bestaande rijstroken.

Samenvattende Analogie

Denk aan een standaard AI als een magiër die antwoorden uit een hoed tovert. Soms is het konijn er wel, en soms is het een sok, maar de magiër doet alsof het een konijn is.

AXIOM is een kwaliteitscontroleur.

Het controleert of het item in de doos past.
Het labelt het item duidelijk.
Het stuurt het door een machine die het meet.
Als de machine het niet kan meten, plakt het een "Afgekeurd" label erop.

Het zal misschien meer items afkeuren dan een magiër zou doen, maar elk item dat de fabriek verlaat met een "Goedgekeurd" label, is gegarandeerd correct.

Technische Samenvatting: AXIOM – Een Trust-First Neuro-Symbolische Executiearchitectuur

1. Probleemstelling

Het artikel behandelt het fundamentele gebrek aan verifieerbaarheid in de wiskundige redenering van frontier Large Language Models (LLM's). Hoewel LLM's hoge nauwkeurigheid bereiken op benchmarks, opereren ze via een "prompt-in-tekst-uit" interface waarbij een zelfverzekend foutief antwoord structureel niet te onderscheiden is van een correct antwoord. Bestaande alternatieven hebben aanzienlijke trade-offs:

Lean-gebaseerde bewijzers vereisen dat problemen vooraf worden geformaliseerd in een specifieke syntaxis (bijv. Lean), wat een bottleneck creëert voor natuurlijke taalvragen.
Gesloten expertsystemen (bijv. Wolfram Alpha) bieden symbolische backends, maar missen LLM-augmentatie aan de inputzijde en bieden geen inspecteerbare afleidingssporen.

De auteurs stellen dat "zelfverzekerd-foutief" de slechtste faalmodus is in wiskundige redenering. Ze stellen voor om het ontwerndoel te verschuiven van "nauwkeurigheid-eerst" naar "vertrouwen-eerst", waarbij vertrouwen wordt gedefinieerd als $1 - \frac{\text{fout}}{\text{poging}}$ , waarbij "fout" die records uitsluit waarbij het systeem expliciet weigert antwoord te geven.

2. Methodologie: De AXIOM Architectuur

AXIOM is een neuro-symbolische executiearchitectuur waarbij de LLM strikt fungeert als een canonicalizer, niet als een solver. Het systeem stuurt natuurlijke taal (NL) input door een deterministische Computer Algebra System (CAS) pipeline. Het kernontwerp rust op vier commitments:

2.1 1:1:1 Taakroutering-alignement

In plaats van een monolithische LLM of een generieke handler, hanteert AXIOM een 1:1:1 invariant:

Trigger: Een probleem-vorm regex die exact één taak selecteert.
Prompt: Een schema-specifieke prompt met few-shot voorbeelden die zijn afgestemd op die specifieke vorm.
Handler: Een deterministische CAS-handler die alleen dat specifieke schema consumeert.

Dit alignement zorgt ervoor dat het toevoegen van een nieuwe taak ( $T_{N+1}$ ) bestaande taken ( $T_1 \dots T_N$ ) niet kan regresseren, omdat hun codepaden disjunct zijn. Dit voorkomt de competitie om het "representatieve budget" die men bij monolithische modellen ziet.

2.2 Abstain als een First-Class Output

Het systeem behandelt answer=null als een structurele, geldige output in plaats van een fout. Drie onafhankelijke kanalen kunnen een 'abstain' (onthouding) triggeren:

Router Miss: Geen regex-trigger komt overeen met de input.
Translator Abstain: De LLM geeft expliciet unknown terug (aangeleerd via few-shot voorbeelden) wanneer het de input niet kan herschrijven naar het schema zonder te gokken.
Handler Abstain: De CAS-pipeline kan geen geverifieerd antwoord afleiden (bijv. door het tegenkomen van een onbekende predicaat of een ConditionSet).

Cruciaal is dat het systeem een whitelist guard afdwingt: als een handler een onbekende predicaat tegenkomt, moet deze een 'abstain' uitvoeren in plaats van te vervallen in een waarde (bijv. nul), wat "zelfverzekerd-foutieve" outputs voorkomt.

2.3 Composed-Task Chain Framework

Voor meerstaps-problemen (bijv. stuksgewijze functies die parsing, oplossen per tak en aggregatie vereisen) gebruikt AXIOM een ComposedTask framework. Dit koppelt deterministische operatoren (pure functies) waarbij de LLM alleen aan het begin wordt aangeroepen (InitialExtractor). De keten valideert afhankelijkheden tijdens registratie, waardoor wordt gegarandeerd dat een fout in een stap resulteert in een schone 'abstain' in plaats van een stille fout.

2.4 Rule-Only Path

Voor gesloten vorm basale aritmetiek (cijfers en operatoren zonder proza), wordt de LLM-stap volledig overgeslagen. Het systeem routeert direct naar een deterministische CAS-evaluator. Dit pad garandeert bit-equivalentie tussen runs en nul inferentiekosten.

3. Belangrijkste Bijdragen

Het artikel benadrukt de forward dynamic van de architectuur in plaats van een statische nauwkeurigheidscijfer. De primaire bijdragen zijn:

Architecturaal Framework: Een 1:1:1 routeringssysteem met een rule-only bypass en een composed-task chain voor meerstapslogica.
Operationele Discipline: Een reeks principes voor betrouwbare neuro-symbolische systemen, waaronder:
- Math-template bucketing: Routering op basis van solver-structuur, niet op basis van oppervlakkige formulering.
- LOST_CORRECT scan: Een pre-commit regressie-orakel dat gearchiveerde benchmarks herhaalt om te waarborgen dat nieuwe taken bestaande prestaties niet ondermijnen.
- Predicate-not-recognized = Abstain: Een structurele verdediging tegen zelfverzekerd-foutieve outputs.
- Parseable-first onboarding: Optimaliseren voor de snelheid van parseerbare inputs voordat men optimaliseert voor vertrouwen in nieuwe domeinen.
Lineair-Additieve Returns: In tegen tegenstelling tot monolithische LLM's die logaritmische returns vertonen (afnemende winsten in nauwkeurigheid), groeit de dekking van AXIOM lineair met het aantal geregistreerde taken, aangezien taken elkaar niet onderdrukken.

4. Empirische Resultaten

De architectuur werd geëvalueerd op de MATH benchmark (4 categorieën), de lm-eval-harness arithmetic suite, en een publieke productie-implementatie (~30.000 queries).

MATH Benchmark (4 Categorieën):
- Cumulatieve Correctheid: 94,36% (2.592/2.747).
- Trust on Parseable: 100,00% over alle vier de domeinen (Algebra, Getaltheorie, Telling & Kansrekening, Precalculus). Er waren nul zelfverzekerd-foutieve antwoorden.
- Latency: Mediaan 446 ms voor LLM-gebonden taken; 1 ms voor rule-only taken.
lm-eval-harness Arithmetic:
- Correctheid: 100,0% (20.000/20.000).
- Kosten: Nul LLM API-calls; 21,6s wall time op commodity CPU.
Productie-implementatie:
- Bediende ~30.000 queries met nul zelfverzekerd-foutieve incidenten aan de API-boundary.
- Latency Separation: ~400x verschil tussen de rule-only (1 ms) en de LLM-gebonden (446 ms) paden.
Vergelijking met Pure LLM (Qwen 2.5 7B CoT):
- AXIOM presteerde aanzienlijk beter dan de pure CoT-baseline in nauwkeurigheid op moeilijkere domeinen (bijv. +38,2 pp op Precalculus) terwijl het nul foutieve antwoorden gaf vergeleken met honderden voor de CoT-baseline.
- AXIOM was ~24x tot ~40x sneller op gemiddelde door smalle prompting en het ontbreken van iteratieve redeneerlussen.

5. Betekenis en Claims

Het artikel claimt dat AXIOM een runtime trust guarantee biedt die onbeschikbaar is voor monolithische LLM's of vooraf geformaliseerde bewijzers. De betekenis ligt niet in het behalen van een specifiek nauwkeurigheidscijfer, maar in de forward dynamic die het mogelijk maakt:

Monotone Verbetering: Elke gelogde 'abstain' in productie is een kandidaat voor een correct antwoord in de volgende ship cycle. Het systeem is ontworpen om 'abstains' om te zetten in correcte antwoorden via gerichte taakcreatie zonder de bestaande prestaties te regresseren.
Verifieerbaarheid: Vertrouwen is een architecturale eigenschap afgeleid van het verificatiepad (deterministische CAS), niet een eigenschap van het onderliggende model.
Schaalbaarheid: De architectuur ondersteunt de incrementele toevoeging van duizenden taak-triples (3.100+ verscheept) met nul lost_correct regressies over 250+ commits.

De auteurs erkennen beperkingen, waaronder een plafond voor visueel gebonden geometrie-problemen (door gebrek aan visuele integratie) en NLP-irreducibele woordproblemen, maar kaderen dit als de volgende cruciale kantelpunten voor het register in plaats van asymptotische muren. De kernbijdrage is het framework dat toestaat dat "de abstain van vandaag" de "correcte van morgen" wordt via een gedisciplineerd, verifieerbaar engineeringproces.

AXIOM: A Trust-First Neuro-Symbolic Execution Architecture for Verifiable Mathematical Reasoning