Skip to main content

​
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

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

​
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.

Build docs developers (and LLMs) love

Get started for freeTalk to us