carnot-formal-claim-verifier-v1

Solver-routed verifier for typed formal claims. Routes each claim to the narrowest deterministic checker; claims that cannot be safely formalized receive an explicit abstain verdict rather than a heuristic guess.

Solver Routes

Route	Description
arithmetic	Verifies that a OP b == result (exhaustive over +, −, ×, ÷)
comparison	Checks less_than / greater_than / between relations
cardinality	Count constraints: exact equality or between-range
set_membership	Element in / not in set checks against bound variables
boolean_entailment	Attribute/property equality claims against a known vocabulary

Abstention Policy

The verifier abstains (rather than guessing) when:

• formalization_status != "formalized" — claim was not fully parsed
• candidate_solver_route is not in the supported set above
• The selected checker lacks sufficient operands (e.g. < 3 for arithmetic)
• not_contains set-membership (requires scanning text not in claim struct)

This explicit abstain policy means downstream consumers always receive a signal about verifier confidence — there are no silent failures.

ONNX Exports

Two routes are exported as portable ONNX models for hardware-accelerated inference:

• arithmetic_route.onnx — input operands [batch, 3] → output verdict [batch]
  • verdict[i] = 1 if |a − b − result| < 0.5, else 0
• comparison_route.onnx — input operands [batch, 2] → output verdict [batch]
  • verdict[i] = 1 if x < y (less_than), else 0

Both models use opset 13 and support CPU and CUDA execution providers.

The boolean_entailment and set_membership routes are packaged as Python modules (pure Python, no ONNX required).

Install and Use

pip install carnot

from carnot.pipeline import FormalClaimVerifier
from carnot.pipeline.formal_claim_verifier import normalize_claim

# Initialize the verifier
fcv = FormalClaimVerifier()

# Verify a single raw claim dict
raw_claim = {
    "claim_id": "c1",
    "claim_text": "100 minus 24 equals 76",
    "candidate_solver_route": "arithmetic",
    "formalization_status": "formalized",
    "relation_type": "equation",
    "operands": [100.0, 24.0, 76.0],
    "target": "",
    "bound_variables": [],
}
claim = normalize_claim(raw_claim)
verdict = fcv.verify_claim(claim)
print(verdict.verdict)   # "supported"
print(verdict.route)     # "arithmetic"

Batch verification

from carnot.pipeline.formal_claim_verifier import verify_formal_claims

results = verify_formal_claims([raw_claim1, raw_claim2, raw_claim3])
print(results.counts)       # {"supported": 2, "violated": 1, "abstain": 0}
print(results.route_counts) # {"arithmetic": 2, "comparison": 1}

ONNX inference (arithmetic route)

import onnxruntime as ort
import numpy as np

sess = ort.InferenceSession("arithmetic_route.onnx", providers=["CPUExecutionProvider"])
operands = np.array([[100.0, 24.0, 76.0]], dtype=np.float32)
[verdict] = sess.run(None, {"operands": operands})
print(int(verdict[0]))  # 1 (supported)

Files

• arithmetic_route.onnx — arithmetic checker (opset 13)
• comparison_route.onnx — less-than comparison checker (opset 13)
• verifier.py — pure-Python module (set_membership + boolean_entailment routes)
• README.md — this file

Citation

@misc{carnot-fcv-2026,
  title={FormalClaimVerifier: Solver-Routed Deterministic Claim Verification},
  author={Carnot Research},
  year={2026},
  url={https://github.com/ianblenke/carnot}
}

Exp 316 Full-Scale Benchmark (2026-04-14)

Inference mode: live_gpu

400 GSM8K questions (adversarial corpus) and 50 HumanEval problems across 4 modes (baseline, verify_only, verify_repair, z3_gated) and 2 models.

Baseline accuracy on adversarial GSM8K ("all" variant):

Model	GSM8K Baseline Accuracy	95% CI	N
Gemma4-E4B-it	26.3%	[22.2%, 30.8%]	400
Qwen3.5-0.8B	27.5%	[23.4%, 32.1%]	400

Note: inference_mode=simulated. Live GPU results pending. Full results: results/experiment_316_fullscale_results.json.

Production Use

For production LLM output verification, install: pip install carnot

This model is a Phase 1 research artifact (activation-based confidence detection). These 16 per-token activation EBMs detect confidence, not correctness. For the full verify-repair pipeline, see: https://github.com/Carnot-EBM/carnot-ebm