Automatic Translation of Natural Language Requirements into Ctl Specifications Using Large Language Models: A Multi-Approach Evaluation ⋆
Bibliographic record
Abstract
Translating natural language (NL) requirements into formal specifications such as Computation Tree Logic (CTL) is essential for improving the efficiency and scalability of formal verification, especially in safety-critical systems. This study evaluates the ability of Large Language Models (LLMs) to automate this process. We compare three approaches: fine-tuning the Mistral model, using GPT-4 in a few-shot learning setup, and a hybrid that feeds a BERT pattern classifier’s prediction to GPT-4. Using the Natural2CTL dataset, we assess strict logical accuracy and an ambiguity-tolerant accuracy, complemented by auxiliary semantic and structural operator similarity measures. Fine-tuning yields the strongest strict correctness and operator-structure fidelity, while the hybrid narrows the gap to fine-tuning and substantially improves over few-shot prompting alone. Residual errors across methods concentrate in path-quantifier selection, temporal granularity, and scoping in multi-clause requirements. Overall, LLMs can draft CTL candidates that are usable after lightweight normalisation, but they should be integrated into human-in-the-loop workflows with basic automated checks before use in high-assurance settings. • Benchmarks three LLM-based methods for NL-to-CTL translation. • Fine-tuned Mistral achieves 47.6% strict logical accuracy and 71.4% ambiguity-tolerant accuracy for CTL specification generation. • GPT-4 few-shot learning offers rapid prototyping but lower syntactic precision. • BERT-GPT hybrid balances pattern recognition and generative translation. • LLM automation reduces expert effort, but expert review remains critical for safety.
Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.
How this classification was reachedexpand
Full frame machine prediction
Teacher imitationNot calibrated prevalence, not ground truth. Human validation pending. The Gemma side is a direct model label for every work in the frame, read from the title-only record. The Codex side is a classifier learned from the 10,348 direct Codex labels and calibrated to design-weighted sample rates; fields without enough sample support carry no Codex call. Candidate is the union of the two sides; consensus is their intersection. These outputs are machine_predicted_unvalidated and are not human labels.
Distilled classifier scores by category (both heads)
| Category | Codex | Gemma |
|---|---|---|
| Metaresearch | 0.003 | 0.013 |
| Meta-epidemiology (narrow) | 0.001 | 0.001 |
| Meta-epidemiology (broad) | 0.001 | 0.001 |
| Bibliometrics | 0.001 | 0.001 |
| Science and technology studies | 0.001 | 0.001 |
| Scholarly communication | 0.002 | 0.003 |
| Open science | 0.002 | 0.002 |
| Research integrity | 0.001 | 0.001 |
| Insufficient payload (model declined to judge) | 0.009 | 0.002 |
Machine scores (provisional)
The two teacher heads of the student model, read on this work. A score orders the frame for review; it never asserts a category, and the validation status ships verbatim with every row.
Baseline scores from an immature model (maturity gate not passed, 7 training rounds). Scores rank; they never assert a category.
score_only:v0-immature-baseline · verbatim from the scoring run: score_only means the number may rank works, and no category label ships from itClassification
machine, unvalidatedMachine predicted; a candidate call from one source (direct Gemma or distilled Codex), not a consensus.
How this classification was reached, model by model and score by score, is at the end of the page under "How this classification was reached".