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

• URL: http://arxiv.org/abs/2606.16886v1
• Date: Mon, 15 Jun 2026 15:59:10 GMT
• Title: Neuro-Symbolic Software Verification: Hyper-charging Local Language Models with Symbolic Reasoning at Scale
• Abstract summary: We present VerIbmc, a neuro-symbolic pipeline that pairs symbolic invariant generation with locally deployable open-weight language models.<n>All inference runs entirely on a single local machine using open-weight models -- no cloud API or proprietary model is required.
• Score: 11.088680803534785
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Loop invariant synthesis remains a central and pivotal bottleneck in formal software verification. Recent LLM-based Neuro-Symbolic tools have achieved impressive solve rates. However, these tools rely on proprietary, often expensive cloud APIs, which constitute a hurdle for privacy-sensitive industrial deployments where the source code cannot leave the organisation or where cost is a factor. We present VerIbmc, a neuro-symbolic pipeline that pairs symbolic invariant generation with locally deployable open-weight language models with the ESBMC verification tool. Our pipeline combines a deterministic symbolic invariant synthesis phase with an iterative LLM refinement loop driven by structured verifier feedback. In addition, we provide two types of pipelines that differ in their prompting strategy: Chain-of-Thought vs. Tree-of-Thought. We conduct an extensive experimental evaluation with five open-weight models (ranging from 7B to 120B parameters) across five benchmark families comprising of 520 problems (499 after excluding 21 with unavoidable overflow). Overall, the best single configuration (GPT-OSS-120B) solves 431 of 499 problems (86.4%). Additionally, on the four benchmark suites shared with the strongest cloud-API tools, VerIbmc is competitive running only on a single local machine. The evaluation shows symbolic invariant synthesis solves 75 problems without any LLM call and yields up to +35 additional problems for the weakest model. Importantly, all inference runs entirely on a single local machine using open-weight models -- no cloud API or proprietary model is required. Overall, we demonstrate that a neuro-symbolic approach based on LLMs can be used effectively for invariant synthesis in a privacy-preserving and energy-efficient manner, without having to resort to expensive proprietary frontier models locked behind APIs.

Related papers

• Can LLMs Use Relational Transformer Embeddings? [0.0]
  Injecting frozen-encoder embeddings as soft tokens into a large language model (LLM) is a conceptually appealing fusion strategy.<n>We test this hypothesis by injecting LLMs from a frozen Transformer (RT) into Qwen3.<n>We report negative results and analyze the failure modes, arguing that soft-token fusion requires stronger alignment objectives and schema-aware design before it can serve as a route to prediction.
  arXiv  Detail & Related papers  (2026-08-31T22:51:21Z)
• Environment-free Synthetic Data Generation for API-Calling Agents [68.95520739708304]
  Training API-calling large language model (LLM) agents demands massive amounts of high-quality trajectories.<n>We propose an environment-free synthetic data generation approach that leverages LLMs as on-the-fly digital world models.<n>We evaluate our approach on the challenging AppWorld and OfficeBench benchmarks, which include both information-retrieval and state-changing tasks.
  arXiv  Detail & Related papers  (2026-07-18T17:36:44Z)
• Knowledge Boundary Probing and Demand-Guided Intervention for LLM-Based Power System Code Generation [8.136015158683694]
  We show that first-pass failures in power-system code generation are dominated by structured API-knowledge boundary: hallucinated function names, misused parameters, and mishandled result tables.<n>We introduce PowerCodeBench, an execution-validated benchmark generator that pairs natural-language operator queries with pandapower code and numerical ground truth.<n>We also introduce an L0-L3 documentation-driven probing procedure that measures per-model API knowledge profiles.
  arXiv  Detail & Related papers  (2026-05-29T16:06:34Z)
• Controllable and Verifiable Tool-Use Data Synthesis for Agentic Reinforcement Learning [82.89535601592739]
  We propose a two-stage pipeline that generates reliable base tool-use trajectories through self-evolving synthesis with multi-level validation.<n>These augmentations introduce distractor tools, indirect or ambiguous user queries, and noisy, multi-format, or erroneous tool outputs.<n>This design enables automatic reward computation via reference matching for standard cases and lightweight judge-assisted verification for special behaviors such as error detection.
  arXiv  Detail & Related papers  (2026-04-10T18:38:52Z)
• Resource-Efficient Iterative LLM-Based NAS with Feedback Memory [49.44875022114861]
  Neural Architecture Search (NAS) automates network design, but conventional methods demand substantial computational resources.<n>We propose a closed-loop pipeline leveraging large language models (LLMs) to iteratively generate, evaluate, and refine convolutional neural network architectures.
  arXiv  Detail & Related papers  (2026-03-12T16:00:22Z)
• Cost-Aware Model Selection for Text Classification: Multi-Objective Trade-offs Between Fine-Tuned Encoders and LLM Prompting in Production [0.0]
  Large language models (LLMs) have demonstrated strong capabilities in open-ended reasoning and generative language tasks.<n>For structured text classification problems with fixed label spaces, model selection is often driven by predictive performance alone.<n>We show that fine-tuned encoder-based models from the BERT family achieve competitive, and often superior, classification performance.
  arXiv  Detail & Related papers  (2026-02-06T03:54:28Z)
• Framework-Aware Code Generation with API Knowledge Graph-Constructed Data: A Study on HarmonyOS [52.483888557864326]
  APIKG4SYN is a framework designed to exploit API knowledge graphs for the construction of API-oriented question-code pairs.<n>We build the first benchmark for HarmonyOS code generation using APIKG4SYN.
  arXiv  Detail & Related papers  (2025-11-29T08:13:54Z)
• Scaling LLM Speculative Decoding: Non-Autoregressive Forecasting in Large-Batch Scenarios [76.85739138203014]
  We present SpecFormer, a novel architecture that accelerates unidirectional and attention mechanisms.<n>We demonstrate that SpecFormer achieves lower training demands and reduced computational costs.
  arXiv  Detail & Related papers  (2025-11-25T14:20:08Z)
• Semantic Agreement Enables Efficient Open-Ended LLM Cascades [18.119677655287607]
  Cascade systems route computational requests to smaller models when possible and defer to larger models only when necessary.<n>We propose semantic agreement as a training-free signal for reliable deferral.<n>We find that semantic cascades match or surpass target-model quality at 40% of the cost and reduce latency by up to 60%.
  arXiv  Detail & Related papers  (2025-09-26T03:51:28Z)
• Syntactic and Semantic Control of Large Language Models via Sequential Monte Carlo [90.78001821963008]
  A wide range of LM applications require generating text that conforms to syntactic or semantic constraints.<n>We develop an architecture for controlled LM generation based on sequential Monte Carlo (SMC)<n>Our system builds on the framework of Lew et al. (2023) and integrates with its language model probabilistic programming language.
  arXiv  Detail & Related papers  (2025-04-17T17:49:40Z)
• Are You Getting What You Pay For? Auditing Model Substitution in LLM APIs [71.7892165868749]
  Commercial Large Language Model (LLM) APIs create a fundamental trust problem.<n>Users pay for specific models but have no guarantee that providers deliver them faithfully.<n>We formalize this model substitution problem and evaluate detection methods under realistic adversarial conditions.<n>We propose and evaluate the use of Trusted Execution Environments (TEEs) as one practical and robust solution.
  arXiv  Detail & Related papers  (2025-04-07T03:57:41Z)
• LLMC: Benchmarking Large Language Model Quantization with a Versatile Compression Toolkit [55.73370804397226]
  Quantization, a key compression technique, can effectively mitigate these demands by compressing and accelerating large language models. We present LLMC, a plug-and-play compression toolkit, to fairly and systematically explore the impact of quantization. Powered by this versatile toolkit, our benchmark covers three key aspects: calibration data, algorithms (three strategies), and data formats.
  arXiv  Detail & Related papers  (2024-05-09T11:49:05Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.