Skip to main content
TL;DR: QWED uses deterministic solvers (SymPy, Z3, AST, SQLGlot) wherever possible. When LLM fallback is required, the response is explicitly marked as HEURISTIC.

​
Engine Classification

Every QWED verification engine falls into one of three categories:
CategoryEnginesTechnologyReproducible?
100% SymbolicMath, Logic, Code, SQL, Schema, TaintSymPy, Z3, AST, SQLGlot✅ Yes
HybridFact, StatsTF-IDF / Sandbox → LLM fallback⚠️ Conditional
HeuristicImage, Consensus, ReasoningVLM / Multi-LLM voting❌ No

​
Detailed Breakdown

EngineModePrimary TechnologyLLM Fallback?
MathSymbolicSymPy (symbolic algebra)❌ Never
LogicSymbolicZ3 Theorem Prover (SMT)❌ Never
CodeSymbolicPython AST + Bandit❌ Never
SQLSymbolicSQLGlot AST parser❌ Never
SchemaSymbolicPydantic + SymPy❌ Never
TaintSymbolicData Flow Analysis (AST)❌ Never
FactHybridTF-IDF similarity✅ When TF-IDF confidence < threshold
StatsHybridWasm/Docker sandbox✅ When sandbox execution fails
ImageHeuristicVision LLM (GPT-4V, Claude)✅ Always
ConsensusHeuristicMulti-LLM voting✅ Always
ReasoningHeuristicChain-of-thought LLM✅ Always

​
How to Know Which Mode Was Used

Every API response includes a verification_mode field: 
{
  "status": "VERIFIED",
  "verified": true,
  "engine": "math",
  "verification_mode": "SYMBOLIC",
  "result": { ... }
}

​
verification_mode Values

ValueMeaningTrust Level
SYMBOLICResult proven by deterministic solver (SymPy/Z3/AST)🟢 100% reproducible
HEURISTICResult from LLM fallback or multi-model voting🟡 Best-effort, not guaranteed

​
Why This Matters

​
For Regulated Industries

Banks, healthcare, and legal systems require audit trails and reproducibility:
  • ✅ SYMBOLIC results can be independently verified
  • ⚠️ HEURISTIC results should be flagged for human review

​
For Production Systems

result = client.verify_math("2+2=4")

if result.verification_mode == "SYMBOLIC":
    # Safe to use without human review
    process_result(result)
elif result.verification_mode == "HEURISTIC":
    # Flag for human review or additional validation
    queue_for_review(result)

​
Design Philosophy

“Probabilistic systems should not be trusted with deterministic tasks.”
QWED treats LLMs as untrusted translators:
  1. LLM converts natural language → formal specification
  2. Deterministic solver verifies the formal specification
  3. If solver cannot verify, result is marked HEURISTIC
┌─────────────────────────────────────────────────────────┐
│                    QWED Protocol                        │
├─────────────────────────────────────────────────────────┤
│  User Query → LLM (Translator) → DSL → Solver → Result │
│                                                         │
│  Solver = SymPy/Z3/AST  →  SYMBOLIC                     │
│  Solver = LLM Fallback  →  HEURISTIC                    │
└─────────────────────────────────────────────────────────┘

​
Frequently Asked Questions

​
Q: Can I filter responses by verification_mode?

A: Yes! Use the require_symbolic option in your request: 
result = client.verify(
    query="Calculate NPV",
    options={"require_symbolic": True}
)
# Fails if solver cannot verify deterministically

​
Q: Why is Fact verification sometimes HEURISTIC?

A: Fact verification uses TF-IDF (deterministic) to find evidence. If TF-IDF confidence is below threshold, it falls back to NLI (LLM-based), marking the result as HEURISTIC.

​
Q: Is Consensus useful if it’s HEURISTIC?

A: Yes! Consensus detects disagreement between multiple LLMs. While not deterministic, it catches cases where models are uncertain — useful as a safety net, not a formal verifier.

​
See Also