After studying this material, you should be able to:

1. Explain why rule engines require complete inputs and why this is problematic in conversational settings
2. Describe the limitations of pure language models and pure symbolic enumeration for answering regional questions
3. Understand the neurosymbolic approach that combines both methods
4. Define key concepts: regions, partitions, SMT solvers, concolic execution, and completeness guarantees
5. Explain how the system works end-to-end using Catala as a concrete example

---

Step-by-Step Study Material

Step 1: Understanding the Problem Domain

What is a Rule Engine?

A rule engine is a system that:

• Takes a fully specified set of typed input variables
• Maps them to a finite set of output categories

Input Variables (complete) → Rule Engine → Output Category

Real-world examples:

The Core Requirement Problem

Rule engines were designed assuming complete inputs

This works perfectly when a computer fills out every field. But humans don't think this way.

---

Step 2: Understanding "Regional Questions"

How Humans Actually Ask Questions

Instead of:

"I am 67 years old, earn $34,000/year, have lived in France for 12 years, and have 2 dependents — am I eligible?"

Humans ask:

"Are retired people eligible for this benefit?" "What happens if someone earns under $40,000?"

Defining a "Region"

A region is a subset of the input space where some variables are specified and others are left open (under-specified).

Full Input Space = all possible combinations of all variables

Region = {
  age: "retired" (specified),
  income: ??? (unspecified),
  residency: ??? (unspecified),
  dependents: ??? (unspecified)
}

Visually:

┌─────────────────────────────────────┐
│         Full Input Space            │
│                                     │
│   ┌─────────────────┐               │
│   │   Region        │               │
│   │ (age=retired,   │               │
│   │  others open)   │               │
│   └─────────────────┘               │
│                                     │
└─────────────────────────────────────┘

Key insight: The question defines a region, not a single point.

---

Step 3: Why Existing Approaches Fail Alone

Approach 1: Pure Language Model (LLM)

An LLM reads the rules and tries to answer in natural language.

What it does well:

• Understands natural language questions
• Produces readable answers
• Handles vague or incomplete questions

Critical failure:

❌ No completeness guarantee

The LLM might say:

"Retired people are generally eligible if they meet income requirements."

But it may miss edge cases, misread rule interactions, or hallucinate conditions.

As the decision space grows (more variables, more rules), the gap between what the LLM says and what is actually true widens.

Reliability
    │
100%│ ──── Symbolic (always complete)
    │
    │         LLM
 50%│    ─────────────────────────────
    │                    ↘ (degrades)
    │
  0%└────────────────────────────────→
         Decision Space Complexity

---

Approach 2: Pure Symbolic Enumeration

A symbolic system explores every possible execution path through the rule engine.

What it does well:

• Finds every path through the rules
• Produces a complete partition of the input space
• Mathematically provable

Critical failure:

❌ Partition explosion — too large to summarize faithfully

Imagine a rule with 10 binary variables:

• 2¹⁰ = 1,024 possible paths
• A real legal rule might have 20+ variables
• 2²⁰ = 1,048,576 paths

Presenting all paths to a user is useless — it's overwhelming and incomprehensible.

User asks: "Are retired people eligible?"

Symbolic system returns:
  Path 1: age≥65 ∧ income<20000 ∧ residency>10 ∧ dependents=0 → ELIGIBLE
  Path 2: age≥65 ∧ income<20000 ∧ residency>10 ∧ dependents=1 → ELIGIBLE
  Path 3: age≥65 ∧ income<20000 ∧ residency>10 ∧ dependents=2 → ELIGIBLE
  ... (1,000+ more paths)

This is complete but not useful.

---

Step 4: The Neurosymbolic Solution

Core Idea

Combine the completeness of symbolic enumeration with the communicability of language models, using a budget-controlled follow-up question strategy.

The method has three key components:

┌──────────────────────────────────────────────────────┐
│              NEUROSYMBOLIC SYSTEM                    │
│                                                      │
│  [LLM Agent]  ←→  [Symbolic Enumerator]  ←→  [SMT]  │
│                                                      │
│  • Lifts question    • Enumerates paths  • Verifies  │
│    to a region       • Partitions space    completeness│
│  • Verbalizes        • Finds best                    │
│    answer              follow-up                     │
└──────────────────────────────────────────────────────┘

---

Component 1: Question Lifting (LLM Role)

The LLM translates a natural language question into a formal region.

Natural Language:          Formal Region:
"Are retired people?"  →   { age: ≥65, income: *, residency: *, ... }

The * means "unspecified" — this is what makes it a region rather than a point.

---

Component 2: Symbolic Path Enumeration

The system runs the rule engine symbolically over the entire region, finding all execution paths.

Concolic execution = concrete + symbolic execution

• Runs the engine with symbolic (unspecified) variables
• Discovers all branches/paths the rules can take
• Produces a partition: a set of sub-regions, each with a definite answer

Region: { age: ≥65, others: * }

Partition:
  Sub-region A: age≥65 ∧ income<30000 → ELIGIBLE
  Sub-region B: age≥65 ∧ income≥30000 ∧ residency>5 → ELIGIBLE
  Sub-region C: age≥65 ∧ income≥30000 ∧ residency≤5 → INELIGIBLE

---

Component 3: SMT Solver Verification

SMT = Satisfiability Modulo Theories — a formal logic solver.

The system reconstructs the rule engine's path constraints in the SMT solver to verify:

✅ The partition is complete — every point in the region falls into exactly one sub-region

This is a checked theorem, not a claim. The difference matters:

---

Component 4: Budget-Controlled Follow-Up Questions

When the partition is too large to present usefully, the system asks the single best follow-up question.

How to find the best question:

The goal is to find the variable that removes the most cases (maximizes information gain):

Partition has 500 sub-regions

Question: "What is the person's income level?"
  → If income < $30,000: reduces to 50 sub-regions
  → If income ≥ $30,000: reduces to 450 sub-regions
  → Average reduction: significant ✓

Question: "Does the person have a middle name?"
  → Irrelevant to rules
  → No reduction ✗

The system picks the question with the maximum reduction in partition size.

This creates a natural conversation:

User:   "Are retired people eligible?"
System: "Are they earning under $30,000/year?"
User:   "Yes."
System: "They are eligible if they have lived here for more than 5 years,
         otherwise they must apply for an exception. [Cite: Article 12, §3]"

---

Step 5: The Complete System Architecture

                    USER QUESTION
                         │
                         ▼
              ┌─────────────────────┐
              │    LLM Agent        │
              │  "Question Lifting" │
              │  Natural language   │
              │  → Formal region    │
              └─────────┬───────────┘
                        │  Region specification
                        ▼
              ┌─────────────────────┐
              │   CUTECat Engine    │
              │  (Concolic executor │
              │   for Catala)       │
              │  Enumerates all     │
              │  paths in region    │
              └─────────┬───────────┘
                        │  Raw partition
                        ▼
              ┌─────────────────────┐
              │   SMT Solver        │
              │  Verifies partition │
              │  is complete        │
              │  (checked theorem)  │
              └─────────┬───────────┘
                        │  Verified partition
                        ▼
              ┌─────────────────────┐
              │  Budget Controller  │
              │  Is partition small │
              │  enough to present? │
              └──────┬──────────────┘
                     │
          ┌──────────┴──────────┐
          │ YES                 │ NO
          ▼                     ▼
   ┌─────────────┐    ┌──────────────────────┐
   │ LLM Agent   │    │ Find best follow-up  │
   │ Verbalizes  │    │ question (max cases  │
   │ answer with │    │ removed)             │
   │ citations   │    └──────────┬───────────┘
   └─────────────┘               │
                                 ▼
                        Ask user → loop back

---

Step 6: Catala — The Concrete Implementation

What is Catala?

Catala is a domain-specific programming language designed specifically for encoding legal rules as executable code.

Why Catala?

• Legal rules have complex priority systems (exceptions override general rules)
• Catala's syntax mirrors legal document structure
• It produces an executable rule engine from legal text

Example (conceptual):

# Article 12 - Benefit Eligibility
scope BenefitEligibility:
  rule eligible under condition
    applicant.age >= 65
    and applicant.income < income_threshold
  consequence fulfilled

CUTECat

CUTECat is Catala's concolic execution engine:

• CUTECat = Concolic Unit TEsting for Catala
• Drives the Catala rule engine symbolically
• Enumerates all execution paths

The Evaluation

The system was tested on:

• French legal texts (encoded in Catala)
• United States legal texts (encoded in Catala)

Results:

---

Step 7: Key Concepts Summary

---

Step 8: Why This Matters — The Big Picture

Traditional Rule Engine:
  Complete input required → Single answer
  
Chatbot with LLM only:
  Partial input accepted → Possibly wrong/incomplete answer
  
This System:
  Partial input accepted → Provably complete answer
  (with follow-up questions if needed)

The fundamental insight:

A question is not a point — it is a region. Treating it as a region allows us to give answers that are both complete (symbolic guarantee) and comprehensible (LLM verbalization).

---

Self-Check Questions

1. Why can't a rule engine handle a regional question directly?
2. What is the difference between a "claim of completeness" and a "checked theorem of completeness"?
3. Why does the system ask only one follow-up question rather than all necessary questions at once?
4. What role does the LLM play, and what role does the symbolic system play? Why can't either do the job alone?
5. What does "concolic" mean, and why is it useful here?
6. If a partition has 1,000 sub-regions, how does the system decide which follow-up question to ask?