Interpreting SMT Results

Understand and explain SMT solver outputs with LLM-generated interpretations

Overview

The interpret_smt_results.py script analyzes SMT solver outputs and generates human-readable explanations for logical fallacies. It provides counter-examples when arguments are invalid.

How It Works

1. Read SMT Output

   Loads the solver output file containing SAT/UNSAT result and counter-model.

2. Parse Result

   Determines if the formula is valid (UNSAT) or contains a fallacy (SAT).

3. Load Sentence Data

   Reads the JSON file with claim, implication, entities, properties, and formula.

4. Generate Interpretation

   Uses LLM to interpret the counter-model in natural language (for fallacies only).

5. Display Results

   Prints the validity status and human-readable explanation.

Command Usage

Basic Command

python3 src/interpret_smt_results.py <output_of_smt_file_path> <json_sentence_data_path>

Parameters

output_of_smt_file_path · string · required

Path to the SMT solver output file (e.g., results/run_name_smt/0_out.txt).

This file should contain:

• First line: sat or unsat
• Subsequent lines: Counter-model (if SAT)

json_sentence_data_path · string · required

Path to JSON file containing the sentence analysis data.

Required fields:

• Claim - The extracted claim
• Implication - The extracted implication
• Referring expressions - Entity mappings
• Properties - Property assignments
• Formula - The FOL formula

Example Usage

Basic Example

python3 src/interpret_smt_results.py \
  results/experiment_1_smt/0_out.txt \
  results/experiment_1_data/0.json

# Interpret first 10 results
for i in {0..9}; do
  python3 src/interpret_smt_results.py \
    results/experiment_1_smt/${i}_out.txt \
    results/experiment_1_data/${i}.json
done

Input File Formats

SMT Output File Format

Valid Argument (UNSAT):

unsat

Logical Fallacy (SAT) with Counter-Model:

sat
(model
  (define-fun Human ((x!0 Entity)) Bool
    (ite (= x!0 a) true false))
  (define-fun Mortal ((x!0 Entity)) Bool
    (ite (= x!0 a) false false))
)

JSON Sentence Data Format

{
  "Claim": "All humans are mortal",
  "Implication": "Socrates is mortal",
  "Referring expressions": "humans, Socrates",
  "Properties": "Human(a), Mortal(a)",
  "Formula": "forall a (Human(a) -> Mortal(a))"
}

Output Examples

Valid Statement

The given statement is a valid statement

Logical Fallacy with Interpretation

The given statement is a logical fallacy

Counter-example explanation:
The argument fails because it assumes all humans are mortal and 
that Socrates is human, but the model shows a case where Socrates 
could be human but not mortal. This violates the logical structure 
of the argument.

Specifically, the counter-model assigns:
- Human(Socrates) = true
- Mortal(Socrates) = false

This demonstrates that the implication does not necessarily follow 
from the claim.

SMTResults Class

The interpretation logic is implemented in the SMTResults class:

class SMTResults:
    def __init__(self, output_file_path, sentence_data_path):
        # Parse SMT output
        with open(output_file_path, "r") as f:
            results = f.read() + "\n"
        
        sat_or_unsat, counter_model = results.split("\n", 1)
        
        if "unsat" in sat_or_unsat:
            self.formula_type = "valid statement"
            self.counter_example = None
        else:
            self.formula_type = "logical fallacy"
            # Generate LLM interpretation
            self.counter_example = self._generate_interpretation(
                sentence_data, counter_model
            )

LLM-Based Interpretation

For logical fallacies, the system uses an LLM to generate natural language explanations:

1. Load Prompt Template

   Reads prompt_counter_example.txt containing instructions for interpretation.

2. Format Prompt

   Inserts claim, implication, entities, properties, formula, and counter-model.

3. Query LLM

   Sends the prompt to the LLM (via llm.py helper).

4. Return Explanation

   Returns human-readable explanation of why the argument fails.

Prompt Template

The interpretation prompt (in prompts/prompt_counter_example.txt) typically includes:

Given the following logical argument:

Claim: {claim}
Implication: {implication}
Referring Expressions: {referring_expressions}
Properties: {properties}
Formula: {formula}

The SMT solver found a counter-model:
{counter_model}

Explain in natural language why this argument is fallacious 
and what the counter-model demonstrates.

Customize the prompt template to adjust the style and detail level of interpretations.

Usage Methods

Programmatic Usage

from interpret_smt_results import SMTResults

# Create interpreter
results = SMTResults(
    output_file_path="results/exp_smt/0_out.txt",
    sentence_data_path="results/exp_data/0.json"
)

# Get results with interpretation
results.get_results(get_interpretation=True)

# Access properties
print(results.formula_type)      # "valid statement" or "logical fallacy"
print(results.counter_example)   # LLM-generated explanation (or None)

Disable Interpretation

To check validity without generating explanations:

results.get_results(get_interpretation=False)
# Only prints: "The given statement is a logical fallacy"

Disabling interpretation speeds up batch processing but provides less insight into why arguments fail.

Counter-Model Analysis

The counter-model from the SMT solver shows:

Function Definitions: How predicates are interpreted

(define-fun Wealthy ((x!0 Entity)) Bool
  (ite (= x!0 a) true false))

Entity Assignments: Which entities satisfy which properties

Wealthy(a) = true
Happy(a) = false

Relationship Violations: Where the implication breaks down

Claim asserts: Wealthy(a)
Implication requires: Happy(a)
Counter-model shows: Wealthy(a) ∧ ¬Happy(a)

Understanding Fallacy Types

Common fallacy patterns revealed by counter-examples:

Hasty Generalization

Argument: “Some wealthy people are happy, therefore all wealthy people are happy.”

Counter-model: Shows a wealthy person who is not happy.

False Cause

Argument: “A happened before B, therefore A caused B.”

Counter-model: Shows A and B occurring without causal relationship.

Composition Fallacy

Argument: “Each part has property P, therefore the whole has property P.”

Counter-model: Shows parts with P but whole without P.

Batch Processing

For processing multiple results:

#!/bin/bash
# interpret_all.sh

RUN_NAME=$1
NUM_FILES=$2

for i in $(seq 0 $((NUM_FILES - 1))); do
  echo "Processing datapoint $i..."
  python3 src/interpret_smt_results.py \
    results/${RUN_NAME}_smt/${i}_out.txt \
    results/${RUN_NAME}_data/${i}.json \
    > results/${RUN_NAME}_interpretations/${i}.txt
done

Error Handling

Missing Files

try:
    results = SMTResults(output_path, data_path)
except FileNotFoundError as e:
    print(f"Error: File not found - {e}")

Malformed Output

try:
    sat_or_unsat, counter_model = results.split("\n", 1)
except ValueError:
    print("Error: SMT output format incorrect")

Invalid JSON

import json

try:
    with open(sentence_data_path) as f:
        data = json.load(f)
except json.JSONDecodeError:
    print("Error: Invalid JSON format")

LLM Configuration

The llm.py helper module typically supports:

def get_llm_result(prompt, model_type='gpt-4o'):
    # OpenAI API call
    # or local model inference
    pass

Configure your LLM provider:

• Set API keys in environment variables
• Adjust model selection for cost/quality tradeoff
• Modify temperature for interpretation creativity

LLM interpretations require API access (OpenAI) or local model setup. Ensure proper authentication and rate limiting.

Visualization

Extend the script to generate visual representations:

import graphviz

def visualize_counter_model(counter_model):
    dot = graphviz.Digraph()
    # Parse counter_model and create graph
    # ...
    return dot

Next Steps

After interpreting individual results:

1. Aggregate results across the dataset
2. Calculate evaluation metrics (accuracy, precision, recall, F1)
3. Analyze patterns in fallacy types
4. Refine FOL translation based on error analysis

See Evaluation Metrics for performance analysis.