---
tags:
  - formal-verification
  - claim-verifier
  - onnx
  - research-prototype
  - carnot
license: apache-2.0
---

# 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

```bash
pip install carnot
```

```python
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

```python
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)

```python
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

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

<!-- carnot-exp317-exp316-results -->
## 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