LLM Tools¶

The llmtools module provides utilities for integrating Large Language Models (LLMs) into the verification pipeline. This is primarily used by the LLM4Inv engine for generating candidate invariants.

Architecture¶

The module follows an abstract base class pattern:

efmc/llmtools/
├── llm_tool.py      # Abstract base classes
├── llm_utils.py     # LLM wrapper and utilities
├── llm_local.py     # Local model support
├── llm_opencode.py  # OpenCode API integration
├── logger.py        # Logging utilities
└── test_llm.py      # Test utilities

LLMTool Base Classes¶

LLMToolInput¶

Abstract base class for LLM tool inputs.

from efmc.llmtools.llm_tool import LLMToolInput

class MyToolInput(LLMToolInput):
    def __init__(self, program: str, property: str):
        self.program = program
        self.property = property

    def __hash__(self):
        return hash((self.program, self.property))

LLMToolOutput¶

Abstract base class for LLM tool outputs.

from efmc.llmtools.llm_tool import LLMToolOutput

class MyToolOutput(LLMToolOutput):
    def __init__(self, candidates: List[str]):
        self.candidates = candidates

LLMTool¶

Abstract base class for LLM-based tools.

from efmc.llmtools.llm_tool import LLMTool

class MyLLMTool(LLMTool):
    def _get_prompt(self, tool_input: MyToolInput) -> str:
        # Generate prompt from input
        return f"Generate invariants for:\n{tool_input.program}"

    def _parse_response(self, response: str, tool_input: MyToolInput) -> MyToolOutput:
        # Parse LLM response
        return MyToolOutput(candidates=response.split("\n"))

LLM Utilities¶

The llm_utils module provides the core LLM interface:

from efmc.llmtools.llm_utils import LLM

# Initialize LLM
llm = LLM(
    model_name="qwen/qwen3-coder-30b",
    logger=my_logger,
    temperature=0.1
)

# Query the model
response, input_tokens, output_tokens = llm.infer(
    prompt="Generate an invariant for x >= 0",
    verbose=True
)

LLM Providers¶

Local Models¶

Support for locally hosted models via various backends:

from efmc.llmtools.llm_local import LocalLLM

# LM Studio
local_llm = LocalLLM(
    provider="lm-studio",
    model="qwen/qwen3-coder-30b"
)

# vLLM
local_llm = LocalLLM(
    provider="vllm",
    model="meta-llama/Llama-2-7b-chat-hf"
)

# SGLang
local_llm = LocalLLM(
    provider="sglang",
    model="deepseek-ai/DeepSeek-V2"
)

Remote Models¶

Support for remote API providers:

from efmc.llmtools.llm_opencode import OpenCodeLLM

remote_llm = OpenCodeLLM(
    model="deepseek-v3",
    api_key="your-api-key"
)

Logging¶

The logger module provides structured logging for LLM interactions:

from efmc.llmtools.logger import Logger

logger = Logger(
    log_file="llm.log",
    console_log=True,
    level="INFO"
)

logger.print_console("Starting LLM inference...")
logger.print_log("Prompt:", prompt)
logger.print_log("Response:", response)

Usage in LLM4Inv¶

The LLM4Inv engine uses these utilities to generate candidate invariants:

from efmc.engines.llm4inv import LLM4InvProver

prover = LLM4InvProver(
    transition_system=sts,
    max_candidates=5,
    provider="local",
    model="qwen/qwen3-coder-30b"
)

result = prover.solve()

Configuration¶

LLM behavior can be configured via command-line arguments:

efmc --file program.smt2 --engine llm4inv \
    --llm4inv-provider local \
    --llm4inv-local-provider lm-studio \
    --llm4inv-local-model qwen/qwen3-coder-30b \
    --llm4inv-temperature 0.1 \
    --llm4inv-max-candidates-per-iter 5 \
    --llm4inv-max-iterations 10

API Reference¶

LLM Tool base classes for implementing LLM-based tools.

class efmc.llmtools.llm_tool.LLMTool(model_name: str, temperature: float, language: str, max_query_num: int, logger: Logger)[source]¶

Bases: ABC

Abstract base class for LLM-based tools.

invoke(tool_input: LLMToolInput) → LLMToolOutput[source]¶

Invoke the LLM tool with given input.

Parameters:: tool_input – Input to the LLM tool
Returns:: Output from the LLM tool

class efmc.llmtools.llm_tool.LLMToolInput[source]¶

Bases: ABC

Abstract base class for LLM tool input.

class efmc.llmtools.llm_tool.LLMToolOutput[source]¶

Bases: ABC

Abstract base class for LLM tool output.

LLM utilities for online inference using various LLM providers.

class efmc.llmtools.llm_utils.LLM(online_model_name: str, logger: Logger, temperature: float = 0.0, system_role: str = 'You are a experienced programmer and good at understanding programs written in mainstream programming languages.')[source]¶

Bases: object

An online inference model using different LLMs: - DeepSeek: V3, R1 (uses OpenAI-compatible API) - GLM: Zhipu AI models

infer(message: str, is_measure_cost: bool = False) → Tuple[str, int, int][source]¶

Infer using the online model.

Parameters:

message – Input message
is_measure_cost – Whether to measure token cost

Returns:

Tuple of (output, input_token_cost, output_token_cost)

infer_with_deepseek_model(message)[source]¶

Infer using the DeepSeek model (V3, R1, etc.) DeepSeek uses OpenAI-compatible API format

Parameters:: message – Input message
Returns:: Model output or empty string on failure

infer_with_glm_model(message)[source]¶

Infer using the GLM model.

Parameters:: message – Input message
Returns:: Model output or empty string on failure

run_with_timeout(func, timeout_seconds)[source]¶

Run a function with timeout that works in multiple threads.

Parameters:

func – Function to execute
timeout_seconds – Timeout in seconds

Returns:

Function result or empty string on timeout/error

Calling local LLMs

vLLM
sglang
LMStudio
Tingly OpenAI proxy (set TINGLY_API_KEY)

class efmc.llmtools.llm_local.LLMLocal(offline_model_name: str, logger: SimpleLogger, temperature: float = 0.0, system_role: str = 'You are an experienced programmer and good at understanding programs written in mainstream programming languages.', max_output_length: int = 4096, measure_cost: bool = False, provider: str = 'lm-studio', base_url: Optional[str] = None, api_key: Optional[str] = None, max_retries: int = 3)[source]¶

Bases: object

Local LLM inference class for offline models.

infer(message: str, is_measure_cost: bool = False) → Tuple[str, int, int][source]¶

Infer using the local model.

Parameters:

message – Input message
is_measure_cost – Whether to measure token cost

Returns:

Tuple of (output, input_token_cost, output_token_cost)

infer_with_openai_compatible_model(message)[source]¶

Infer using an OpenAI-compatible API endpoint.

Parameters:: message – Input message
Returns:: Model output or empty string on failure

run_with_timeout(func, timeout_seconds)[source]¶

Run a function with timeout that works in multiple threads.

Parameters:

func – Function to execute
timeout_seconds – Timeout in seconds

Returns:

Function result or empty string on timeout/error

class efmc.llmtools.llm_local.SimpleLogger(log_level=20)[source]¶

Bases: object

Simple logger interface for local LLM.

print_console(*args: Any) → None[source]¶: Print console message.

print_log(*args: Any) → None[source]¶: Print log message.

Logger module for EFMC LLM tools.

class efmc.llmtools.logger.Logger(log_file_path: str, log_level=20)[source]¶

Bases: object

print_console(*args: Any) → None[source]¶

Output messages to both console and log file.

Parameters:: *args – Message parts to be logged, which are merged into a single string.

print_log(*args: Any) → None[source]¶

Output messages to log file only.

Parameters:: *args – Message parts to be logged, which are merged into a single string.

LLM Tools¶

Architecture¶

LLMTool Base Classes¶

LLMToolInput¶

LLMToolOutput¶

LLMTool¶

LLM Utilities¶

LLM Providers¶

Local Models¶

Remote Models¶

Logging¶

Usage in LLM4Inv¶

Configuration¶

API Reference¶

Table of Contents

Previous topic

Next topic

This Page