LLM-based Satisfiability Checking of String Requirements by Consistent Data and Checker Generation

• URL: http://arxiv.org/abs/2506.16639v1
• Date: Thu, 19 Jun 2025 22:41:43 GMT
• Title: LLM-based Satisfiability Checking of String Requirements by Consistent Data and Checker Generation
• Abstract summary: Large language models (LLMs) have emerged as an alternative approach for formal reasoning tasks.<n>In this paper, we introduce a hybrid approach that verifies the satisfiability of NL requirements over strings.<n>LLMs effectively translate natural language into checkers, even achieving perfect testing accuracy for Python-based checkers.
• Score: 2.892899073587433
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Requirements over strings, commonly represented using natural language (NL), are particularly relevant for software systems due to their heavy reliance on string data manipulation. While individual requirements can usually be analyzed manually, verifying properties (e.g., satisfiability) over sets of NL requirements is particularly challenging. Formal approaches (e.g., SMT solvers) may efficiently verify such properties, but are known to have theoretical limitations. Additionally, the translation of NL requirements into formal constraints typically requires significant manual effort. Recently, large language models (LLMs) have emerged as an alternative approach for formal reasoning tasks, but their effectiveness in verifying requirements over strings is less studied. In this paper, we introduce a hybrid approach that verifies the satisfiability of NL requirements over strings by using LLMs (1) to derive a satisfiability outcome (and a consistent string, if possible), and (2) to generate declarative (i.e., SMT) and imperative (i.e., Python) checkers, used to validate the correctness of (1). In our experiments, we assess the performance of four LLMs. Results show that LLMs effectively translate natural language into checkers, even achieving perfect testing accuracy for Python-based checkers. These checkers substantially help LLMs in generating a consistent string and accurately identifying unsatisfiable requirements, leading to more than doubled generation success rate and F1-score in certain cases compared to baselines without generated checkers.

Related papers

• ClarifyCodeBench: Evaluating LLMs on Clarifying Ambiguous Requirements for Code Generation [54.788849448970154]
  We introduce ClarifyCodeBench, a novel interactive benchmark for evaluating Large Language Models' capability in resolving requirement ambiguity.<n>We conduct a systematic evaluation of six state-of-the-art LLMs using ClarifyCodeBench.<n>Our empirical results yield three critical insights: 1) Capability Decoupling: Strong code generation performance does not inherently translate to effective requirement clarification; 2) The Reasoning Paradox: While increased computational thinking enhances code correctness, it yields marginal gains in identifying ambiguities.
  arXiv  Detail & Related papers  (2026-07-01T09:58:59Z)
• Teaching Language Models to Check Grounded Claim Factuality with Human Test-Taking Strategies [0.9867902290081937]
  Grounded claim factuality checking is important for large language model (LLM) applications such as retrieval-augmented generation.<n>We address this by formulating grounded claim factuality checking as a true/false reading comprehension task.<n>Our method reduces token usage by over 80% compared to unguided open-ended reasoning.
  arXiv  Detail & Related papers  (2026-05-28T10:11:42Z)
• LLM-Based Static Verification of Code Against Natural-Language Requirements: An Industrial Experience Report [3.5867640049033054]
  This article presents a two-stage LLM-based workflow for addressing this challenge in an intelligent-vehicle cybersecurity case study.<n>In the first stage, an AI-based rule miner extracts verifiable rules from natural-language requirements.<n>In the second stage, an AI-based code auditor checks implementation evidence against the extracted rules.
  arXiv  Detail & Related papers  (2026-05-18T06:34:03Z)
• Assessing the Impact of Requirement Ambiguity on LLM-based Function-Level Code Generation [14.755517753769837]
  We introduce Orchid, the first code generation benchmark specifically designed with ambiguous requirements.<n>It comprises 1,304 function-level tasks covering four distinct types of ambiguity: lexical, syntactic, semantic, and vagueness.<n>Our results demonstrate that ambiguity consistently degrades the performance of all evaluated LLMs, with the most pronounced negative effects observed in highly advanced models.
  arXiv  Detail & Related papers  (2026-04-23T10:07:33Z)
• Syntax Is Easy, Semantics Is Hard: Evaluating LLMs for LTL Translation [14.34799644541222]
  Linear Temporal Logic is a popular formalism for specifying desirable requirements and security and privacy policies for software, networks, and systems.<n>Since many security and privacy analysis tools require formulas as input, this difficulty places them out of reach for many developers and analysts.<n>This paper evaluates that premise by assessing how effectively several representative LLMs translate English sentences into Proposition formulas.
  arXiv  Detail & Related papers  (2026-04-08T17:36:33Z)
• 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)
• Do Large Language Models Understand Data Visualization Rules? [2.3332469289621787]
  Large language models (LLMs) can generate charts or flag misleading figures, but it remains unclear whether they can reason about and enforce visualization rules directly.<n>We present the first systematic evaluation of LLMs against visualization rules using hard-verification ground truth derived from Answer Set Programming (ASP)<n>Results show that frontier models achieve high adherence (Gemma 3 4B / 27B: 100%, GPT-oss 20B: 98%) and reliably detect common violations (F1 up to 0.82),yet performance drops for subtler perceptual rules (F1 0.15 for some categories) and for outputs generated from technical
  arXiv  Detail & Related papers  (2026-02-23T18:47:51Z)
• LLMCFG-TGen: Using LLM-Generated Control Flow Graphs to Automatically Create Test Cases from Use Cases [11.173694789846435]
  Appropriate test case generation is critical in software testing.<n>Use-case descriptions are a popular method for capturing functional behaviors and interaction flows in a structured form.<n>We propose a new approach that automatically generates test cases from NL use-case descriptions.
  arXiv  Detail & Related papers  (2025-12-06T11:19:37Z)
• Towards Autoformalization of LLM-generated Outputs for Requirement Verification [0.6015898117103068]
  Autoformalization, the process of translating informal statements into formal logic, has gained renewed interest with the emergence of powerful Large Language Models.<n>This paper explores the use of a simple LLM-based autoformalizer to verify LLM-generated outputs against a small set of natural language requirements.<n>Our findings, while limited, suggest that autoformalization holds significant potential for ensuring the fidelity and logical consistency of LLM-generated outputs.
  arXiv  Detail & Related papers  (2025-11-14T19:45:17Z)
• RELIC: Evaluating Compositional Instruction Following via Language Recognition [37.49115450182637]
  Large language models (LLMs) are increasingly expected to perform tasks based only on a specification of the task provided in context.<n>We introduce the Recognition of Languages In-Context (RELIC) framework to evaluate instruction following using language recognition.
  arXiv  Detail & Related papers  (2025-06-05T16:17:24Z)
• ConformalNL2LTL: Translating Natural Language Instructions into Temporal Logic Formulas with Conformal Correctness Guarantees [10.687644259002674]
  We introduce a new NL-to-LTL translation method, called ConformalNL2LTL, that can achieve user-defined translation success rates over unseen NL commands.<n>Our method constructs formulas iteratively by addressing a sequence of open-vocabulary Question-Answering (QA) problems with LLMs.
  arXiv  Detail & Related papers  (2025-04-22T20:32:34Z)
• Self-Steering Language Models [113.96916935955842]
  DisCIPL is a method for "self-steering" language models.<n>DisCIPL uses a Planner model to generate a task-specific inference program.<n>Our work opens up a design space of highly-parallelized Monte Carlo inference strategies.
  arXiv  Detail & Related papers  (2025-04-09T17:54:22Z)
• $\texttt{SEM-CTRL}$: Semantically Controlled Decoding [53.86639808659575]
  $texttSEM-CTRL$ is a unified approach that enforces rich context-sensitive constraints and task- and instance-specific semantics directly on an LLM decoder.<n>texttSEM-CTRL$ allows small pre-trained LLMs to efficiently outperform larger variants and state-of-the-art reasoning models.
  arXiv  Detail & Related papers  (2025-03-03T18:33:46Z)
• RuleArena: A Benchmark for Rule-Guided Reasoning with LLMs in Real-World Scenarios [58.90106984375913]
  RuleArena is a novel and challenging benchmark designed to evaluate the ability of large language models (LLMs) to follow complex, real-world rules in reasoning.<n> Covering three practical domains -- airline baggage fees, NBA transactions, and tax regulations -- RuleArena assesses LLMs' proficiency in handling intricate natural language instructions.
  arXiv  Detail & Related papers  (2024-12-12T06:08:46Z)
• Aligning Language Models to Explicitly Handle Ambiguity [22.078095273053506]
  We propose Alignment with Perceived Ambiguity (APA), a novel pipeline that aligns language models to deal with ambiguous queries. Experimental results on question-answering datasets demonstrate that APA empowers LLMs to explicitly detect and manage ambiguous queries. Our finding proves that APA excels beyond training with gold-standard labels, especially in out-of-distribution scenarios.
  arXiv  Detail & Related papers  (2024-04-18T07:59:53Z)
• Log Probabilities Are a Reliable Estimate of Semantic Plausibility in Base and Instruction-Tuned Language Models [50.15455336684986]
  We evaluate the effectiveness of LogProbs and basic prompting to measure semantic plausibility. We find that LogProbs offers a more reliable measure of semantic plausibility than direct zero-shot prompting. We conclude that, even in the era of prompt-based evaluations, LogProbs constitute a useful metric of semantic plausibility.
  arXiv  Detail & Related papers  (2024-03-21T22:08:44Z)
• Learning to Check: Unleashing Potentials for Self-Correction in Large Language Models [5.463333911506443]
  We aim to enhance the self-checking capabilities of large language models (LLMs) by constructing training data for checking tasks. We propose a specialized checking format called "Step CoT Check" Experiments demonstrate that fine-tuning with the "Step CoT Check" format significantly improves the self-checking and self-correction abilities of LLMs.
  arXiv  Detail & Related papers  (2024-02-20T14:23:23Z)
• Self-Evaluation Improves Selective Generation in Large Language Models [54.003992911447696]
  We reformulate open-ended generation tasks into token-level prediction tasks. We instruct an LLM to self-evaluate its answers. We benchmark a range of scoring methods based on self-evaluation.
  arXiv  Detail & Related papers  (2023-12-14T19:09:22Z)
• Grammar-Constrained Decoding for Structured NLP Tasks without Finetuning [27.59524153097858]
  grammar-constrained decoding (GCD) can be used to control the generation of large language models (LMs) GCD can serve as a unified framework for structured NLP tasks in general. We show that grammar-constrained LMs substantially outperform unconstrained LMs or even beat task-specific finetuned models.
  arXiv  Detail & Related papers  (2023-05-23T11:54:37Z)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  We propose a new satisfiability-aided language modeling (SatLM) approach for improving the reasoning capabilities of large language models (LLMs) We use an LLM to generate a declarative task specification rather than an imperative program and leverage an off-the-shelf automated theorem prover to derive the final answer. We evaluate SATLM on 8 different datasets and show that it consistently outperforms program-aided LMs in the imperative paradigm.
  arXiv  Detail & Related papers  (2023-05-16T17:55:51Z)
• Large Language Models are Better Reasoners with Self-Verification [48.534270563880845]
  Large language models (LLMs) have shown strong reasoning ability in several natural language processing tasks. LLMs with chain of thought (CoT) prompting require multi-step prompting and multi-token prediction, which is highly sensitive to individual mistakes. We propose and prove that LLMs also have similar self-verification abilities.
  arXiv  Detail & Related papers  (2022-12-19T15:51:52Z)
• Measuring Reliability of Large Language Models through Semantic Consistency [3.4990427823966828]
  We develop a measure of semantic consistency that allows the comparison of open-ended text outputs. We implement several versions of this consistency metric to evaluate the performance of a number of PLMs on paraphrased versions of questions.
  arXiv  Detail & Related papers  (2022-11-10T20:21:07Z)

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.