Why Automated Reasoning?

The difference between pattern matching and automated reasoning isn't just technical. It's the difference between hoping your LLM behaves and proving it did.

Pattern Matching: The Common Approach

Most teams verify LLM outputs with regex patterns, keyword filters, or secondary LLM "judge" models. This works for simple cases but breaks down quickly:

# Check if loan recommendation mentions required fields
patterns = [
    r"credit score[:\s]+(\d{3})",
    r"loan amount[:\s]+\$?([\d,]+)",
    r"DTI[:\s]+(\d+)%"
]

# Problems:
# - Breaks when LLM says "FICO of 720" instead of "credit score: 720"
# - Can't verify "if score < 650 then amount must be < 50k"
# - No proof that all rules were checked
# - Maintenance nightmare as patterns multiply

The fundamental limitation: pattern matching finds text, but compliance requires verifying relationships between values.

Automated Reasoning: Mathematical Verification

aare.ai uses Z3, a satisfiability modulo theories (SMT) solver, to mathematically verify that extracted values satisfy your constraints. Instead of checking if text matches patterns, we prove whether constraints hold.

# Define your rules as logical constraints
constraints = {
    "loan_amount": {"<=": 100000},
    "credit_score": {">=": 600},
    "debt_to_income": {"<=": 0.43},
    "conditional": "credit_score < 650 -> loan_amount <= 50000"
}

# Z3 explores the entire solution space
# - If constraints are satisfiable: COMPLIANT (with proof)
# - If unsatisfiable: VIOLATION (with counterexample)

The Architecture

What Pattern Matching Cannot Do

The Compositional Advantage

Consider 10 business rules. With pattern matching, you check each independently. With automated reasoning, Z3 evaluates all 2¹⁰ = 1,024 possible states automatically.

• 20 rules: 1,048,576 possible states
• 30 rules: Over 1 billion possible states
• 76 rules (HIPAA ontology): ~10^23 possible states. Z3 uses symbolic reasoning to verify without enumeration

This is how Z3 catches rule interactions that humans miss: violations that only occur when specific combinations of conditions align.

Comparison

Capability	Pattern Matching	Automated Reasoning
Find "credit score: 720"	Yes	Yes (via extractors)
Verify score >= 600	Fragile	Proven
Verify "if score < 650 then amount < 50k"	No	Yes
Handle rule interactions	No	Complete
Explain violations	Pattern name only	Counterexample with values
Audit trail	"Pattern matched"	Machine-verifiable proof
Maintenance at scale	Exponential	Linear

The Proof Difference

Pattern Match Output

"Pattern matched" or "Pattern not found"
No explanation of why
No proof of correctness

Automated Reasoning Output

Verification ID: a8f3b2c
Status: VIOLATION

Constraint: LOAN_AMOUNT_LIMIT
  Formula: loan_amount <= 100000
  Extracted: loan_amount = 150000
  Result: 150000 > 100000 (UNSAT)

Counterexample:
  {loan_amount: 150000, credit_score: 720, dti: 0.35}

Violated at: "We recommend a loan of $150,000..."

When to Use Each

Pattern matching is appropriate for:

• Simple keyword blocking (profanity, PII detection)
• Format validation (email addresses, phone numbers)
• Single-value checks without relationships

Automated reasoning is required for:

• Regulatory compliance (HIPAA, financial regulations)
• Multi-variable constraints ("if X and Y then Z")
• Arithmetic relationships (limits, ratios, thresholds)
• Audit requirements with proof of compliance
• High-stakes decisions where false negatives are costly