KBSpec: LLM-driven Formal Specification Generation with Evolving Domain Knowledge Base

• URL: http://arxiv.org/abs/2606.21339v1
• Date: Fri, 19 Jun 2026 11:37:00 GMT
• Title: KBSpec: LLM-driven Formal Specification Generation with Evolving Domain Knowledge Base
• Abstract summary: We propose KBSpec, which augments large language models (LLMs) with dual-source knowledge of formal specification language corpora.<n>Results show that KBSpec improves verification pass rates by 10-25% over state-of-the-art LLM-based approaches.
• Score: 9.796586560498026
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Automated formal specification generation is a key step towards program understanding and formal verification. Recently, due to the success of large language models (LLMs) in code generation, researchers have made early attempts to adopt LLMs for generating formal specifications. However, the lack of formal specification language corpora in the wild often makes LLMs fail to generate syntactically correct and semantically verifiable specifications. To mitigate this gap, we propose KBSpec, which augments LLMs with dual-source knowledge of formal specification language: external knowledge from official documentation, and internal knowledge distilled from verifier feedback on LLM-generated specifications. KBSpec maintains a self-evolving knowledge base that is continuously updated from successful generation and repair trajectories, without any LLM parameter tuning or labeled training data. We evaluate KBSpec on Java Modeling Language (JML) specification generation with three LLM backends, and results show that KBSpec improves verification pass rates by 10-25% over state-of-the-art LLM-based approaches, while producing the largest number of high-completeness specifications.

Related papers

• KARLA: Knowledge-base Augmented Retrieval for Language Models [12.509786917611125]
  We propose a new method that allows an LLM to automatically pull in factual knowledge from a knowledge base during token generation.<n>This means that (1)factual knowledge in the LLM output can be updated without retraining the LLM, (2)facts in the LLM output can be traced to the knowledge base for transparency and explainability, and (3)smaller models can achieve the same factual accuracy as larger models.
  arXiv  Detail & Related papers  (2026-06-25T09:44:40Z)
• An Empirical Study of LLM-Generated Specifications for VeriFast [7.58397933941565]
  Static verification tools can assure industrial scale software, but require significant human labor to write specifications.<n>Recent work applies large language models (LLMs) to generate code, tests, and proofs, including specifications for verifiers.<n>This paper thoroughly evaluates how well LLMs perform when prompted to generate specifications for verifying 303 C functions with the SL verifier VeriFast.
  arXiv  Detail & Related papers  (2026-06-25T00:50:43Z)
• Are LLMs Reliable Code Reviewers? Systematic Overcorrection in Requirement Conformance Judgement [8.059802912761919]
  We uncover a systematic failure of large language models (LLMs) in matching code to natural language requirements.<n>More detailed prompt design, particularly with those requiring explanations and proposed corrections, leads to higher misjudgment rates.<n>We propose a Fix-guided Verification Filter that treats the model proposed fix as executable counterfactual evidence.
  arXiv  Detail & Related papers  (2026-02-28T08:35:25Z)
• Aligning Requirement for Large Language Model's Code Generation [9.205909320363247]
  Specine is a novel specification alignment technique for large language models (LLMs) code generation.<n>Its key idea is to identify misaligned input specifications, lift LLM-perceived specifications, and align them to enhance the code generation performance of LLMs.<n>For example, Specine outperforms the most effective baseline, achieving an average improvement of 29.60% across all subjects in terms of Pass@1.
  arXiv  Detail & Related papers  (2025-09-01T09:56:13Z)
• SPARQL Query Generation with LLMs: Measuring the Impact of Training Data Memorization and Knowledge Injection [81.78173888579941]
  Large Language Models (LLMs) are considered a well-suited method to increase the quality of the question-answering functionality.<n>LLMs are trained on web data, where researchers have no control over whether the benchmark or the knowledge graph was already included in the training data.<n>This paper introduces a novel method that evaluates the quality of LLMs by generating a SPARQL query from a natural-language question.
  arXiv  Detail & Related papers  (2025-07-18T12:28:08Z)
• LightPROF: A Lightweight Reasoning Framework for Large Language Model on Knowledge Graph [57.382255728234064]
  Large Language Models (LLMs) have impressive capabilities in text understanding and zero-shot reasoning.<n> Knowledge Graphs (KGs) provide rich and reliable contextual information for the reasoning process of LLMs.<n>We propose a novel Lightweight and efficient Prompt learning-ReasOning Framework for KGQA (LightPROF)
  arXiv  Detail & Related papers  (2025-04-04T03:03:47Z)
• How Reliable are LLMs as Knowledge Bases? Re-thinking Facutality and Consistency [60.25969380388974]
  Large Language Models (LLMs) are increasingly explored as knowledge bases (KBs)<n>Current evaluation methods focus too narrowly on knowledge retention, overlooking other crucial criteria for reliable performance.<n>We propose new criteria and metrics to quantify factuality and consistency, leading to a final reliability score.
  arXiv  Detail & Related papers  (2024-07-18T15:20:18Z)
• FOFO: A Benchmark to Evaluate LLMs' Format-Following Capability [70.84333325049123]
  FoFo is a pioneering benchmark for evaluating large language models' (LLMs) ability to follow complex, domain-specific formats. This paper presents FoFo, a pioneering benchmark for evaluating large language models' (LLMs) ability to follow complex, domain-specific formats.
  arXiv  Detail & Related papers  (2024-02-28T19:23:27Z)
• If LLM Is the Wizard, Then Code Is the Wand: A Survey on How Code Empowers Large Language Models to Serve as Intelligent Agents [81.60906807941188]
  Large language models (LLMs) are trained on a combination of natural language and formal language (code) Code translates high-level goals into executable steps, featuring standard syntax, logical consistency, abstraction, and modularity.
  arXiv  Detail & Related papers  (2024-01-01T16:51:20Z)
• Supervised Knowledge Makes Large Language Models Better In-context Learners [94.89301696512776]
  Large Language Models (LLMs) exhibit emerging in-context learning abilities through prompt engineering. The challenge of improving the generalizability and factuality of LLMs in natural language understanding and question answering remains under-explored. We propose a framework that enhances the reliability of LLMs as it: 1) generalizes out-of-distribution data, 2) elucidates how LLMs benefit from discriminative models, and 3) minimizes hallucinations in generative tasks.
  arXiv  Detail & Related papers  (2023-12-26T07:24:46Z)
• Configuration Validation with Large Language Models [22.018488540410548]
  Large Language Models (LLMs) show promise in addressing some of the long-lasting limitations of ML-based configuration validation. We develop a generic LLM-based configuration validation framework, named Ciri. Ciri employs effective prompt engineering with few-shot learning based on both valid configuration and misconfiguration data.
  arXiv  Detail & Related papers  (2023-10-15T00:50:27Z)
• How Effective are Large Language Models in Generating Software Specifications? [14.170320751508502]
  Large Language Models (LLMs) have been successfully applied to numerous Software Engineering (SE) tasks.<n>We conduct the first empirical study to evaluate the capabilities of LLMs for generating software specifications from software comments or documentation.
  arXiv  Detail & Related papers  (2023-06-06T00:28:39Z)
• Augmented Large Language Models with Parametric Knowledge Guiding [72.71468058502228]
  Large Language Models (LLMs) have significantly advanced natural language processing (NLP) with their impressive language understanding and generation capabilities. Their performance may be suboptimal for domain-specific tasks that require specialized knowledge due to limited exposure to the related data. We propose the novel Parametric Knowledge Guiding (PKG) framework, which equips LLMs with a knowledge-guiding module to access relevant knowledge.
  arXiv  Detail & Related papers  (2023-05-08T15:05:16Z)

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.