LLM Integration

Introduction

The LLM module (arlib/llm) integrates large language models into automated reasoning workflows, enabling natural language interfaces, LLM-guided solving strategies, and reasoning about programs with unspecified components.

Key Features

  • Natural Language to SMT: Convert natural language constraints to SMT formulas

  • SMTO (SMT + Oracles): Solve constraints with LLM-based oracle components

  • LLM-Guided Abduction: Generate explanations using language models

  • Interpolant Generation: Synthesize interpolants with LLM assistance

  • UNSAT Core Analysis: Minimal unsatisfiable core extraction with explanations

Components

Natural Language Translation (arlib/llm/nl2smt.py, arlib/llm/smt2nl.py)

Bidirectional translation between natural language and SMT-LIB:

from arlib.llm import nl_to_smt, smt_to_nl

# Convert natural language to SMT
formula = nl_to_smt("x is greater than 5 and less than 10")

# Convert SMT to natural language description
description = smt_to_nl(smt_formula)

SMTO: SMT with Oracles (arlib/llm/smto)

Satisfiability Modulo Theories and Oracles for reasoning about programs with unspecified components:

from arlib.llm.smto import OraxSolver, OracleInfo
import z3

# Initialize solver
solver = OraxSolver(provider="openai", model="gpt-4")

# Register blackbox oracle with examples
oracle = OracleInfo(
    name="check_password",
    input_types=[z3.StringSort()],
    output_type=z3.BoolSort(),
    description="Validate password strength",
    examples=[
        {"input": {"arg0": "weak"}, "output": "false"},
        {"input": {"arg0": "Str0ng!Pass"}, "output": "true"}
    ]
)
solver.register_oracle(oracle)

# Solve constraints
password = z3.String('password')
check_pw = z3.Function('check_password', z3.StringSort(), z3.BoolSort())
solver.add_constraint(check_pw(password) == True)
model = solver.check()

Whitebox Mode: Enhanced analysis with source code or documentation:

from arlib.llm.smto import WhiteboxOracleInfo, OracleAnalysisMode

oracle = WhiteboxOracleInfo(
    name="oracle_func",
    analysis_mode=OracleAnalysisMode.SOURCE_CODE,
    source_code="def oracle_func(x): return x > 0 and x < 100"
)

LLM-Guided Abduction (arlib/llm/abduct)

Generate explanatory hypotheses for observations:

from arlib.llm.abduct import LLMAbductor

abductor = LLMAbductor()
explanation = abductor.abduce(
    background_theory=theory,
    observation=observation
)

LLM Interpolant Generation (arlib/llm/interpolant)

Synthesize Craig interpolants using language models:

from arlib.llm.interpolant import LLMInterpolant

interpolant = LLMInterpolant().generate(formula_a, formula_b)

LLM Tools (arlib/llm/llmtool)

Utilities for LLM integration:

  • Multi-provider support (OpenAI, Anthropic, local models)

  • Prompt engineering utilities

  • Response parsing and validation

  • Caching and rate limiting

Applications

  • Natural language specification to formal constraints

  • Reasoning about third-party libraries without specifications

  • LLM-guided solver heuristics and strategy selection

  • Automated explanation generation for verification results

  • Interactive constraint debugging with natural language

References