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

The paper introduces AXIOM, a trust-first neuro-symbolic architecture that leverages language models solely to canonicalize natural language problems into a deterministic Computer-Algebra-System pipeline, achieving 94.36% correctness with 100% trust (zero confident errors) on mathematical benchmarks while ensuring that system improvements never regress previously verified results.

The Gist

Imagine you are trying to solve a complex math problem, but instead of asking a brilliant but sometimes overconfident genius, you are asking a very organized, slightly rigid, but incredibly honest librarian.

That is the core idea behind AXIOM, a new system designed to do math reasoning with a "trust-first" mindset. Here is how it works, broken down into simple concepts and analogies.

The Problem: The "Confidently Wrong" Genius

Current AI models (like the ones you chat with) are like brilliant students who love to guess. If they don't know the answer, they might just make one up and present it with total confidence. In math, this is dangerous because a wrong answer looks exactly the same as a right one to the user. You have no way of knowing if the AI is lying or just hallucinating.

The AXIOM Solution: The "Specialized Assembly Line"

AXIOM doesn't try to be a genius who solves everything from scratch. Instead, it acts like a highly efficient factory assembly line with four strict rules:

1. The Sorter (The Regex Router)

When a question arrives, it doesn't go straight to the AI. First, it hits a Sorter. Think of this as a mailroom clerk who looks at the envelope's shape.

• If the letter looks like a "simple arithmetic" note, it gets sent to the Fast Lane.
• If it looks like an "algebra" note, it goes to the Algebra Station.
• If the shape doesn't match any known category, the clerk immediately stamps it "Unknown" and stops. It never guesses.

2. The Translator (The AI as a "Rewriter")

If the letter makes it to a station, it doesn't ask the AI to solve the problem. Instead, the AI acts as a Translator.

• Old Way: "Here is a word problem, please solve it." (AI guesses the steps).
• AXIOM Way: "Here is a word problem. Please rewrite it into this specific, narrow format that our calculator understands."
  The AI is strictly forbidden from doing the math itself. It just cleans up the sentence so the next step can read it perfectly.

3. The Calculator (The Deterministic Engine)

Once the AI rewrites the problem, it passes it to a Calculator (a computer algebra system). This is a robot that never guesses, never gets tired, and never hallucinates.

• It takes the rewritten problem and crunches the numbers.
• If it can solve it, it gives the answer.
• If it can't solve it (maybe the math is too weird or the input was slightly off), it stops and says, "I cannot verify this."

4. The "Honesty" Rule (Abstaining)

This is the most important part. In most systems, if the calculator fails, the system might try to guess anyway. In AXIOM, saying "I don't know" is a valid, structured answer.
If any part of the line fails (the Sorter didn't recognize the shape, the Translator couldn't rewrite it, or the Calculator couldn't solve it), the system outputs a clear message: "I am abstaining." It never gives a confident wrong answer.

The Results: Speed and Safety

The paper reports some impressive stats from testing this system:

• Zero Confident Mistakes: Across thousands of tests, the system never gave a wrong answer that looked like a right one. If it gave an answer, it was verified.
• High Accuracy: On standard math tests, it got about 94% of the questions right.
• Speed: For simple math (like "2 + 2"), it skips the AI translator entirely and solves it in 1 millisecond (faster than you can blink). For harder stuff, it's still much faster than asking a standard AI to "think step-by-step."
• Cost: Because it doesn't ask the AI to write long essays or guess, it costs almost nothing to run.

The "Forward Dynamic": Getting Better Without Breaking

The authors emphasize that this system is designed to grow.

• Imagine the system encounters a new type of math problem it doesn't know. Instead of failing silently or guessing, it logs: "I saw this shape, but I don't have a station for it."
• The developers can then build a new "Station" (a new rule) specifically for that shape.
• Because every station is isolated, adding a new one never breaks the old ones. It's like adding a new lane to a highway; it doesn't cause traffic jams in the existing lanes.

Summary Analogy

Think of a standard AI as a magician who pulls answers out of a hat. Sometimes the rabbit is there; sometimes it's a sock, but the magician acts like it's a rabbit.

AXIOM is a quality control inspector.

1. It checks if the item fits the box.
2. It labels the item clearly.
3. It runs it through a machine that measures it.
4. If the machine can't measure it, it puts a "Rejected" tag on it.

It might reject more items than a magician would, but every item that leaves the factory with a "Pass" tag is guaranteed to be correct.

Technical Summary

Technical Summary: AXIOM – A Trust-First Neuro-Symbolic Execution Architecture

1. Problem Statement

The paper addresses the fundamental lack of verifiability in frontier Large Language Model (LLM) mathematical reasoning. While LLMs achieve high accuracy on benchmarks, they operate via a "prompt-in-text-out" interface where a confident-wrong answer is structurally indistinguishable from a correct one. Existing alternatives have significant trade-offs:

• Lean-based provers require problems to be pre-formalized in a specific syntax (e.g., Lean), creating a bottleneck for natural language queries.
• Closed expert systems (e.g., Wolfram Alpha) offer symbolic backends but lack LLM augmentation at the input boundary and do not provide inspectable derivation traces.

The authors argue that "confident-wrong" is the worst failure mode in mathematical reasoning. They propose shifting the design goal from "accuracy-first" to "trust-first," defining trust as $1 - \frac{\text{wrong}}{\text{attempted}}$, where "wrong" excludes records the system explicitly abstains from answering.

2. Methodology: The AXIOM Architecture

AXIOM is a neuro-symbolic execution architecture where the LLM functions strictly as a canonicalizer, not a solver. The system routes natural language (NL) input through a deterministic Computer Algebra System (CAS) pipeline. The core design relies on four commitments:

2.1 1:1:1 Task Routing Alignment

Instead of a monolithic LLM or a generic handler, AXIOM employs a 1:1:1 invariant:

1. Trigger: A problem-shape regex that selects exactly one task.
2. Prompt: A schema-specific prompt with few-shot examples tailored to that specific shape.
3. Handler: A deterministic CAS handler that consumes only that specific schema.

This alignment ensures that adding a new task ($T_{N+1}$) cannot regress existing tasks ($T_1 \dots T_N$) because their code paths are disjoint. This prevents the "representational budget" competition found in monolithic models.

2.2 Abstain as a First-Class Output

The system treats answer=null as a structural, valid output rather than a failure. Three independent channels can trigger an abstain:

1. Router Miss: No regex trigger matches the input.
2. Translator Abstain: The LLM explicitly returns unknown (taught via few-shot examples) when it cannot rewrite the input into the schema without guessing.
3. Handler Abstain: The CAS pipeline cannot derive a verified answer (e.g., encountering an unrecognized predicate or a ConditionSet).

Crucially, the system enforces a whitelist guard: if a handler encounters an unrecognized predicate, it must abstain rather than defaulting to a value (e.g., zero), preventing "confident-wrong" outputs.

2.3 Composed-Task Chain Framework

For multi-step problems (e.g., piecewise functions requiring parsing, solving per branch, and aggregating), AXIOM uses a ComposedTask framework. This chains deterministic operators (pure functions) where the LLM is called only once at the start (InitialExtractor). The chain validates dependencies at registration time, ensuring that failure at any step results in a clean abstain rather than a silent error.

2.4 Rule-Only Path

For closed-form bare arithmetic (digits and operators with no prose), the LLM step is bypassed entirely. The system routes directly to a deterministic CAS evaluator. This path guarantees bit-equivalence across runs and zero inference cost.

3. Key Contributions

The paper emphasizes the forward dynamic of the architecture rather than a static accuracy figure. The primary contributions are:

• Architectural Framework: A 1:1:1 routing system with a rule-only bypass and a composed-task chain for multi-step logic.
• Operational Discipline: A set of principles for trustworthy neuro-symbolic systems, including:
  • Math-template bucketing: Routing based on solver structure, not surface phrasing.
  • LOST_CORRECT scan: A pre-commit regression oracle that replays archived benchmarks to ensure new tasks do not break existing ones.
  • Predicate-not-recognized = Abstain: A structural defense against confident-wrong outputs.
  • Parseable-first onboarding: Optimizing for the rate of parseable inputs before optimizing for trust in new domains.
• Linear-Additive Returns: Unlike monolithic LLMs which exhibit logarithmic returns (diminishing accuracy gains), AXIOM's coverage grows linearly with the number of registered tasks, as tasks do not suppress one another.

4. Empirical Results

The architecture was evaluated on the MATH benchmark (4 categories), the lm-eval-harness arithmetic suite, and a public production deployment (~30,000 queries).

• MATH Benchmark (4 Categories):
  • Cumulative Correctness: 94.36% (2,592/2,747).
  • Trust on Parseable: 100.00% across all four domains (Algebra, Number Theory, Counting & Probability, Precalculus). There were zero confident-wrong answers.
  • Latency: Median 446 ms for LLM-bound tasks; 1 ms for rule-only tasks.
• lm-eval-harness Arithmetic:
  • Correctness: 100.0% (20,000/20,000).
  • Cost: Zero LLM API calls; 21.6s wall time on commodity CPU.
• Production Deployment:
  • Served ~30,000 queries with zero confident-wrong incidents at the API boundary.
  • Latency Separation: ~400x difference between rule-only (1 ms) and LLM-bound (446 ms) paths.
• Comparison with Pure LLM (Qwen 2.5 7B CoT):
  • AXIOM significantly outperformed the pure CoT baseline in accuracy on harder domains (e.g., +38.2 pp on Precalculus) while emitting 0 wrong answers compared to hundreds for the CoT baseline.
  • AXIOM was ~24x to ~40x faster on average due to narrow prompting and lack of iterative reasoning loops.

5. Significance and Claims

The paper claims that AXIOM establishes a runtime trust guarantee unavailable to monolithic LLMs or pre-formalized provers. The significance lies not in achieving a specific accuracy score, but in the forward dynamic it enables:

• Monotonic Improvement: Every logged abstain in production is a candidate for a correct answer in the next ship cycle. The system is designed to convert abstains into correct answers via targeted task creation without regressing existing performance.
• Verifiability: Trust is an architectural property derived from the verification path (deterministic CAS), not a property of the underlying model.
• Scalability: The architecture supports the incremental addition of thousands of task triples (3,100+ shipped) with zero lost_correct regressions over 250+ commits.

The authors acknowledge limitations, including a ceiling on vision-locked geometry problems (due to lack of vision integration) and NLP-irreducible word problems, but frame these as the next inflection points for the registry rather than asymptotic walls. The core contribution is the framework that allows "today's abstain" to become "tomorrow's correct" through a disciplined, verifiable engineering process.