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

# A Trust-First Neuro-Symbolic Execution Architecture for Verifiable Mathematical Reasoning
Source: [https://arxiv.org/html/2606.00671](https://arxiv.org/html/2606.00671)
###### Abstract

We presentAXIOM, a trust\-first neuro\-symbolic execution architecture for natural\-language mathematical reasoning\. InAXIOM, the language model functions strictly as a*canonicalizer*: it rewrites informal problem text into a narrow schema consumed by a deterministic Computer\-Algebra\-System \(CAS\) pipeline, which derives and verifies the answer or abstains as a first\-class output\. Routing follows a1:1:11\{:\}1\{:\}1alignment between problem\-shape regex, schema\-specific prompt, and closed\-form CAS handler, with3,1003\{,\}100\+ such routes shipped and zerolost\_correctregressions across250\+250\+consecutive ship commits\.

We report empirical results on44MATH categories with a cumulative correctness of94\.36%94\.36\\%\(2,592/2,7472\{,\}592/2\{,\}747\) at100\.00%100\.00\\%trust on parseable \(zero confident\-wrong answers across the full2,7472\{,\}747\-record benchmark\), all four domains above the per\-domain70/90/7070/90/70floor with per\-domain trust at100\.0%100\.0\\%, and median latency of1​ms1\\,\\text\{ms\}on rule\-only handlers \(88%88\\%of records on the lm\-eval arithmetic20,00020\{,\}000\-record benchmark\)\. The architecture has served∼\\sim30,00030\{,\}000production queries through a public deployment\.

The contribution we emphasize is not a final accuracy figure but the*forward dynamic*the architecture establishes: every logged abstain in production is a candidate correct after one ship cycle, since new tasks compose without regressing the registry\. The operational discipline behind this property — math\-template bucketing,lost\_correctscan as regression oracle, parseable\-first onboarding, and abstain as first\-class output — constitutes a transferable framework for trustworthy neuro\-symbolic systems beyond mathematics\.

## 1 Introduction

#### The unverifiable\-LLMmath problem\.

Frontier large language models achieve impressive accuracy on mathematical reasoning benchmarks, but they expose no verification pathway: at theAPIlevel, a confident\-wrong answer is indistinguishable from a confident\-right one\. The user has no structural recourse to know whether a given output is reliable\. This is not a defect of any particular model — it is a structural property of theprompt\-in\-text\-outinterface itself\.

Two existing alternatives partially address verification but at the cost of severely restricting input scope\. Lean\-based provers withLLMcopilots\[[11](https://arxiv.org/html/2606.00671#bib.bib5),[1](https://arxiv.org/html/2606.00671#bib.bib6)\]verify each tactic against the Lean kernel but require the problem to be pre\-formalized in Lean syntax — the formalization is itself the bottleneck for natural\-language queries\. Closed expert systems such as Wolfram Alpha\[[12](https://arxiv.org/html/2606.00671#bib.bib12)\]answerNLinput with rich symbolic backends, but their derivation traces are not inspectable and the system is notLLM\-augmented at the input boundary\.

#### Trust\-first vs accuracy\-first\.

We define*trust*as1−wrong/attempted1\-\\text\{wrong\}/\\text\{attempted\}, where*wrong*excludes records on which the system explicitly returnedunknown\. Trust is distinct from*accuracy*\(correct/total\\text\{correct\}/\\text\{total\}\): a system that refuses unsafe questions can have very high trust even at modest accuracy\. Our position is that*confident\-wrong is the worst failure mode*in mathematical reasoning, and an architecture should be designed to make confident\-wrong structurally rare, not to be punished*post hoc*by benchmarks\.

#### Bottom\-up architectural commitment\.

AXIOMcommits to four design choices that follow from the trust\-first stance: \(a\) the language model serves as a*canonicalizer*that rewritesNLinput into a narrow task\-specific schema, never as a solver; \(b\) a deterministicCASpipeline derives every emitted answer; \(c\) routing between theLLMand theCASpipeline is template\-aligned: each routed task is one⟨trigger,prompt,handler⟩\\langle\\text\{trigger\},\\text\{prompt\},\\text\{handler\}\\rangletriple co\-designed against the same math template; and \(d\)abstainis a first\-class structural output emitted by any of three independent channels \(no template match,LLMunknown, handler cannot derive\)\. The combination yields a runtime trust guarantee that is not available to either monolithicLLMsystems or pre\-formalized provers\.

#### Contributions\.

- •Architecture\([Section˜2](https://arxiv.org/html/2606.00671#S2)\): a1:1:11\{:\}1\{:\}1⟨trigger,prompt,handler⟩\\langle\\text\{trigger\},\\text\{prompt\},\\text\{handler\}\\ranglerouting architecture, an operator\-pipeline chain framework for multi\-step shapes, and arule\_onlyLLM\-bypass for closed\-form bare arithmetic\. We ship3,1003\{,\}100\+ task triples and55chain tasks at the time of writing\.
- •Empirical evaluation\([Section˜3](https://arxiv.org/html/2606.00671#S3)\):94\.36%94\.36\\%cumulative correctness \(2,592/2,7472\{,\}592/2\{,\}747\) at100\.00%100\.00\\%trust on parseable \(zero confident\-wrong answers across the full benchmark\), with all44MATHcategories \(Algebra, Number Theory, Counting & Probability, Precalculus\) above the70/90/7070/90/70per\-domain floor and100\.0%100\.0\\%trust on parseable in each\. Therule\_onlypath achieves100%100\\%on the20,00020\{,\}000\-record lm\-eval\-harness arithmetic suite\. The architecture has served∼\\sim30,00030\{,\}000production queries through a public deployment\.
- •Operating principles\([Section˜4](https://arxiv.org/html/2606.00671#S4)\): four principles transferable beyond mathematics — math\-template bucketing,LOST\_CORRECTscan as regression oracle, predicate\-not\-recognized as mandatory abstain, and parseable\-first onboarding with regime\-dependent trust floor — each justified by direct empirical observation across250\+250\+ship cycles\.

#### Reproducibility\.

A live, publicly accessible deployment of the architecture runs at[https://huggingface\.co/spaces/Squagghy/axiom\-solver](https://huggingface.co/spaces/Squagghy/axiom-solver)\. The single\-query view \([Figure˜1](https://arxiv.org/html/2606.00671#S1.F1)\) illustrates the1:1:11\{:\}1\{:\}1alignment on every record and the structural visibility of the abstain channels; the cumulative dashboard \([Figure˜2](https://arxiv.org/html/2606.00671#S1.F2)\) exposes the production statistics referenced throughout[Section˜3](https://arxiv.org/html/2606.00671#S3)\.

![Refer to caption](https://arxiv.org/html/2606.00671v1/figs/demo_trace.png)Figure 1:Single\-query trace from the production demo onCompute the value ofx2\+y2x^\{2\}\+y^\{2\}wherex=3x=3andy=5y=5\. The four exposed stages \(Router / Translator / Handler / Answer\) materialize the1:1:11\{:\}1\{:\}1alignment from[Section˜2\.1](https://arxiv.org/html/2606.00671#S2.SS1): Router and Handler reference the same*Numeric expression evaluation*template, and the Translator block surfaces the verbatimLLMcanonical rewrite \(Compute 3\*\*2 \+ 5\*\*2\) with an explicit hallucination caveat\. The final answer reports the per\-query cost \(1,7551\{,\}755tokens≈\\approx$​0\.00035\\mathdollar 0\.00035at Together\.ai $0\.18/M;[Section˜3\.5](https://arxiv.org/html/2606.00671#S3.SS5)\)\. Any of the three abstain channels \(router miss,LLMunknown, handler abstain\) becomes visible at the stage that emitted it\.![Refer to caption](https://arxiv.org/html/2606.00671v1/figs/demo_dashboard.png)Figure 2:Cumulative dashboard from the production deployment\. Top row: hero counters \(Total queries, Answered, Abstained, Answer rate\)\. Middle row: structural correctness signals \(Routed rate∼97%\\sim 97\\%; p95 latency∼865\\sim 865\\,ms dominated byLLM\-bound traffic\)\. Bottom row: efficiency aggregates confirming the per\-query footprint of[Section˜3\.5](https://arxiv.org/html/2606.00671#S3.SS5)\(LLM\-bound queries, average tokens / query, total tokens, inference cost estimated as tokens×\\timesTogether\.ai $0\.18/M\)\. The live activity log \(below\) anchors the dashboard to real, free\-form user traffic — each entry is one query, with per\-record latency and routed task\.

## 2 Architecture

The architecture realizes the trust\-first stance from[Section˜1](https://arxiv.org/html/2606.00671#S1)as a deterministic execution path: a problem\-shape regex selects exactly one task, the language model rewrites the input into that task’s narrow schema, and a closed\-formCAShandler derives and verifies the answer or abstains through a structured fail\-reason\. The four design choices we enumerate below —1:1:11\{:\}1\{:\}1task routing alignment \([Section˜2\.1](https://arxiv.org/html/2606.00671#S2.SS1)\), abstain as a first\-class output \([Section˜2\.2](https://arxiv.org/html/2606.00671#S2.SS2)\), the composed\-task chain framework for multi\-step shapes \([Section˜2\.3](https://arxiv.org/html/2606.00671#S2.SS3)\), and therule\_onlypath that bypasses theLLMentirely on math\-template\-pure shapes \([Section˜2\.4](https://arxiv.org/html/2606.00671#S2.SS4)\) — are each motivated by a specific failure mode of theprompt\-in\-text\-outinterface\.[Figure˜3](https://arxiv.org/html/2606.00671#S2.F3)summarizes the execution path of a single query\.

Problem text\(natural language\)Router\(regex,O​\(1\)O\(1\)\)LLM rewriter\(canonicalizer\)Handler\(CAS, deterministic\)Answerorunknowntaskschemarule\_only=True

Figure 3:AXIOMpipeline\. The router selects exactly one task per query \(regex match on problem\-shape,O​\(1\)O\(1\)\)\. The LLM rewrites the input into a task\-specific schema; the handler deterministically derives and verifies the answer via SymPy\. Therule\_only=Truepath bypasses the LLM for math\-template\-pure shapes \(e\.g\. bare arithmetic;88%88\\%of lm\-eval arithmetic records\)\.### 2\.11:1:11\{:\}1\{:\}1task routing alignment

Routing inAXIOMdeparts from the two prevailing patterns inLLM\-augmented mathematical reasoning: “one model emits the answer end\-to\-end” \(frontier monolithic systems\) and “theLLMrewrites into a single structured form, then a genericCAShandler consumes it” \(early hybrid systems\)\. Instead, every problem shape we cover is carved out as a*triple*of \(a\) a regex trigger, \(b\) a prompt whose few\-shot examples teach a schema specific to that shape, and \(c\) a deterministic handler that consumes only that schema\. The three components are co\-designed so the trigger fires precisely on shapes whose canonical the prompt can produce and whose answer the handler can verify\. We call this the*1:1:11\{:\}1\{:\}1alignment invariant*: one trigger, one prompt, one handler\.

The invariant is load\-bearing in two senses\. First,*trust attribution becomes local*: a record routed to taskTTthat produces an answer is verifiable strictly throughTT’s code path; no emergent behaviour spans tasks\. Second,*registry growth is linearly additive*: adding taskTN\+1T\_\{N\+1\}cannot regress tasksT1\.\.NT\_\{1\.\.N\}because their code paths are disjoint by construction \(non\-overlapping triggers, isolated handlers\)\. Across theN=1,600N=1\{,\}600\+ task triples shipped at the time of writing,lost\_correctregressions cumulated to0over250\+250\+consecutive ship commits\. A pre\-commit migration scan against archived benchJSONfiles acts as the regression oracle: any trigger widening or new task that would steal a previously\-correct record and produce a worse outcome is caught before commit \(see[Section˜4](https://arxiv.org/html/2606.00671#S4), Principle \#17\)\.

This stands in deliberate contrast with monolithicLLM\-as\-solver systems, in which each new capability shares representational budget with all existing ones, and adding capabilityN\+1N\+1implicitly competes against1\.\.N1\.\.Nfor prompt space, attention, and retrieval relevance\.

### 2\.2 Abstain as first\-class output

A response withanswer=nullis structurally distinct inAXIOMfrom a response withanswer=value\. Three independent channels feed the same null:

1. 1\.Router miss: no task’s regex trigger matched the problem text\. The system has no template\-aligned interpretation\. Logged asfail\_reason=no\_task\.
2. 2\.Translator abstain: theLLMreturnedunknownvia a dedicated few\-shot example in the task’s prompt\. The prompt teaches the model to recognize when its rewrite would be a guess\.
3. 3\.Handler abstain: theLLMproduced a canonical and the regex matched, but the deterministicCASpipeline could not derive a verified answer \(e\.g\.,sp\.solvereturned aConditionSet, a predicate value was unrecognized, multiple solution branches required disambiguation\)\.

[Figure˜4](https://arxiv.org/html/2606.00671#S2.F4)visualizes the four exits\. Each channel is a structured, telemetry\-visible signal, not a thrown exception or a confident\-wrong fallback\. As the trace traverses the public\-API boundary, we strip internal task names and fail reasons but preserve the per\-stage outcome \(router*matched*, translator*abstained*, handler*skipped*\), so the demoUIcan render which subsystem declined to answer\.

Router\(regex\)LLM rewriterHandler\(CAS\)Answerabstained:falseno\_task\(router miss\)rewrite\_abstain\(LLMunknown\)handler\_abstain\(can’t derive\)\{answer: null, abstained: true, fail\_reason: <which\_stage\>\}matchedcanonicalverifiedFigure 4:Abstain as a first\-class structured output\. Three pipeline stages each have an independent abstain channel \(dashed, red\); when any fires, the public\-APIresponse carries a structuredfail\_reasonnaming the stage\. The committed\-answer path \(top, green\) is taken only when all three stages succeed\. This four\-exit structure is the architectural foundation ofAXIOM’s trust property: confident\-wrong is emitted only if the handler verifies a wrong canonical, never as a silent fall\-through\.The discipline behind this design is illustrated by a real bug encountered in the30 00030\\,000\-query production deployment\. A probability handler computedP​\(rolling\>4\)P\(\\text\{rolling\}\>4\)on a fair die\. TheLLMcorrectly producedpredicate=greater\_than\_4, but the handler’s predicate dispatcher had no branch for thegreater\_than\_\*family and silently fell through to a default count of0matching outcomes, emitting the confident\-wrong answer “0” \(expected1/31/3\)\. The architectural fix was a whitelist guard: enumerate the predicate types the handler recognizes and, on any unknown predicate, returnNone\(handler abstain\) rather than proceed with a default that resembles a valid count\. This pattern is the structural defense against the worst failure mode the architecture can produce:*predicate\-not\-recognized must be abstain, never default\-zero*\. We discuss the generalization in[Section˜4](https://arxiv.org/html/2606.00671#S4)as Principle \#22\.

### 2\.3 Composed\-task chain framework

Some shapes require multi\-step deterministic computation after theLLMhas extracted structure\. An archetypal example is a piecewise functionff, evaluated wheref​\(x\)=cf\(x\)=cacross multiple branches, then aggregated \(e\.g\.,*sum of all solutions*\)\. This factorizes naturally into three deterministic steps —ParsePiecewise,SolvePerBranch, andAggregateRealSolutions— but the atomic1:1:11\{:\}1\{:\}1pattern cannot represent it without inlining solver and aggregator into one monolithic handler\.

We extend the framework withComposedTask: theLLM’s structured canonical is consumed by anOperatorpipeline\. EachOperatoris a pure functionctx↦ctx\\text\{ctx\}\\mapsto\\text\{ctx\}with declaredrequiresandproducestype sets\. Validation at registration time enforces that each operator’s required keys are produced by some upstream operator, catching missing dependencies at definition time rather than at runtime\. Operators chain deterministically; failure at any step aborts and returns a clean abstain\. Crucially, theLLMcall remains exactly once per record \(the first “InitialExtractor” operator\) — we do not iterate the model in the chain\.

FiveComposedTasks ship in production, covering the piecewise solve\+aggregate above and four*Number Theory*multi\-step shapes \(count\-then\-mod, base\-from\-equation, modular two\-variable evaluation, three\-constraint Chinese Remainder search\)\. The pattern preserves both architectural invariants \(1:1:11\{:\}1\{:\}1at the operator level, abstain first\-class on each operator\) and empirically delivers100%100\\%trust on parseable on its target records, identical to atomic tasks\.

### 2\.4 Rule\-only architectural special case

When a task’s math template is closed\-form bare arithmetic — digits, operators, parentheses, with no prose disambiguation — theLLMcanonicalization step is structurally redundant: the handler can parse the raw problem text directly and emit an answer through deterministicCASevaluation\. We expose this via atask\.rule\_only=Trueflag that bypasses theLLMcall entirely \(dashed path in[Figure˜3](https://arxiv.org/html/2606.00671#S2.F3)\)\.

Empirically, the rule\-only path on the lm\-eval\-harness arithmetic benchmark\[[4](https://arxiv.org/html/2606.00671#bib.bib4)\]\(20 00020\\,000records across ten sub\-tasks: 1\-digit chain, 2\-digit add/multiply/subtract, 3\-digit add/sub, 4\-digit add/sub, 5\-digit add/sub\) achieves100\.0%100\.0\\%correct in21\.621\.6s wall time on commodityCPU, with zeroLLMAPIcalls and zero cost\. Output bit\-equivalence across runs is guaranteed by construction — no sampling, no stochasticity, no thread scheduling effects on the answer surface\.

Rule\-only is the asymptotic limit of1:1:11\{:\}1\{:\}1alignment, not a separate pattern: when trigger and handler are sufficient on raw text, the prompt becomes vestigial\. Most production tasks remainLLM\-bound \(the77BInstruct model handles routing context for prose\-rich shapes\), but the rule\-only flag is the architectural lever for closed\-form domains and the structural delivery vehicle for the strongest correctness claim the architecture can make\.

## 3 Empirical Evaluation

We evaluateAXIOMon three complementary axes: \(a\) standardMATHbenchmarks across44categories, evaluating the full⟨router,LLM,handler⟩\\langle\\text\{router\},\\text\{LLM\},\\text\{handler\}\\ranglepipeline; \(b\) the lm\-eval\-harness arithmetic suite, which exercises therule\_onlyLLM\-bypass path; and \(c\) the public production deployment, which captures the full distribution of queries served to date through the live demo\.

TheLLMused in all configurations is Qwen 2\.5 7B Instruct\[[10](https://arxiv.org/html/2606.00671#bib.bib9)\]\. No fine\-tuning is performed; all results below use the same model with task\-specific prompts at inference time\.

### 3\.1 Per\-domainMATHcoverage

[Table˜1](https://arxiv.org/html/2606.00671#S3.T1)reports per\-domain results on theMATHtest split for the four categories at the70/90/7070/90/70floor \(parseable rate≥70%\\geq 70\\%, trust on parseable≥90%\\geq 90\\%, total correct≥70%\\geq 70\\%\)\. All four domains crossed the floor under the same architecture \(no domain\-specific model or training step\); only the registry of task triples differs by domain\.

Table 1:AXIOMper\-domain results on MATH benchmark \(Hendrycks et al\., 2021\)\. Trust on parseable at100\.0%100\.0\\%across all four domains \(zero confident\-wrong answers\); per\-domain70/90/7070/90/70floor reached and substantially exceeded \(parseable≥70%\\geq 70\\%, trust on parseable≥90%\\geq 90\\%, total correct≥70%\\geq 70\\%\)\. Parseable and Correct are identical by construction: every parseable record is correct\. Latency is reported as*mean / median*on theLLM\-bound inference path; therule\_onlybypass \([Section˜2\.4](https://arxiv.org/html/2606.00671#S2.SS4)\) does not apply to theseMATHcategories\. Latencies measured on production deployment via Together\.ai\-hosted Qwen 2\.5 7B Instruct \([Section˜3\.3](https://arxiv.org/html/2606.00671#S3.SS3)\)\.
### 3\.2 lm\-eval arithmetic: structural correctness

The lm\-eval\-harness arithmetic suite\[[4](https://arxiv.org/html/2606.00671#bib.bib4)\]comprises20,00020\{,\}000records across ten sub\-tasks \(1\-digit chain, 2\-digit add/multiply/subtract, 3\-digit add/sub, 4\-digit add/sub, 5\-digit add/sub\) testing bare arithmetic inQ: What is X plus Y?\\nA:format\. Therule\_onlytaskarithmetic\_natural\_evalmatches this shape via regex on the raw input and dispatches a directsympifyevaluation, bypassing theLLMentirely\.

Result:20,00020\{,\}000/20,00020\{,\}000correct\(100\.0%100\.0\\%\),21\.621\.6s wall time on commodityCPU,0LLMAPIcalls,0inference cost\. Output bit\-equivalence across runs is guaranteed by construction since the path is deterministic and stochasticity\-free at the model level\.

While bare arithmetic is structurally trivial, this result demonstrates the strongest correctness claim our architecture can make: when math\-template purity holds, the system delivers100%100\\%provably correct output at sub\-millisecond per\-record latency\. This is the asymptotic limit of the1:1:11\{:\}1\{:\}1alignment \([Section˜2\.4](https://arxiv.org/html/2606.00671#S2.SS4)\); most production tasks remainLLM\-bound, but the limit is achievable for the right problem class and provides a verification benchmark against which the architecture’s full\-pipeline behaviour can be sanity\-checked\.

### 3\.3 Real\-world production distribution

The architecture has served30k\+queries through a public deployment \(FastAPIon Railway with Together\.ai\-hostedLLM, frontend on Hugging Face Spaces\)\. Traffic spans theMATHtest split for the four covered categories, theMATHtraining split for the same categories \(used as out\-of\-bench\-distribution material because the architecture has no parametric memory and the train split is therefore diagnostically equivalent to test\), the lm\-eval\-harness arithmetic suite \(all routed through therule\_onlybypass,[Section˜2\.4](https://arxiv.org/html/2606.00671#S2.SS4)\), and free\-form user\-typed queries covering shapes well beyond the fourMATHcategories\.

#### Latency by inference path\.

Per\-record latency segregates cleanly by routing decision\.rule\_onlyrecords \(lm\-eval arithmetic and a small set of closed\-form bare\-input shapes\) report median11\\,ms / p9511\\,ms — effectively pureCASevaluation cost\.LLM\-bound records report median446446\\,ms / p951,1161\{,\}116\\,ms — dominated by the Together\.ai inference round\-trip\. Router\-miss records \(no\_task, fast\-fail before anyLLMcall\) report median2525\\,ms / p95155155\\,ms\. Across the full production sample, the architectural latency separation is∼\\sim400×400\\timesbetween rule\-only andLLM\-bound, which is the structural origin of the cost\-per\-correct\-answer advantage discussed in[Section˜3\.4](https://arxiv.org/html/2606.00671#S3.SS4)\.

#### Zero confident\-wrong incidents at the API boundary\.

The deployment serves arbitrary user\-typed mathematical queries — including out\-of\-distribution shapes \(asymptote diagrams, free\-form word problems\) that exceed the fourMATHcategories evaluated in[Section˜3\.1](https://arxiv.org/html/2606.00671#S3.SS1)\. The architectural guarantee —answer=null,abstained=truewith a structured fail\-reason at theAPIboundary — held across 30k\+ recorded queries: no free\-form output that a user might mistake for a verified answer was emitted\. The handler\-exception class is itself bounded \(<0\.1%<\\\!0\.1\\%of traffic\); the dispatcher catches every uncaught exception and converts to abstain, preserving the trust\-binary surface even when individual handlers fail\.

#### No\-task pool as architectural discovery channel\.

Records on which the router emitted no match are the discovery channel for new task design: each recurring shape is a candidate sprint\. Heuristic taxonomy of theno\_taskpool yields three buckets\.*Vision\-locked*shapes \(Asymptote diagrams, geometric figures\) account for the dominant cluster, blocked until vision integration\.*Narrow\-task\-recoverable*shapes \(matrix operations, advanced function inverse, infinite series, modular widening, log identities\) account for a smaller tier and are direct candidate sprints under the forward dynamic of[Section˜6](https://arxiv.org/html/2606.00671#S6)\. The remaining residual is the long tail of one\-of\-a\-kind shapes that we expect to drain incrementally across many sprint cycles rather than via single targeted ships\.

#### Live registry expansion during manuscript preparation\.

The forward\-dynamic claim is*exercised*, not asserted, in this work\. Within the manuscript\-preparation window, three consecutive sprint cycles ran the full operational pipeline:

production→abstain telemetry→cluster analysis\\displaystyle\\;\\rightarrow\\;\\textsc\{abstain telemetry\}\\;\\rightarrow\\;\\textsc\{cluster analysis\}→narrow\-task creation→regression\-oracle scan→immediate deploy\\displaystyle\\;\\rightarrow\\;\\textsc\{narrow\-task creation\}\\;\\rightarrow\\;\\textsc\{regression\-oracle scan\}\\;\\rightarrow\\;\\textsc\{immediate deploy\}
- •Sprint 1 \(matrix arithmetic\)\.Explicit matrixdet\\det/tr\\mathrm\{tr\}/ inverse / transpose / integer power on2×22\{\\times\}2–4×44\{\\times\}4matrices\. Captured∼\\sim1111records from the matrix sub\-cluster, including the trophy\[3−41−1\]2016\\bigl\[\\begin\{smallmatrix\}3&\-4\\\\ 1&\-1\\end\{smallmatrix\}\\bigr\]^\{2016\}resolved in<500<\\\!500ms via Cayley–Hamilton inSymPy\.
- •Sprint 2 \(piecewise inverse sum\)\.For a piecewise\-definedffwith numeric branches, compute∑if−1​\(vi\)\\sum\_\{i\}f^\{\-1\}\(v\_\{i\}\)on an explicit list of values\. Captured 4 records from the function\-inverse sub\-cluster \(all 4 trophy cases verified*in production*via the/api/solveendpoint\)\.
- •Sprint 3 \(piecewise self\-inverse parameters\)\.Given a22\-branch piecewiseffwith one parameterised linear branch and the involution propertyf​\(f​\(x\)\)=xf\(f\(x\)\)=x, compute a target expression in the parameters\. Captured22records, deferred a third \(thek​\(x\)k\(x\)functional\-output sub\-shape\) via the prompt’sunknownchannel\.

Cumulatively, three narrow task triples were shipped during manuscript preparation, capturing∼17\\sim 17records from the abstain pool to the answered class with0lost\_correctacross all three commits and100%100\\%trust on parseable on the captured records\. The registry*scales operationally through isolated task expansion validated by regression\-oracle deployment cycles*\([Section˜4\.1](https://arxiv.org/html/2606.00671#S4.SS1), Principle 2\)\. This is the routine architectural cadence under which the system has shipped1,6001\{,\}600\+ task triples across250\+250\+commits with the same zero\-regression discipline; the manuscript\-window expansion demonstrates that the cadence applies to the production\-derived abstain pool with no methodological adjustment\.

### 3\.4 Comparison with pure\-LLMchain\-of\-thought

To characteriseAXIOMrelative to a pure\-LLMinference baseline, we run the*same frozen*model used internally \(Qwen 2\.5 7B Instruct, loaded via Hugging Face transformers on aT4GPU\) in chain\-of\-thought mode — no router, noCASverification, no abstain mechanism — on the fourMATHcategories whereAXIOMreaches the per\-domain70/90/7070/90/70floor\. The model weights, the hardware, the dataset, and the grader \(answers\_matchfrom[Section˜3\.1](https://arxiv.org/html/2606.00671#S3.SS1)\) are identical across both arms; the only varying factor is the inference architecture\. We frame the comparison as two architectural philosophies operating on the same underlying model rather than as a head\-to\-head contest — the two systems optimise different objectives and occupy different points on the trust/latency/accuracy tradeoff curve\.

TheLLMis queried with a standard CoT system prompt \(*“solve step by step, end with*\\boxed\{X\}*”*\) at temperature0\(greedy decoding\), with up to10241024new tokens per response\. Answer extraction uses a regex prioritising\\boxed\{\.\.\.\}and falling back to “the answer isXX” patterns\.

Table 2:Per\-category comparison on theMATHtest split\. Same Qwen 2\.5 7B Instruct model, same T4GPU, sameanswers\_matchgrader\.*Wrong*counts records on which the system emitted an answer that was incorrect \(no abstain trace at theAPIboundary\)\. Latency is reported as*mean / median*on theLLM\-bound inference path for both systems;AXIOMalso exposes a closed\-formrule\_onlybypass discussed separately\.#### Two architectural philosophies, not a contest\.

On Algebra — theMATHcategory most densely represented in the model’s pretraining corpus —AXIOMexceeds Qwen 7B CoT accuracy by11\.511\.5percentage points while emitting0wrong answers vs159159\. We do not interpret this as a contest the two systems are playing: theLLMcommits to an answer on every record by construction \(no abstain mechanism in the pure\-CoT setup\), whileAXIOMis selective about commitment by design and emits an answer only when its 1:1:1 template alignment can verify it\. The relevant comparison is therefore not “which system is more accurate” but “what does each system give up, and what does each gain in return”\.

#### What the numbers say\.

On the same Algebra split:

- •Qwen commits on96\.5%96\.5\\%of records \(1146/11871146/1187\) and is correct on86\.6%86\.6\\%overall; that is, of the159159records on which it is wrong, all159159are committed outputs, indistinguishable at theAPIboundary from the10281028correct ones\.
- •AXIOMcommits on98\.15%98\.15\\%of records and is correct on98\.15%98\.15\\%overall; the trust on the committed subset is100\.00%100\.00\\%, and the system emits0wrong outputs along with2222records explicitly tagged with a structured fail\-reason \(no\_task,rewrite\_abstain,handler\_abstain\)\.
- •Trust on committed records:86\.6%86\.6\\%\(Qwen\) and100\.00%100\.00\\%\(AXIOM\)\. We attribute the gap not to a difference in per\-record reasoning quality but to an architectural property of the inference path: pure chain\-of\-thought has no abstain mechanism — the model produces a committed output on every record by construction, regardless of its own uncertainty\.AXIOMexposes three structured abstain channels \(router miss,LLMunknown, handler abstain — see[Section˜2\.2](https://arxiv.org/html/2606.00671#S2.SS2)\) and exercises them on the2222records it cannot verify, yielding the complete elimination of confident\-wrong incidents \(159159vs0on Algebra\)\. Trust here is therefore an architectural property, not a property of the underlying model\.
- •On theLLM\-bound inference path,AXIOMruns∼24×\\sim 24\\timesfaster on the mean \(590590ms vs14\.014\.0s\) and∼31×\\sim 31\\timesfaster on the median \(446446ms vs14\.014\.0s\) on the same hardware\. The closed\-formrule\_onlybypass \(lm\-eval arithmetic,∼1\\sim 1ms; not exercised on Algebra\) is a separate architectural feature for problem shapes that do not require anLLMat all\.
- •Reproducibility: Qwen’s CoT output is subject tobf16non\-determinism even at temperature0;AXIOMrule\-only output is bit\-identical across runs by construction\.AXIOMalso exposes a per\-stage \(router, translator, handler\) trace that lets downstream consumers attribute every output, abstain, or wrong answer to a specific subsystem \([Section˜3\.3](https://arxiv.org/html/2606.00671#S3.SS3)\)\.

#### Convexity ofAXIOM’s advantage on harder domains\.

Qwen 7B CoT operates at one end of this curve: full commitment by construction, no abstain channel, latency dominated by theLLMinference cost\.AXIOMoperates at another end: selective commitment via template\-aligned routing, structured abstain on the unverified residual, and substantially lower latency on identical hardware \(∼24×\\sim 24\\timesto∼40×\\sim 40\\timeson the mean across the four measured categories, depending on domain\)\.

The raw\-accuracy ordering between the two systems is nowAXIOM\-dominant across everyMATHcategory we measure\. On AlgebraAXIOMleads by\+11\.5\+11\.5pp \(98\.15%98\.15\\%vs86\.6%86\.6\\%\); on Number Theory by\+22\.1\+22\.1pp \(95\.37%95\.37\\%vs73\.3%73\.3\\%\); on Counting & Probability by\+24\.6\+24\.6pp \(91\.35%91\.35\\%vs66\.7%66\.7\\%\); on Precalculus by\+38\.2\+38\.2pp \(87\.73%87\.73\\%vs49\.5%49\.5\\%\)\. The lead is monotone in the inverse of how densely each domain is represented in the model’s pretraining corpus: the thinner Qwen’s coverage of a domain, the larger the gap\. The total swing is∼27\\sim 27pp across the four categories\.

The within\-Qwen variance across these four categories is itself diagnostic\. The same model achieves86\.6%86\.6\\%on Algebra and49\.5%49\.5\\%on Precalculus — a3737pp gap on supposedly comparable mathematical reasoning\. The per\-level decomposition is even more striking: Qwen’s L5 accuracy is75\.2%75\.2\\%on Algebra,54\.5%54\.5\\%on Number Theory,45\.5%45\.5\\%on Counting & Probability, and20\.0%20\.0\\%on Precalculus\. We do not have access to Qwen’s training corpus, but the magnitude of this variance is consistent with differential training\-data exposure acrossMATHsubcategories rather than uniform reasoning quality\. The implication for our positioning is interpretive: any single\-category reading is limited as a reference, and the four\-category spread maps each architecture’s contribution across the difficulty axis more completely than any individual point\. The\+20\.8\+20\.8ppAXIOMadvantage on Precalculus complements the Algebra reading by showing how each architecture behaves where pretraining coverage is thinner\.

The*confident\-wrong reduction*is now structural\.AXIOMemits0confident\-wrong answers in every category measured:0vs159159on Algebra,0vs144144on Number Theory,0vs158158on Counting & Probability,0vs276276on Precalculus\. The multiplier is unbounded in every direction\. On records where Qwen does not know how to commit, the lack of an abstain channel converts uncertainty into confident\-wrong outputs, whileAXIOM’s structured abstain \(router miss,LLMunknown, or handler abstain\) preserves trust by declining\. The architectural property of the inference path is the source of this property, not a property of the underlying model\.

Neither system dominates the other on every axis\. The contribution of this paper is the architectural framework underlyingAXIOM’s position on this curve and the operational discipline \([Section˜4\.1](https://arxiv.org/html/2606.00671#S4.SS1)\) that allows it to expand monotonically over time \([Section˜3\.3](https://arxiv.org/html/2606.00671#S3.SS3)\)\.

### 3\.5 Token efficiency through task\-localized prompting

The latency advantage observed in[Section˜3\.4](https://arxiv.org/html/2606.00671#S3.SS4)\(∼24×\\sim 24\\timesto∼40×\\sim 40\\timeson the mean across the fourMATHcategories\) is the surface manifestation of a deeper architectural property: per\-query theLLMsees ONLY the prompt of the routed task, not a universal "math reasoning" prompt that has to anticipate every possible problem shape\. The router performs the shape\-identification step*before*anyLLMcall, so the rewriter receives a narrow context:3−53\{\-\}5shape\-specific few\-shot examples plus the problem text\.

The empirical token footprint perLLM\-bound query, measured on the production deployment via the Together\.ai usage\-reporting field:

- •Median input tokens:∼250\\sim 250\(system prompt \+3−53\{\-\}5task\-specific few\-shot examples \+ problem text\)\.
- •Median output tokens:∼30−50\\sim 30\{\-\}50\(compact canonical form: a single line, no chain\-of\-thought\)\.
- •Total per query:∼280−300\\sim 280\{\-\}300tokens\.

By comparison, on the same problems:

- •Pure chain\-of\-thought \(Qwen 7B CoT, our[Section˜3\.4](https://arxiv.org/html/2606.00671#S3.SS4)baseline\) emits500−1500500\{\-\}1500tokens per query, since the model writes out its reasoning before committing to a boxed answer\.
- •Self\-consistency / N\-sampling approaches multiply the cost byNN\(typically3−103\{\-\}10\), each sample independently producing a CoT\.
- •Tool\-augmented agentic systems with multi\-step reasoning can spend5000−200005000\{\-\}20000tokens per problem, especially on compositional shapes that require several rounds of plan→\\rightarrowact→\\rightarrowobserve\.

This gap is not the result of token\-budget tuning\. It emerges from three architectural commitments that the rest of the paper has already named:

1. 1\.1:1:11\{:\}1\{:\}1alignment\([Section˜2\.1](https://arxiv.org/html/2606.00671#S2.SS1)\) means the router selects exactly one task per query — the rewriter receives ONLY that task’s prompt, not the union of all1,6001\{,\}600\+ task prompts\.
2. 2\.DeterministicCASverification\([Section˜2\.2](https://arxiv.org/html/2606.00671#S2.SS2)\) eliminates the need for additionalLLMpasses: there is no self\-consistency loop, no critic\-model debate, no retry\-with\-CoT\. The handler either derives the answer from the canonical or returns ahandler\_abstain\.
3. 3\.Abstain as first\-class output\([Section˜2\.2](https://arxiv.org/html/2606.00671#S2.SS2)\) means a low\-confidence translation is not promoted into a longer reasoning chain — it returnsrewrite\_abstainimmediately, and the system commits no token to a recovery attempt\.

At Together\.ai’s published Qwen 2\.5 7B Instruct Turbo pricing \($0\.18 per million tokens for both input and output\),AXIOMserves an averageLLM\-bound query for∼\\sim$0\.00006 \(≈6\\approx 6microcents\)\. The cumulative inference cost visible on the public\-demo dashboard tracks this in real time across all served queries — narrow prompts makeAXIOM’s per\-query footprint roughly proportional to the canonical’s information content, not to the size of the mathematical domain it is drawn from\. The latency advantage and the cost advantage are surface manifestations of the same property: routing eliminates the "universal reasoning overhead" otherwise paid on every query\.

## 4 Discussion

### 4\.1 Operating principles formalized

The architectural commitments codified in[Section˜2](https://arxiv.org/html/2606.00671#S2)emerged through more than250250ship cycles iterating on the production demo\. We extract the four operating principles most transferable beyond mathematics: any system in which a language model produces structured input for a deterministic verifier faces the same regression\-discipline, abstain\-class, bucketing, and onboarding tradeoffs\.

#### Principle 1: math\-template bucketing\.

Routing tasks must be partitioned by the math template they implement \(one solver path, one closed\-form structure\), not by surface phrasing or domain category\. Empirically, every task split by*surface*category that mixed multiple solver paths plateaued at33​–​62%33\\text\{\-\-\}62\\%trust on parseable; every task split by*template*reached80​–​100%80\\text\{\-\-\}100\\%trust on parseable in its first bench cycle\. The boundary between routes is mathematical, not lexical\.

#### Principle 2:LOST\_CORRECTscan as regression oracle\.

Routing changes — trigger widenings, new tasks, defer\-guard additions — are gated by a pre\-commit migration scan that replays an archived benchJSONthrough the proposed router and reports any record that was correct in versionN−1N\{\-\}1and would become wrong or abstain in versionNN\. Across250\+250\+consecutive ship commits, this oracle caught all regressions before commit \(cumulativelost\_correct=0\\textsc\{lost\\\_correct\}=0\)\. The discipline decouples ship velocity from bench wall\-time: a sprint can land8​–​158\\text\{\-\-\}15changes per cycle without re\-running the full bench per change, becauselost\_correct=0\\textsc\{lost\\\_correct\}=0on the relevant records is a sharper guarantee than bench\-aggregate parity\.

#### Principle 3: predicate\-not\-recognized must be abstain\.

Where a handler taxonomically classifies its input \(predicate type, mode, target enum\), every branch not matched must be an explicit abstain, never a fallthrough to a default value\. Default fallthrough is the structural source of confident\-wrong, the worst failure mode this architecture can produce \(see[Section˜2\.2](https://arxiv.org/html/2606.00671#S2.SS2)for the case study\)\. The protection is whitelist\-up\-front: enumerate the recognized cases before any computation; on no\-match, return abstain rather than proceed with a default that resembles a valid output\.

#### Principle 4: parseable\-first onboarding for new domains\.

When opening a domain that the architecture has not seen before, optimize for parseable rate first \(target≥50%\\geq 50\\%\) before optimizing for trust on parseable\. Low parseable starves the cluster\-level triage loop; defensive prompt design \(\>3\>3unknownfew\-shot teachers\) at onboarding time locks theLLMintounknown\-conservative output and yields no signal for the next sprint cycle\. The aspirational trust floor is therefore*regime\-dependent*:40​–​50%40\\text\{\-\-\}50\\%during onboarding \(parseable<30%<30\\%\),55​–​65%55\\text\{\-\-\}65\\%during maturation \(30​–​60%30\\text\{\-\-\}60\\%parseable\),70​–​80%70\\text\{\-\-\}80\\%in steady state \(parseable\>60%\>60\\%\)\. The original*North Star*80%80\\%trust floor was calibrated on a domain that had high parseable from day one; applied uniformly it forces excessive abstain on under\-parsed domains and produces fake signal on tiny denominators\.

### 4\.2 Linear\-return composition

MonolithicLLMsystems exhibit logarithmic accuracy returns: each additional point on standard benchmarks requires exponentially more training compute or curated data\.AXIOM’s narrow\-task architecture, by contrast, exhibits*linear\- additive*returns:

coverage​\(ℬ\)=∑k∈𝒯coveragek​\(ℬ\),\\text\{coverage\}\(\\mathcal\{B\}\)\\;=\\;\\sum\_\{k\\,\\in\\,\\mathcal\{T\}\}\\text\{coverage\}\_\{k\}\(\\mathcal\{B\}\),
where𝒯\\mathcal\{T\}is the registered task set,ℬ\\mathcal\{B\}a benchmark, andcoveragek​\(ℬ\)\\text\{coverage\}\_\{k\}\(\\mathcal\{B\}\)the records inℬ\\mathcal\{B\}matching taskkk’s\(trigger,schema,solver\-path\)\(\\text\{trigger\},\\text\{schema\},\\text\{solver\-path\}\)triple\. Each shipped task contributes a fixed quantity of records on every benchmark whose distribution contains its shape; the contribution is independent of other tasks \(they cannot suppress each other under the1:1:11\{:\}1\{:\}1invariant\)\.

We refer to this empirical effect as the*boomerang*: a task developed for one benchmark benefits every other benchmark that contains its shape\. A modular\-arithmetic Number\-Theory predicate handler shipped for theMATHNumber Theory category contributed records toMATHAlgebra word problems that involve modular structure, to the lm\-eval\-harness arithmetic suite \(via therule\_onlyfast path\), and toMATH\-500\. The cost is registry size —1,6001\{,\}600\+ task triples ship at the time of writing\. The benefit is debug\-locality: any wrong record traces to a specific\(trigger,prompt,handler\)\(\\text\{trigger\},\\text\{prompt\},\\text\{handler\}\)triple, never to emergent behaviour\. Trust attribution is local; failure attribution is local\.

### 4\.3 Limitations

#### Vision\-locked records\.

A meaningful subset ofMATHGeometry \(and a few records in Algebra\) reference Asymptote \(asy\) diagrams\. The current architecture has no vision integration; these records remain at the architectural ceiling without either \(a\) anasy\-declarative parser when the diagram explicitly specifies coordinates, or \(b\) a vision\-augmentedLLMthat interprets the rendered figure\. Geometry coverage plateaus near32%32\\%for this reason\.

#### NLP\-irreducible word problems\.

Multi\-paragraph word problems with named characters, contextual inferences, and conditional setup \(“Adam hasXX…; Bob boughtYY…; if both…”\) fall outside the1:1:11\{:\}1\{:\}1canonicalization frame\. A subset is recoverable via theWordToSystemchain task \([Section˜2\.3](https://arxiv.org/html/2606.00671#S2.SS3)\), which delegates extraction to theLLMbut routes the resulting linear system through a deterministic solver\. The residual requires either reasoning\-native model support or task\-specific extraction operators that have not yet been built\.

#### Intermediate Algebra ceiling\.

This domain — heavy on functional equations, complex modulus, ansatz\-driven proofs — is bounded near22​–​30%22\\text\{\-\-\}30\\%correct under the current architecture\. Closed\-formCAShandlers can only reach this far without prompt\-iteratedLoRAdistillation or a reasoning\-native model swap\. The cluster analysis of the production log \([Section˜3](https://arxiv.org/html/2606.00671#S3)\) confirms that the residual is dominated by shapes the deterministic layer cannot derive fromLLM\-canonicalized form alone\.

#### The bottom\-up commitment\.

A reasoning\-native model swap \(DeepSeek\-R1,Qwen 2\.5 Math,OpenAI o1\) would mechanically lift accuracy on hard records but would invert the architectural commitment: theLLMwould become the solver, not the canonicalizer, and the deterministic\-verification guarantee would no longer hold end\-to\-end\. We document this as a known design trade rather than a path forward; the contribution of this work is the verifiable architecture, not the highest accuracy attainable on any single benchmark\.

## 5 Related Work

#### LLM benchmarks for mathematical reasoning\.

Hendrycks et al\.\[[6](https://arxiv.org/html/2606.00671#bib.bib1)\]introduced theMATHbenchmark spanning77domains and55difficulty levels, which we use here for per\-domain evaluation\. Cobbe et al\.\[[2](https://arxiv.org/html/2606.00671#bib.bib2)\]introducedGSM8Kfor grade\-school word problems\. Lightman et al\.\[[8](https://arxiv.org/html/2606.00671#bib.bib3)\]demonstrated that process\-supervised reward models substantially help frontierLLMs onMATH\. The lm\-eval\-harness arithmetic suite\[[4](https://arxiv.org/html/2606.00671#bib.bib4)\]provides a20,00020\{,\}000\-record benchmark of bare\-arithmetic problems, which ourrule\_onlypath handles with mathematically provable correctness \([Section˜2\.4](https://arxiv.org/html/2606.00671#S2.SS4)\)\. Our position is orthogonal to these works: we do not aim for state\-of\-the\-art accuracy on any of these benchmarks; we contribute a verifiable architecture whose trust profile is the primary metric\.

#### Theorem proving with language\-model copilots\.

Lean Copilot\[[11](https://arxiv.org/html/2606.00671#bib.bib5)\]integratesLLMs into the Lean 4 interactive theorem prover, generating tactic suggestions verified by Lean’s kernel\. Llemma\[[1](https://arxiv.org/html/2606.00671#bib.bib6)\]pretrained anLLMon mathematical text and formal Lean corpora\. These systems require input pre\-formalized in a specific calculus \(Lean, Coq\);AXIOMtakes natural\-language input and verifies throughCASderivation, which is weaker than full formal verification but covers a much broader class of student\-style problems where formalization is the bottleneck\.

#### Symbolic and neuro\-symbolic systems\.

Wolfram Alpha\[[12](https://arxiv.org/html/2606.00671#bib.bib12)\]pioneered closed\-source expert\-system\-style mathematical answering with rich symbolic backends, but is not language\-model\-augmented and is not inspectable\.SymPy\[[9](https://arxiv.org/html/2606.00671#bib.bib10)\]provides our openCASbackend\. The neuro\-symbolic literature\[[5](https://arxiv.org/html/2606.00671#bib.bib7),[3](https://arxiv.org/html/2606.00671#bib.bib8)\]positions architectures along axes including: \(a\) whether the neural component is trained jointly with the symbolic, \(b\) whether inference is probabilistic or discrete, and \(c\) whether verification is intrinsic or extrinsic\.AXIOMoccupies a specific point:*frozen*LLM,*discrete*deterministicCASinference, and*intrinsic*verification by construction\. We are unaware of a published system in this exact configuration\.

#### Trust and verifiability frameworks\.

Huang et al\.\[[7](https://arxiv.org/html/2606.00671#bib.bib11)\]survey trust dimensions acrossLLMoutputs at the model level \(truthfulness, robustness, fairness\)\. Our contribution is complementary at the architectural level: rather than benchmark trust as an attribute of an opaque model, we structure a system in which trust is a runtime guarantee of the verification path\. Confident\-wrong is the failure mode the architecture defends against by construction, not a metric to be measured*post hoc*\.

## 6 Conclusion: today’s abstain, tomorrow’s correct

We have presentedAXIOM, a trust\-first neuro\-symbolic execution architecture for verifiable mathematical reasoning\. Four design commitments — the language model as canonicalizer \(not solver\), deterministicCASverification,1:1:11\{:\}1\{:\}1task routing, and abstain as first\-class structured output — together yield a runtime trust guarantee unavailable to either monolithicLLMsystems or pre\-formalized provers\. Empirically, the architecture clears a70/90/7070/90/70floor on fourMATHcategories with95​–​98%95\\text\{\-\-\}98\\%trust on parseable, achieves100%100\\%on the lm\-eval\-harness arithmetic suite, and has served approximately30,00030\{,\}000production queries with zero observed confident\-wrong incidents\.

The contribution we wish to emphasize, however, is not the specific accuracy figures: it is the*forward dynamic*the architecture establishes\. Every abstain emitted in production is logged with a structured fail\-reason that attributes the gap to a specific subsystem — router miss,LLMunknown, handler abstain, endpoint timeout\. Cluster analysis of these logs maps directly to candidate new tasks; the1:1:11\{:\}1\{:\}1invariant together with theLOST\_CORRECTscan oracle \([Section˜4\.1](https://arxiv.org/html/2606.00671#S4.SS1)\) ensure each new task can be shipped without regressing the existing registry\.AXIOMis therefore not a frozen artifact but a*monotonically\-improving scaffold*: coverage grows over time as triage cycles convert documented abstains into bench\-validated answered records, while the trust profile is preserved by construction across every ship\.

This dynamic reframes the limitations of[Section˜4\.3](https://arxiv.org/html/2606.00671#S4.SS3)\. Vision\-locked records,NLP\-irreducible word problems, and the Intermediate Algebra ceiling are not asymptotic walls of the architecture — they are the next inflection points on its growth path, each attackable by a corresponding extension to the registry, the chain framework, or the operator library\. The architectural commitment is what makes them*addressable rather than fixed*: we have a procedure for converting any well\-attributed abstain into a candidate correct, bounded only by curatorial effort, not by compute or model capacity\.

The contribution of this paper is therefore the framework, not a final accuracy figure\. Today’s abstain — documented, attributed, telemetered — is a candidate correct after one ship cycle\. We do not ask the reader to take this on faith: during preparation of this manuscript itself, the operational pipeline \(production telemetry→\\toabstain cluster analysis→\\tonarrow task creation→\\toregression\-oracle scan→\\toimmediate deploy\) was exercised three times in two hours, recovering∼17\\sim 17records from the no\-task pool with zerolost\_correctregressions \([Section˜3\.3](https://arxiv.org/html/2606.00671#S3.SS3)\)\. The architecture is built to support that conversion indefinitely\.

## Acknowledgments

The architecture rests on the open\-source ecosystem that makes deterministic symbolic verification feasible at deployment scale:SymPy\[[9](https://arxiv.org/html/2606.00671#bib.bib10)\]for the entireCASderivation layer, Hugging Face Transformers and FastAPI for theLLMrewriter and production service plumbing, and Together\.ai for the hosted inference endpoint that serves the live demo\. TheMATHbenchmark\[[6](https://arxiv.org/html/2606.00671#bib.bib1)\]and the lm\-eval\-harness arithmetic suite\[[4](https://arxiv.org/html/2606.00671#bib.bib4)\]provide the empirical ground used throughout this work\.

## References

- \[1\]Z\. Azerbayev, H\. Schoelkopf, K\. Paster, M\. D\. Santos, S\. McAleer, A\. Q\. Jiang, J\. Deng, S\. Biderman, and S\. Welleck\(2023\)Llemma: an open language model for mathematics\.arXiv preprint arXiv:2310\.10631\.External Links:[Link](https://arxiv.org/abs/2310.10631)Cited by:[§1](https://arxiv.org/html/2606.00671#S1.SS0.SSS0.Px1.p2.1),[§5](https://arxiv.org/html/2606.00671#S5.SS0.SSS0.Px2.p1.1)\.
- \[2\]K\. Cobbe, V\. Kosaraju, M\. Bavarian, M\. Chen, H\. Jun, L\. Kaiser, M\. Plappert, J\. Tworek, J\. Hilton, R\. Nakano,et al\.\(2021\)Training verifiers to solve math word problems\.arXiv preprint arXiv:2110\.14168\.External Links:[Link](https://arxiv.org/abs/2110.14168)Cited by:[§5](https://arxiv.org/html/2606.00671#S5.SS0.SSS0.Px1.p1.3)\.
- \[3\]L\. De Raedt, R\. Dušek, R\. Manhaeve, and G\. Marra\(2024\)From statistical relational to neurosymbolic artificial intelligence: a survey\.Artificial Intelligence Journal\.External Links:[Link](https://arxiv.org/abs/2108.11451)Cited by:[§5](https://arxiv.org/html/2606.00671#S5.SS0.SSS0.Px3.p1.1)\.
- \[4\]L\. Gao, J\. Tow, B\. Abbasi,et al\.\(2023\)A framework for few\-shot language model evaluation \(lm\-eval\-harness\)\.Zenodo\.External Links:[Link](https://github.com/EleutherAI/lm-evaluation-harness)Cited by:[§2\.4](https://arxiv.org/html/2606.00671#S2.SS4.p2.3),[§3\.2](https://arxiv.org/html/2606.00671#S3.SS2.p1.1),[§5](https://arxiv.org/html/2606.00671#S5.SS0.SSS0.Px1.p1.3),[Acknowledgments](https://arxiv.org/html/2606.00671#Sx1.p1.1)\.
- \[5\]A\. d\. Garcez and L\. C\. Lamb\(2023\)Neurosymbolic AI: the third wave\.Artificial Intelligence Review\.External Links:[Link](https://arxiv.org/abs/2012.05876)Cited by:[§5](https://arxiv.org/html/2606.00671#S5.SS0.SSS0.Px3.p1.1)\.
- \[6\]D\. Hendrycks, C\. Burns, S\. Kadavath, A\. Arora, S\. Basart, E\. Tang, D\. Song, and J\. Steinhardt\(2021\)Measuring mathematical problem solving with the MATH dataset\.NeurIPS Datasets and Benchmarks Track\.External Links:[Link](https://arxiv.org/abs/2103.03874)Cited by:[§5](https://arxiv.org/html/2606.00671#S5.SS0.SSS0.Px1.p1.3),[Acknowledgments](https://arxiv.org/html/2606.00671#Sx1.p1.1)\.
- \[7\]Y\. Huang, L\. Sun,et al\.\(2024\)TrustLLM: trustworthiness in large language models\.arXiv preprint arXiv:2401\.05561\.External Links:[Link](https://arxiv.org/abs/2401.05561)Cited by:[§5](https://arxiv.org/html/2606.00671#S5.SS0.SSS0.Px4.p1.1)\.
- \[8\]H\. Lightman, V\. Kosaraju, Y\. Burda, H\. Edwards, B\. Baker, T\. Lee, J\. Leike, J\. Schulman, I\. Sutskever, and K\. Cobbe\(2023\)Let’s verify step by step\.arXiv preprint arXiv:2305\.20050\.External Links:[Link](https://arxiv.org/abs/2305.20050)Cited by:[§5](https://arxiv.org/html/2606.00671#S5.SS0.SSS0.Px1.p1.3)\.
- \[9\]A\. Meurer, C\. P\. Smith, M\. Paprocki, O\. Čertík, S\. B\. Kirpichev, M\. Rocklin, A\. Kumar, S\. Ivanov, J\. K\. Moore, S\. Singh,et al\.\(2017\)SymPy: symbolic computing in Python\.PeerJ Computer Science3,pp\. e103\.External Links:[Document](https://dx.doi.org/10.7717/peerj-cs.103)Cited by:[§5](https://arxiv.org/html/2606.00671#S5.SS0.SSS0.Px3.p1.1),[Acknowledgments](https://arxiv.org/html/2606.00671#Sx1.p1.1)\.
- \[10\]Qwen Team\(2024\)Qwen2\.5 technical report\.arXiv preprint arXiv:2412\.15115\.External Links:[Link](https://arxiv.org/abs/2412.15115)Cited by:[§3](https://arxiv.org/html/2606.00671#S3.p2.1)\.
- \[11\]P\. Song, K\. Yang, and A\. Anandkumar\(2024\)Lean Copilot: large language models as copilots for theorem proving in Lean\.InNeurIPS Datasets and Benchmarks Track,External Links:[Link](https://arxiv.org/abs/2404.12534)Cited by:[§1](https://arxiv.org/html/2606.00671#S1.SS0.SSS0.Px1.p2.1),[§5](https://arxiv.org/html/2606.00671#S5.SS0.SSS0.Px2.p1.1)\.
- \[12\]Wolfram Research\(2009\)Wolfram Alpha computational knowledge engine\.Note:[https://www\.wolframalpha\.com](https://www.wolframalpha.com/)First released 2009; closed\-source proprietary system\.Cited by:[§1](https://arxiv.org/html/2606.00671#S1.SS0.SSS0.Px1.p2.1),[§5](https://arxiv.org/html/2606.00671#S5.SS0.SSS0.Px3.p1.1)\.