VerifAxis

A verification axis for frozen LLMs: think, test, falsify, revise, or abstain.

Language models can revise an answer repeatedly without learning whether it is correct. VerifAxis puts an unchanged model in a bounded loop with independent, executable verifiers. Evidence is typed and auditable; unresolved or conflicting evidence leads to abstention rather than a confident guess.

VerifAxis is an exploratory research runtime and benchmark. It is not a truth machine and does not eliminate hallucinations.

Quick start

Requires Python 3.11+. Install locally with python -m pip install ., then run this five-line example:

from verifaxis import verify
from verifaxis.models import ReplayModel
from verifaxis.verifiers import SafeMathVerifier

result = verify("What is 197 * 83?", ReplayModel(), [SafeMathVerifier()], 4)
print(result.answer, result.status.value)

Expected deterministic output:

16351 VERIFIED

No API key, network, GPU, or paid call is needed.

Before and after

ReplayModel deliberately gets the first attempt wrong. The math verifier parses only a strict arithmetic AST, reports the violated equality and expected value, and the model revises only after receiving that independent evidence:

$ verifaxis demo
{
  "final_answer": "16351",
  "initial_answer": "16352",
  "iterations": 2,
  "label": "smoke/demo",
  "model_calls": 2,
  "status": "VERIFIED",
  "task": "What is 197 * 83?",
  "verifier_calls": 2
}

This is smoke/demo output, not a benchmark result.

Architecture

VerifAxis implements Verifier-Conditioned External Recurrence (VCER):

flowchart LR
    T["Task + bounded budget"] --> M["Frozen ModelAdapter"]
    M --> C["Candidate"]
    C --> V["Independent Verifier(s)"]
    V --> E["Typed EvidencePacket(s)"]
    E --> R["EvidenceResidual"]
    R --> K{"VerificationController"}
    K -->|"verified"| O["Answer + JSON trace"]
    K -->|"revise"| M
    K -->|"conflict, unverifiable, or exhausted"| A["Abstain + JSON trace"]

Loading

The loop persists candidates, concise structured state, evidence hashes, residuals, budgets, and termination decisions. It neither requests nor stores private chain-of-thought. LLM-generated criticism is always marked as LLM-produced and never silently treated as independent evidence.

The black-box adapter supports OpenAI-compatible HTTP endpoints, including compatible local servers. Open-weight latent recurrence is an interface-level future direction only; v0.1 makes no claim that it works.

What VerifAxis does not guarantee

• A passing verifier proves only the checked property within that verifier's scope.
• Bugs, missing constraints, stale state, or compromised verifiers can still produce wrong outcomes.
• Retrieved text is not automatically true or independent evidence.
• More iterations can regress correct answers; the benchmark measures that transition explicitly.
• Arbitrary model-generated Python is never executed by the default verifiers.

See the threat model and novelty decision.

CLI and reproduction

verifaxis demo
verifaxis run examples/arithmetic.yaml
verifaxis bench --config configs/smoke.yaml
verifaxis report runs/latest --format html

Run all offline checks:

python -m pip install -e ".[dev]"
ruff format --check .
ruff check .
mypy src
pytest
python -m build

The smoke benchmark runs direct, intrinsic Self-Refine, Best-of-N, a fixed external-feedback loop, random stopping, residual-aware VCER, a tool-augmented initial-answer baseline, and an oracle allocation upper bound. Budgets and tool access are reported rather than hidden. See reproducing and the benchmark card.

Add a verifier

Implement the Verifier protocol and return an EvidencePacket for every applicable check. A verifier must document its version, checked claim, provenance, independence class, reliability assumptions, raw artifact policy, and whether any field came from an LLM. Counterexamples should be machine-readable when possible.

class MyVerifier:
    name = "my-verifier"
    version = "1"

    def verify(self, *, task, candidate): ...

Start with src/verifaxis/verifiers/ and the security boundaries in CONTRIBUTING.md.

Research status

The Phase-0 audit produced a PIVOT. External tool-conditioned correction, recurrence, adaptive stopping, and counterexample-guided iteration all have direct prior art. The defensible contribution is a model-agnostic runtime and benchmark for typed evidence, correction/regression dynamics, matched accounting, safe stopping, and verifier-fault experiments. Read the prior-art audit and frozen research contract before interpreting results.

License and citation

Apache-2.0. Public author credit: Ali. See CITATION.cff.