2026· Poster Volume 0007 The 2026 Twenty-Second International Conference on Intelligent Computing July 23-26, 2026 Toronto, Canada· pp. 677-681· 0 citations
TL;DR
GenCTL is proposed, a prompt-based framework for effective and model-aware NL2CTL translation without task-specific fine-tuning that improves the reliability and practical checkability of LLM-generated CTL specifications.
Abstract
Natural language (NL) requirements are widely used in system design, but their ambiguity makes formal verification difficult. Translating NL requirements into Computation Tree Logic (CTL) is challenging because generated formulas must be both semantically appropriate and compatible with concrete verification models. Although large language models (LLMs) provide a promising basis for NL-to-CTL(NL2CTL) translation, their outputs are often unstable and prone to parsing, typing, and grounding errors.
To address these issues, we propose GenCTL, a prompt-based framework for effective and model-aware NL2CTL translation without task-specific fine-tuning. GenCTL combines structured prompting, retrieval-enhanced few-shot examples, atomic-proposition (AP) grounding from nuXmv models, multi-candidate generation with frequency-first selection and length-normalized log-likelihood tie-breaking, and interactive refinement through an explanation dictionary.
Experimental results demonstrate the effectiveness of the proposed framework in both model-agnostic and model-aware settings. On a generated NL--CTL dataset, the best automatically selected translation achieves 68% accuracy, which increases to 92% after one round of user refinement. On 150 NL requirements grounded in three nuXmv models, AP-list prompting yields 139/150 directly checkable formulas, increasing to 149/150 after lightweight normalization. These results show that GenCTL improves the reliability and practical checkability of LLM-generated CTL specifications.
Large Language Models (LLMs) have shown promise for translating Natural Language (NL) planning descriptions into PDDL problem instances. However, standard evaluation criteria such as syntactic validity or planner success can substantially overestimate faithfulness to the described task: a generated problem may be parseable and solvable while misrepresenting the intended initial state, goal, object structure, or optimization target. This paper studies an end-to-end NL-to-PDDL pipeline that combines LLM generation, checks in terms of PDDL parsing, planning and validation, a domain-conformance checker, an LLM critic, and iterative repair. Fine-grained repair feedback is constructed from the domain description, the generated problem, the natural language problem description, and operational diagnostics. Reference-based comparisons against curated benchmark PDDL problem descriptions are used for post-hoc benchmark analysis, and these offline checks include renaming-invariant structural matching and semantic equivalence, where domain support is available. Across Planetarium, AutoPlanBench, and curated PDDL~2.1 problems, results show that operational success and benchmark-reference reconstruction can diverge substantially. Results also show that structured repair can be useful, and that PDDL~2.1 remains challenging for reference reconstruction, even when operational success improves.
J. Rosa, Pedro Santos, Valdemar Oliveira et al.· 0 citations
LLMSuite is proposed, a hybrid test generation framework that integrates self-refinement prompting with class-level LLM reasoning into the search-based testing process and complements manually written test suites by exercising domain-specific behaviors that are often left untested.
Amirhossein Deljouyi, Annibale Panichella, Andy Zaidman· 0 citations
The results indicate that current general-purpose LLMs can achieve practically significant performance on the unstructured NL-to-LTL task without task-specific fine-tuning, and suggest that modern LLMs are becoming viable front-end assistants for semi-automated formalization workflows.
In LLM-based code generation, Non-Functional Requirements (NFRs) are often specified as terse one-line phrases. We ask whether grounding those specifications in ISO/IEC 25010 Quality Model, either as rich natural-language prose (NL-rich) or as structured JSON (Structured), improves code generated on HumanEval/HumanEval-ET compared to a RobuNFR-style one-line baseline (NL-simple). We evaluate four NFRs (performance, error handling, code smell, readability) with ten prompt variations per condition under a fixed model snapshot and paired non-parametric analysis. Primary finding: ISO-grounded enrichment improves static quality proxies (unreadability density falls across all four NFRs (e.g., Performance 0.88 ->0.69 for NL-rich)) and reduces sensitivity to prompt wording, but does not reliably improve functional correctness; for error handling, extended-test pass rate decreases, suggesting tension between defensive coding patterns and exact-output benchmarks. Secondary finding: when ISO content is held constant, NL-rich and Structured differ negligibly in correctness (|delta|<= 0.023), indicating that semantic content matters more than JSON-vs-prose format. Practitioners should invest in standard-grounded NFR content rather than serialization form. A fully traceable replication package is provided.
Converting Korean natural-language avionics test procedures into an executable XML domain-specific language (DSL) is a labor-intensive bottleneck, yet neither automation extreme is acceptable in this safety-critical setting: end-to-end large language model (LLM) generation is unauditable and emits schema-violating values, while purely deterministic extraction leaves externally-grounded slots unsolved. We ask where, and how sparingly, an LLM should be invoked. From a 64-slot schema we derive a data-computed, five-class evidence-grounding slot taxonomy and build a confidence-gated selective hybrid: a deterministic tier resolves every slot whose evidence is lexical or catalog-grounded, and an on-premises retrieval-augmented LLM is invoked only for residual open-grounded slots with low retrieval confidence, under a gate threshold selected on a held-out validation split. On a leakage-controlled clean test split of <inline-formula> <tex-math notation="LaTeX">$1{,}705$ </tex-math></inline-formula> unique procedures (drawn from <inline-formula> <tex-math notation="LaTeX">$213{,}013$ </tex-math></inline-formula> industrial pairs after removing <inline-formula> <tex-math notation="LaTeX">$11.4\times $ </tex-math></inline-formula> duplication and 7.4% near-duplicate leakage), the hybrid is statistically equivalent to the pure on-premises LLM (59.4% instance Exact Match; paired 90% CI ±0.7 pp within a ±2 pp margin) while invoking the LLM on only 37% of instances, keeping 90% of emitted slots deterministic and audit-logged, and eliminating closed-vocabulary schema violations by construction (0 vs. 0.89%). Instantiating the same gate with a stronger BM25 backend nominally exceeds the pure LLM (60.4%; paired 90% CI <inline-formula> <tex-math notation="LaTeX">$[+0.2, +1.7]$ </tex-math></inline-formula> pp, McNemar <inline-formula> <tex-math notation="LaTeX">$p{=}0.044$ </tex-math></inline-formula>) at a 14% call rate. Because strict full automation remains below deployment thresholds, we position the system as an authoring-support tool: on a <inline-formula> <tex-math notation="LaTeX">$1{,}879$ </tex-math></inline-formula>-procedure candidate-ranking analysis of the full test split (an upper-bound characterization, not a clean-split estimate), the correct value appears in the top-five list for 84.5% of grounded slots (mean reciprocal rank 0.953), supporting a human-in-the-loop workflow in which a reviewer controls every emitted action. We conclude that a taxonomy-driven selective hybrid is simultaneously accurate, LLM-frugal, and supportive of DO-330 tool-qualification evidence generation.
This paper presents new Cantonese ParGram resources and evaluates LLMs for knowledge-driven grammar engineering within a controlled experimental paradigm. Using Cantonese ParGram resources as gold standards, with corresponding English baselines, we investigate whether OpenAI's gpt-oss-120b and GPT-5.4 can generate machine-processable grammars from sentences and target formal structures under systematically varied prompting conditions. GPT-5.4 outperformed gpt-oss-120b, while grammars generated from target formal structures generally outperformed those generated from sentences. Although both models could generate locally plausible phrase-structure rules, lexical entries, and templates, they often struggled to coordinate interacting formal constraints, especially in multi-construction settings. The results characterize both the capabilities and limitations of current LLMs for potential integration into AI-assisted expert workflows: LLMs may support intermediate stages of grammar development, but human linguistic expertise remains central to analysis, validation, and refinement. The study also contributes new Cantonese symbolic grammatical resources.
Chit-Fung Lam· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
