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 aria.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 aria.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 aria.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 aria.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 aria.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 aria.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 aria.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 aria.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 aria.efmc.llmtools.llm_tool.LLMTool(model_name: str, temperature: float, language: str, max_query_num: int, logger: Logger)[source]
Bases:
ABCAbstract 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 aria.efmc.llmtools.llm_tool.LLMToolInput[source]
Bases:
ABCAbstract base class for LLM tool input.
- class aria.efmc.llmtools.llm_tool.LLMToolOutput[source]
Bases:
ABCAbstract base class for LLM tool output.
LLM utilities for online inference using various LLM providers.
- class aria.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:
objectAn 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
- Calling local LLMs
vLLM
sglang
LMStudio
Tingly OpenAI proxy (set TINGLY_API_KEY)
- class aria.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: str | None = None, api_key: str | None = None, max_retries: int = 3)[source]
Bases:
objectLocal 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)
- class aria.efmc.llmtools.llm_local.SimpleLogger(log_level=20)[source]
Bases:
objectSimple logger interface for local LLM.
Logger module for EFMC LLM tools.