Skip to main content
Last updated: January 2026
Purpose: Document the human architectural decisions, trade-offs, and design thinking behind QWED

​
Core Philosophy

“Don’t reduce hallucinations. Make them irrelevant.”
Large Language Models (LLMs) are probabilistic and will always hallucinate. Rather than trying to fix the LLM, QWED verifies its outputs using deterministic solvers. The LLM becomes an untrusted translator, not a trusted computer.

​
Architecture: The Untrusted Translator Pattern

​
The Problem

Traditional approach: Trust the LLM to compute correctly
  • Train it better (fine-tuning)
  • Give it more context (RAG)
  • Ask it to check itself (LLM-as-judge)
Why this fails: LLMs are fundamentally probabilistic. No amount of training guarantees correctness.

​
The QWED Solution

Separation of concerns:
  1. LLM: Translates natural language → formal specification
  2. Symbolic Solver: Verifies the formal specification deterministically
User: "What is the derivative of x²?"
  ↓
LLM: Translates to → diff(x**2, x)
  ↓
SymPy: Computes → 2*x (proven correct)
  ↓
QWED: Returns verified result
Key insight: LLMs are good at translation, terrible at computation. Use them for what they’re good at.

​
Design Decision 1: Multiple Specialized Engines

​
The Trade-off

Option A: Single general-purpose verifier
  • Pros: Simpler architecture, one dependency
  • Cons: No general verifier matches domain-specific tools
Option B: Multiple domain-specific engines ← CHOSEN
  • Pros: Each domain uses decades of specialized research
  • Cons: More complex architecture, multiple dependencies

​
The Decision

Chosen: Multiple specialized engines Engines:
  • SymPy (math): Symbolic algebra, calculus, linear algebra
  • Z3 (logic): SAT/SMT solving, formal verification
  • AST (code): Static analysis, syntax validation
  • SQLGlot (SQL): Query parsing and validation
  • NLI + TF-IDF (facts): Grounding against source documents
Rationale: Each domain has specialized tools refined over decades. No general-purpose verifier can match the precision of SymPy for calculus or Z3 for logic. Better to integrate experts than build a generalist.

​
Design Decision 2: TF-IDF for Fact Grounding

​
The Trade-off

Option A: Vector embeddings (semantic similarity)
  • Pros: Captures semantic meaning, state-of-the-art
  • Cons: Probabilistic, can match opposite meanings
Option B: TF-IDF (lexical matching) ← CHOSEN
  • Pros: Deterministic, reproducible, searches for evidence
  • Cons: Doesn’t capture semantic similarity

​
The Decision

Chosen: TF-IDF for evidence retrieval Example of the problem with embeddings: 
query1 = "The Earth orbits the Sun"
query2 = "The Sun orbits the Earth"

# Embeddings similarity: 0.92 (HIGH!)
# Meaning: Completely opposite
TF-IDF advantage: Searches for actual word evidence, not “vibes” Academic validation: 10+ papers (2018-2025) from AAAI, ACL, Neurocomputing use TF-IDF for fact verification (FEVER dataset, etc.) Use case: For verification, you need evidence-based grounding, not semantic similarity.

​
Design Decision 3: LLM-as-Translator vs LLM-as-Judge

​
The Trade-off

Option A: LLM-as-judge (e.g., GPT-4 checks GPT-3.5)
  • Pros: Uses latest models, easy to implement
  • Cons: Both models probabilistic → recursive hallucination
Option B: Solver-as-judge ← CHOSEN
  • Pros: Deterministic, mathematical proof
  • Cons: Limited to verifiable domains

​
The Decision

Chosen: Symbolic solver as judge Comparison:
ApproachJudgeGuaranteeExample
LLM-as-judgeGPT-4Probabilistic”Probably correct”
QWEDSymPy/Z3Mathematical proof”Provably correct”
Rationale: If both judge and generator are probabilistic, errors compound. Need deterministic judge for verification. Limitation acknowledged: Only works for mathematically verifiable domains (math, logic, syntax). Not for creative writing or subjective content.

​
Design Decision 4: API Design Philosophy

​
The Trade-off

Option A: Low-level API (expose all solver internals)
  • Pros: Maximum flexibility
  • Cons: Steep learning curve, users need solver expertise
Option B: High-level developer-friendly API ← CHOSEN
  • Pros: Easy to use, hides complexity
  • Cons: Less control over solver behavior

​
The Decision

Chosen: High-level, developer-friendly API Design principles:
  1. Single method per domain: verify_math(), verify_logic(), verify_code()
  2. Smart routing: Auto-detect domain from query
  3. Rich error messages: Explain what failed and why
  4. Fallback values: Graceful degradation on verification failure
Example: 
# User doesn't need to know about SymPy internals
result = client.verify_math("What is 2+2?")
print(result.verified)  # True
print(result.value)  # 4
Rationale: Developers shouldn’t need to learn SymPy, Z3, AST separately. QWED provides a unified interface.

​
Design Decision 5: Integration Patterns

​
The Trade-off

Option A: Standalone verification service
  • Pros: Clean separation
  • Cons: Hard to integrate with existing LLM workflows
Option B: Framework integrations ← CHOSEN
  • Pros: Drops into LangChain, LlamaIndex, etc.
  • Cons: More maintenance, framework dependencies

​
The Decision

Chosen: Native integrations with popular frameworks Integrations:
  • LangChain: QWEDTool as native LangChain tool
  • LlamaIndex: Query engine wrapper
  • Direct API: For custom workflows
Rationale: Developers already use LangChain/LlamaIndex. QWED should integrate seamlessly rather than forcing workflow changes.

​
Design Decision 6: Error Handling Philosophy

​
The Trade-off

Option A: Fail fast (reject on any error)
  • Pros: Safe, conservative
  • Cons: Breaks user experience
Option B: Graceful degradation with audit trails ← CHOSEN
  • Pros: Better UX, transparent failures
  • Cons: Users might miss errors

​
The Decision

Chosen: Graceful degradation with comprehensive logging Pattern: 
try:
    result = verify_math(query, llm_output)
except VerificationError as e:
    log_error(e, audit_trail=True)
    return fallback_value  # User-defined
Features:
  • Audit trails: Log every verification attempt
  • Retry with exponential backoff: Handle transient LLM errors
  • Alert systems: Notify on repeated failures
  • Fallback values: User-defined safe defaults
Rationale: Production systems need resilience. Total failure is worse than controlled degradation with visibility.

​
Design Decision 7: PII Masking Strategy

​
The Trade-off

Option A: No PII handling (user responsibility)
  • Pros: Simpler architecture
  • Cons: Privacy risk, compliance issues
Option B: Built-in PII masking ← CHOSEN
  • Pros: HIPAA/GDPR compliance, privacy by default
  • Cons: Performance overhead, false positives

​
The Decision

Chosen: Optional built-in PII masking Implementation:
  • Uses Microsoft Presidio for entity detection
  • Masks before sending to LLM
  • Unmasks in verification step
  • Logs PII detection events
Rationale: Healthcare, finance, legal sectors require PII protection. Making it built-in lowers adoption barrier for regulated industries.

​
Design Decision 8: Calculator vs Wikipedia Analogy

​
The Mental Model

Why this matters: Helps users understand QWED’s scope Calculator (Deterministic):
  • Input: 2 + 2
  • Output: 4 (always)
  • Verifiable: ✅
Wikipedia (Knowledge Base):
  • Input: “Who is the president?”
  • Output: Depends on edit history
  • Verifiable: ❌ (subjective, changes)
QWED is a calculator, not Wikipedia:
  • ✅ Math: Provable
  • ✅ Logic: Provable
  • ✅ Code syntax: Provable
  • ❌ Opinions: Not provable
  • ❌ Creative content: Not provable

​
What QWED Is NOT

​
Rejected Design Paths

1. Novel Research
  • Not claiming: New verification algorithms
  • Claiming: Practical integration of existing solvers
2. LLM Improvement
  • Not claiming: Making LLMs more accurate
  • Claiming: Catching LLM errors deterministically
3. General AI Safety
  • Not claiming: Solving jailbreaks, toxicity, bias
  • Claiming: Verifying mathematical/logical correctness

​
Development Transparency

​
AI Assistance

This project was developed with assistance from generative AI tools: Tools used:
  • Antigravity IDE with Claude Sonnet 4.5
  • Scope: Code implementation, documentation, test generation
Human contributions:
  • All architectural decisions documented above
  • Trade-off analysis and solver selection
  • API design and integration patterns
  • Error handling philosophy
  • Domain modeling and verification workflows
Validation: All AI-generated code was reviewed, tested against benchmarks, and validated through comprehensive testing.

​
Lessons Learned

​
What Worked

  1. Specialized engines: Better than trying to build one general verifier
  2. Developer-friendly API: Easier adoption than low-level solver access
  3. TF-IDF for grounding: Deterministic evidence > semantic vibes
  4. Open development: Community contributions improved design

​
What We’d Change

  1. Earlier framework integrations: Should have built LangChain support sooner
  2. More domain tutorials: Users needed more examples per domain
  3. Clearer scope communication: “Calculator not Wikipedia” analogy should be upfront

​
References

Academic validation for design decisions:
  1. TF-IDF for fact verification:
    • FEVER Shared Task (2018): Fact verification benchmark
    • AAAI 2019: Combining fact extraction and verification
    • Neurocomputing 2023: Information retrieval for fact-checking
  2. Neurosymbolic AI:
    • Kautz (2020): The third AI summer
    • Marcus (2020): The next decade in AI
  3. LLM verification challenges:
    • Ji et al. (2023): Survey of hallucination in NLP
    • OpenAI (2023): GPT-4 technical report

​
Contributing to Design

Have suggestions on design improvements? Open an issue on GitHub to discuss! Questions welcome:
  • Why this solver over alternatives?
  • Trade-offs we should reconsider?
  • New design patterns?
GitHub Discussions: https://github.com/QWED-AI/qwed-verification/discussions