💻 computer science

Neuro-Symbolic Software Verification: Hyper-charging Local Language Models with Symbolic Reasoning at Scale

This paper introduces VerIbmc, a neuro-symbolic pipeline that leverages local open-weight language models combined with symbolic invariant synthesis and iterative verifier feedback to achieve state-of-the-art loop invariant generation for software verification, offering a privacy-preserving and cost-effective alternative to proprietary cloud-based tools.

Original authors: Muhammad A. A. Pirzada, Julian Parsert, Weiqi Wang, Konstantin Korovin, Lucas C. Cordeiro

Published 2026-06-16

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Muhammad A. A. Pirzada, Julian Parsert, Weiqi Wang, Konstantin Korovin, Lucas C. Cordeiro

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are trying to prove that a complex machine (a computer program) will never break, no matter how many times you run it. The hardest part of this proof is understanding the machine's "loops"—parts where it repeats a task over and over. To prove the machine is safe, you need to find a Loop Invariant.

Think of a Loop Invariant like a "safety rule" that must be true every single time the machine starts a new cycle of its loop. For example, if a loop counts down from 10 to 0, the safety rule might be: "The number is always between 0 and 10." If you can prove this rule holds true at the start, stays true after every step, and leads to a safe finish, the whole machine is proven safe.

The problem is that finding these rules automatically is incredibly hard. It's like trying to guess the secret combination to a safe without any clues.

The Old Way vs. The New Way

The Old Way (Symbolic Reasoning):
Traditionally, computers tried to find these rules using strict math and logic. It's like a super-precise accountant checking every single number. It's very reliable, but it's slow and often gets stuck on complex, messy problems. It's like trying to solve a maze by checking every single wall one by one.

The "Cloud" Way (Big AI Models):
Recently, people started using massive Artificial Intelligence (AI) models to guess these rules. These AIs are like brilliant, well-read students who have read millions of code examples. They can guess the right rule very quickly. However, to use them, you usually have to send your code to a giant, expensive cloud server (like sending your secret blueprints to a stranger). This is bad for companies that need to keep their code private, and it costs a lot of money.

The Solution: VerIbmc (The Local "Super-Helper")

The authors of this paper built a new system called VerIbmc. Think of it as a local workshop where you can use a smart AI assistant without ever leaving your building.

Here is how VerIbmc works, using a simple analogy:

Imagine you are trying to solve a difficult puzzle (the loop invariant).

The Deterministic Detective (Phase 0 & 1): Before asking the AI for help, VerIbmc sends a strict, logical detective (a tool called ESBMC) to look at the puzzle. The detective checks simple facts first. If the puzzle is easy, the detective solves it instantly. If the detective finds a few solid clues (like "the number is always positive"), they write them down on a whiteboard.
The Local AI Assistant (Phase 2): If the detective gets stuck, they call in the Local AI Assistant. But here's the trick: the AI doesn't start from scratch. The detective hands the AI the whiteboard with the clues they already found.
The Feedback Loop: The AI guesses a full solution. The detective checks it.
- If it's wrong, the detective doesn't just say "No." They say, "This part is wrong, but this other part is actually correct." They take the correct part, write it on the whiteboard, and ask the AI to try again, using the new clues.
- This happens over and over until the puzzle is solved or they run out of time.

Two Ways to Think (CoT vs. ToT)

The paper also tested how the AI should "think" while solving the puzzle:

Chain-of-Thought (CoT): The AI thinks in a straight line, step-by-step, like writing a single story.
Tree-of-Thoughts (ToT): The AI branches out, like a tree. It tries a few different paths at once, sees which one looks promising, and then focuses its energy on the best paths. The paper found that for the strongest AI models, this branching method was great, but for smaller, weaker models, it sometimes wasted time.

The Results: Why This Matters

The researchers tested this system on hundreds of different programming puzzles using five different "open-weight" AI models (models that anyone can download and run on their own computers).

Privacy First: Because everything runs on a local machine, no code ever leaves the organization. It's like doing your math homework in your own room instead of handing it to a stranger.
Cost Effective: You don't need to pay expensive fees to big cloud companies.
Performance: The best setup (using a large local model called GPT-OSS-120B) solved 86.4% of the problems. This is better than many traditional tools and competitive with the expensive cloud-based AI tools.
The "Free" Boost: The system found that the "Detective" phase (the symbolic part) solved 75 problems all by itself without needing the AI at all. For weaker AI models, the detective's clues helped them solve 35 more problems than they could have solved alone.

The Bottom Line

VerIbmc proves that you don't need expensive, privacy-invading cloud supercomputers to verify software safety. By combining a strict logical detective with a smart, local AI assistant that learns from its mistakes, you can get top-tier results right on your own computer. It's a way to make software verification private, affordable, and powerful.

Technical Summary: Neuro-Symbolic Software Verification with VerIbmc

Problem Statement

Loop invariant synthesis remains a central bottleneck in formal software verification. While symbolic techniques (e.g., abstract interpretation, constraint solving) and data-driven "guess-and-check" methods exist, they often struggle with scalability, expressiveness, or the diversity of real-world code. Recently, Large Language Models (LLMs) have shown promise in generating candidate invariants by leveraging learned patterns from code corpora. However, existing neuro-symbolic approaches typically rely on proprietary, closed models accessed via external cloud APIs. This reliance introduces significant hurdles for industrial deployment:

Privacy and Compliance: Source code must be transmitted to third-party services, raising confidentiality concerns.
Reproducibility: Dependence on external providers complicates integration into controlled verification pipelines.
Cost and Sustainability: Large-scale models are computationally expensive and energy-intensive, limiting their practicality for continuous verification workflows.

The authors posit that these challenges necessitate a shift toward locally deployable, open-weight language models that can operate entirely within an organization's infrastructure without exposing proprietary code.

Methodology: The VerIbmc Pipeline

The paper presents VerIbmc, a neuro-symbolic pipeline designed to synthesize loop invariants for C programs by pairing symbolic reasoning with locally hosted open-weight LLMs. The system uses ESBMC (Efficient SMT-Based Context-Bounded Model Checker) as the verification oracle. The pipeline is designed on the principle of "escalate only when necessary," prioritizing cheap, deterministic symbolic reasoning before invoking the LLM.

Core Architecture

The pipeline operates in three distinct phases:

Phase 0 (Baseline Verification): ESBMC verifies the unannotated program. If the program is trivially safe or provably unsafe, the process terminates immediately, avoiding unnecessary synthesis effort.
Phase 1 (Symbolic Candidate Generation): If Phase 0 returns "Unknown," the system symbolically enumerates atomic candidate invariants by pairwise comparison of loop-entry variables and constants. These atoms are verified for inductivity using ESBMC. The system maintains three stores: Provable ( $P$ ), Disprovable ( $D$ ), and Unknown ( $U$ ). If the conjunction of all provable atoms suffices to prove the post-condition, the pipeline terminates successfully without any LLM call.
Phase 2 (LLM Refinement Loop): If the symbolic phase is insufficient, the pipeline enters an iterative loop where an LLM is prompted to generate new invariants.
- Feedback Mechanism: The LLM receives the current program, the contents of the $P$ , $D$ , and $U$ stores as structured feedback, and few-shot examples.
- Decomposition and Recombination: When an LLM-generated candidate fails verification, the system decomposes it into sub-formulas (atoms). Atoms are individually verified and added to the appropriate stores. The conjunction of all currently provable atoms is then re-verified. This allows the system to salvage useful components of failed LLM proposals.
- Termination: The loop continues until a valid invariant is found, the iteration budget is exhausted, or a timeout occurs.

Inference Strategies

The authors evaluate four inference strategies based on two design axes:

Verifier Feedback (Symbolic Prior):
- Basic: Runs the full three-phase pipeline, utilizing the symbolic prior from Phase 1 and atom-level filtering.
- LLM-Only: Skips Phase 1 and atom-level decomposition, relying solely on the LLM to generate inductive invariants as a whole. This serves as an ablation baseline.
Reasoning Structure:
- Chain-of-Thought (CoT): Uses standard prompting with step-by-step reasoning examples (Inductive, Hoare Logic, Horn Clause, or direct derivation).
- Tree-of-Thoughts (ToT): Explores multiple derivation styles in parallel during a "scouting" stage, scores them based on the number of provable atoms generated, and concentrates the remaining iteration budget on the top-two performing styles.

Key Contributions

Neuro-Symbolic Pipeline: A complete system integrating locally served open-weight LLMs with ESBMC for automated loop invariant synthesis, operating entirely on internal infrastructure.
Systematic Evaluation of Strategies: A comprehensive comparison of pure LLM, symbolic-guided, and Tree-of-Thoughts (ToT) variants, demonstrating the impact of symbolic feedback and reasoning structures.
Symbolic Feedback Gains: Demonstration that providing provable invariant atoms as context to the LLM yields consistent gains, particularly for weaker models (e.g., Llama-3.1-8B gains +35 solved benchmarks over a pure-LLM baseline).
Prompt Engineering Analysis: Evaluation of different prompting styles (CoT vs. ToT) and reasoning templates (Inductive, Hoare Logic, Horn Clause) on invariant synthesis.
Large-Scale Benchmarking: An extensive evaluation across five open-weight models (7B to 120B parameters), four inference strategies, and five benchmark families (520 problems, 499 effective), totaling 10,400 per-problem outcomes.

Experimental Results

The evaluation was conducted on a server with four NVIDIA RTX A6000 GPUs using five open-weight models: GPT-OSS-120B, GPT-OSS-20B, Qwen2.5-32B, Qwen2.5-7B, and Llama-3.1-8B.

Overall Performance: The best single configuration (GPT-OSS-120B with the Basic strategy) solved 431 out of 499 problems (86.4%).
Comparison with State-of-the-Art (SOTA):
- VerIbmc substantially outperforms traditional symbolic tools (CPA-Checker, 2ls, ESBMC-Kind) and neural-only tools (Code2Inv) when run on the same local hardware.
- On shared benchmark suites, VerIbmc is competitive with or slightly below the strongest LLM-augmented tools (Clause2Inv, LaM4Inv, LORIS) that rely on expensive external APIs (e.g., GPT-4). Notably, VerIbmc achieves these results without transmitting code to the cloud.
- VerIbmc uniquely scales to the full SV-COMP benchmark set (154 problems), including programs with arrays, nested loops, and pointers, which many competing tools cannot express due to frontend limitations.
Impact of Symbolic Phase: The symbolic Phase 1 solved 75 problems without any LLM call. For weaker models, the symbolic augmentation provided significant boosts (up to +35 additional solved problems for Llama-3.1-8B).
ToT vs. CoT: ToT prompting showed a diversity-accuracy trade-off. While it reached unique problem-model pairs inaccessible to CoT, it often incurred a wall-clock overhead and, for weaker models, resulted in a net decrease in solved problems due to iteration budget exhaustion. For the strongest models (GPT-OSS-120B), the performance difference between CoT and ToT was negligible.
Model Capability: The results indicate that model capability is the primary driver of accuracy. The gap between the strongest and weakest models was significantly larger than the performance variance introduced by changing strategies within the same model.

Significance and Claims

The paper claims that VerIbmc demonstrates that a neuro-symbolic approach based on LLMs can be effectively applied to invariant synthesis in a privacy-preserving and energy-efficient manner. By operating entirely on local infrastructure with open-weight models, the approach eliminates the need for expensive proprietary frontier models locked behind APIs.

The authors emphasize that their method is sound by construction: every candidate invariant is discharged by a formal verifier (ESBMC) before acceptance. While the system is incomplete due to the undecidability of the problem, it provides a practical, scalable, and reproducible pathway for AI-assisted formal verification of production software. The work takes a step toward industry-ready verification pipelines where data privacy and resource efficiency are critical requirements.