PaperlayerView exact revision on arXiv

Source-linked AI summary

nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models

Matthias Cosler, Christopher Hahn, Daniel Mendoza, Frederik Schmitt, Caroline Trippel

arXiv:2303.04864v1cs.LOcs.AIcs.LG

TL;DR

Writing formal specifications from natural language is error-prone and time-consuming. nl2spec uses LLM-generated sub-translations that users can edit interactively; on the study dataset, it correctly translated 31 of 36 instances (86.11%) with an average of 1.4 translation loops.

  • Problem

    Writing formal specifications is an error-prone and time-consuming manual task, typically reserved for experts.

    Source: §1 · p. 1

  • Method

    nl2spec uses LLMs to decompose natural-language requirements into sub-translations that users can interactively add, edit, or delete.

    Source: §1 · pp. 1–2

  • Results

    31 of 36 instances (86.11%) were correctly translated using nl2spec, with an average of 1.4 translation loops.

    Source: §4.2 · p. 10

  • Takeaways & Limitations

    A user study showed nl2spec can be used efficiently to interactively formalize unstructured and ambiguous natural language.

    Source: §5 · p. 11

    The approach relies on computational resources at inference time, and initial translation quality may depend on the underlying model’s pretraining data.

    Source: §5 · p. 10

Abstract

from arXiv · show

A rigorous formalization of desired system requirements is indispensable when performing any verification task. This often limits the application of verification techniques, as writing formal specifications is an error-prone and time-consuming manual task. To facilitate this, we present nl2spec, a framework for applying Large Language Models (LLMs) to derive formal specifications (in temporal logics) from unstructured natural language. In particular, we introduce a new methodology to detect and resolve the inherent ambiguity of system requirements in natural language: we utilize LLMs to map subformulas of the formalization back to the corresponding natural language fragments of the input. Users iteratively add, delete, and edit these sub-translations to amend erroneous formalizations, which is easier than manually redrafting the entire formalization. The framework is agnostic to specific application domains and can be extended to similar specification languages and new neural models. We perform a user study to obtain a challenging dataset, which we use to run experiments on the quality of translations. We provide an open-source implementation, including a web-based frontend.

1 Introduction

nl2spec translates natural-language requirements into temporal logic by decomposing them into editable sub-translations, letting users interactively resolve ambiguity and translation errors. The introduction also describes an expert study that provides challenging translations for evaluating the approach.

Introduction

  • nl2spec decomposes natural-language requirements into sub-translations that users can add, edit, or delete instead of revising an entire formalization.The framework targets LTL and similar temporal logics and includes a web-based tool.Source: §1 · p. 1
  • For the requirement “Globally, grant 0 and grant 1 do not hold at the same time until it is allowed”, nl2spec correctly produces the LTL formula G((!((g0 & g1)) U a)).It also generates the subtranslation pair (“do not hold at the same time”, !(g0 & g1)), which helps verify the translation.Source: §1 · p. 2
  • An expert user study gathered challenging natural-language-to-LTL translations, and the paper evaluates end-to-end translation accuracy on that benchmark.The study targets ambiguity such as uncertainty about operator precedence, which users can address by adding or editing a sub-translation with explicit parentheses.Source: §1 · pp. 2–3
  • Confidence scores, alternative suggestions, and deletion of misleading sub-translations are designed to keep human supervision minimal and efficient.Users can choose suggested alternatives from a drop-down menu before the next translation loop.Source: §1 · p. 2
  • The framework is agnostic to machine-learning models and application domains, and the paper gives an STL prompt as a proof of concept for other logics.The authors also discuss adapting prompts and inputs to application domains to improve translation quality.Source: §1 · p. 3

2 Background & Related Work

The background introduces LTL as a prototype temporal logic for specifications and reviews prior natural-language translation approaches. It motivates nl2spec’s focus on resolving natural-language ambiguity and explains its use of LLMs with few-shot prompting.

2.1 Natural Language to Linear-time Temporal Logic

  • LTL extends propositional logic with temporal operators and serves as a prototype for keeping nl2spec extendable to domain-specific specification languages.Its operators include U (until) and X (next), with F for eventuality and G for global properties.Source: §2.1 · p. 3
  • Prior translation work spans grammar-based, interactive, domain-specific, and neural approaches, but previous tools lack detection and interactive resolution of natural-language ambiguity.Some robotics datasets and domains use structured natural language, unlike nl2spec’s setting.Source: §2.1 · pp. 3–4

2.2 Large Language Models

  • LLMs are large neural networks, and Transformers have also shown performance in verification, reasoning, and auto-formalization tasks.The cited examples include GPT and BERT families, as well as open-source T5 and Bloom and commercial Codex models.Source: §2.2 · p. 4
  • The framework uses few-shot prompting, presenting a language model with a task description and examples of input-output behavior.This is described as a common way to pursue high performance with limited labeled data, alongside fine-tuning as a valid translation approach.Source: §2.2 · p. 4
  • Codex and Bloom were implemented and used in the expert-user study after showing the best performance during testing.Source: §2.2 · p. 4

3 The nl2spec Framework

nl2spec combines a frontend-backend tool with interactive few-shot prompting that lets users refine sub-translations feeding into an LTL formalization. Its prompt structure and modular design support adaptation to new models and domain-specific prompts.

3.1 Overview

  • The Python 3 and Flask framework can run from the command line or through a web frontend, and parses generated LTL formulas with a standard parser.Source: §3.1 · pp. 5–6
  • The frontend accepts a natural-language sentence and model settings, presents sub-translations and confidence information, and lets users edit them; the backend handles models, prompts, and ambiguity resolution.The framework is designed to support new models and domain-specific prompt files, which must follow its interactive prompting scheme.Source: §3.1 · p. 6

3.2 Interactive Few-shot Prompting

  • The interactive loop feeds user-added, edited, or deleted sub-translations back to the model as given translations until the user approves the LTL formula.Confidence scores reflect consensus across multiple model queries, with alternative translations available for interactive selection.Source: §3.2 · pp. 6–7
  • The few-shot prompt uses two examples that pair natural-language inputs and given sub-translations with explanations and final LTL formulas; sub-translations are neither unique nor exhaustive.The scheme elicits sub-translations as fine-grained explanations that provide context for generating the formalization.Source: §3.2 · p. 7

4 Evaluation

On a 36-instance expert benchmark, nl2spec’s sub-translation methodology achieved 86.11% correctness with an average of 1.4 translation loops. The evaluation also examined initial translation quality, ambiguity resolution, and correction of erroneous translations.

4 Evaluation

  • The evaluation used a minimal prompt focused on interactive refinement, with three runs and temperature 0.2.The prompt included minimal specification-language knowledge, was written before the expert study, and used at most two few-shot examples without any “given translations” example.Source: §4 · p. 8, §4.2 · p. 8

4.1 Study Setup

  • Five experts contributed 36 benchmark instances, each an unrestricted one-sentence natural-language specification over at most five atomic propositions.The experts worked in a shared document to ensure unique instances.Source: §4.1 · p. 8

4.2 Results

  • Codex translated 44.4% of instances correctly with the minimal prompt, outperforming Bloom; in-distribution examples raised accuracy to 58.3%.The in-distribution prompt used four randomly drawn expert examples, with those examples remaining in the dataset.Source: §4.2 · p. 9, Table 1 · p. 9
  • With Codex-generated sub-translations supplied, Bloom solved 4 of 11 instances it could not initially solve (36.4%), without human supervision.This experiment indicates that improving sub-translations can improve the final formalization even with an underperforming neural model.Source: §4.2 · p. 9
  • At least 9 of 36 benchmark requirements were ambiguous, involving either natural-language limits such as operator precedence or semantic ambiguity.Editing the corresponding sub-translations enabled the tool to produce the experts’ intended formulas in both illustrated cases.Source: §4.2 · p. 10
  • Refinement corrected 15 of 20 initially incorrect Codex translations in at most three loops, averaging 1.86 loops; the remaining five required manual translation.The failures requiring manual translation involved highly complex natural-language requirements.Source: §4.2 · p. 10
  • 31 of 36 instances (86.11%) were translated correctly using the sub-translation methodology, with an average of 1.4 translation loops.The reported overall result follows interactive sub-translation refinement.Source: §4.2 · p. 10

5 Conclusion

nl2spec maps formula fragments to relevant natural-language fragments and lets users interactively revise those mappings; a user study showed it can efficiently support formalization of unstructured, ambiguous requirements.

5 Conclusion

  • At inference time, nl2spec relies on computational resources, while initial-translation quality might depend on models’ pre-training exposure to logic, code, or mathematics.Commercial and open-source models provide accessible APIs, but the paper identifies inference-time resource reliance as a general limitation of deep learning.Source: §5 · p. 10
  • nl2spec decomposes input into formula-fragment sub-translations and lets users add, edit, or delete them instead of redrafting an entire formalization.An interactive prompting scheme queries LLMs for the mappings, and the framework includes an interface for users to revise them.Source: §5 · p. 11
  • A user study showed that nl2spec can be used efficiently to interactively formalize unstructured and ambiguous natural language.Source: §5 · p. 11

A Linear-time Temporal Logic (LTL)

This section introduces LTL syntax and semantics over infinite traces of atomic propositions, defining conjunction, next-step satisfaction, and until.

A Linear-time Temporal Logic (LTL)

  • LTL formulas are built from atomic propositions, negation, conjunction, a unary temporal operator, and until.The displayed grammar gives the formula forms, while the semantics identifies the unary operator as shifting satisfaction to the trace suffix beginning at position 1.Source: A Linear-time Temporal Logic (LTL) · p. 15
  • Traces are infinite sequences over sets of atomic propositions; t[i] gives the propositions at position i, and t[i,j] and t[i,∞] denote finite segments and infinite suffixes.Source: A Linear-time Temporal Logic (LTL) · p. 15
  • LTL satisfaction requires both conjuncts to hold, evaluates the unary temporal operator on the suffix from position 1, and defines until by a future position where its second formula holds after its first holds at every earlier position.The semantics is introduced as the smallest relation satisfying the stated conditions.Source: A Linear-time Temporal Logic (LTL) · p. 15

B Transformer Architecture · C Prompts

The paper explains how Transformer architectures process sequences through embeddings, positional encodings, and self-attention, then describes prompts that support LTL and other specification tasks. The prompt discussion notes an unoptimized limitation and gives smart-home and STL examples.

B Transformer Architecture

  • A vanilla Transformer encodes input embeddings in parallel and autoregressively generates output embeddings, with positional encodings distinguishing sequence order.The encoder constructs a hidden embedding for each input embedding, while the decoder generates output embeddings one at a time.Source: B Transformer Architecture · p. 15
  • Transformer variants include decoder-only GPT models and encoder-only BERT models [11], alongside the vanilla encoder-decoder structure.Embeddings map plain inputs such as words or characters to high-dimensional vectors; the passage gives word2vec [32] as an example.Source: B Transformer Architecture · p. 15
  • Self-attention uses learned query, key, and value projections to score which sequence positions matter when computing each element’s embedding.The embeddings can be calculated all at once using matrix operations.Source: B Transformer Architecture · pp. 15–16

C Prompts

  • The post-study prompt retains the minimal prompt’s initial LTL tutorial so the impact of sub-translations can be shown.Figure 4 presents the augmented prompt after the expert user study.Source: C Prompts · p. 16
  • The prompt leaves room for optimization: it does not explain the combined FG temporal operators, which led to failed translations in the expert user dataset.Source: C Prompts · p. 16
  • A proof-of-concept prompt applies the framework to a smart-home case study.The prompt is shown in Figure 6 and will be included in the open-source release.Source: C Prompts · p. 16
  • A second proof-of-concept prompt targets Signal Temporal Logic, a variation of LTL for continuous signals.The prompt is shown in Figure 5 and will be included in the open-source release.Source: C Prompts · p. 16

D Remaining Instances

This section examines instances nl2spec could not translate within three tries, which were difficult because they used advanced operators or obscured temporal meaning.

D Remaining Instances

  • Untranslated instances resisted nl2spec and the minimal prompt within three tries, often using operators such as “release” or hiding temporal meaning in natural language.The section reports these as especially difficult cases.Source: D Remaining Instances · p. 16

E Variables

The section describes how users can provide or edit variable translations as subtranslations, allowing the model to adjust to natural-language patterns. In the example, specifying one variable helps the model infer another.

E Variables

  • LLMs can adjust variable translations to patterns in natural language.The paper identifies this adaptability as an advantage of using large language models.Source: E Variables · p. 16
  • Users can provide or edit variable translations as subtranslations.Source: E Variables · pp. 16–17
  • In the example, adding “process 0 terminates” as a subtranslation lets the model adjust “process 1 will start” to s p1 automatically.The natural-language input says that globally, when process 0 terminates, process 1 will start in the next step (Figure 7).Source: E Variables · p. 17

F Ambiguity Resolving

This section shows the nl2spec frontend during ambiguity resolution.

F Ambiguity Resolving

G Fixing Erroneous Translations

This section illustrates how users fix erroneous translations by editing subtranslations in nl2spec’s frontend, including changes to address operator precedence and reflect the input’s meaning.

G Fixing Erroneous Translations

  • The frontend lets users edit subtranslations to debug erroneous translations and make them reflect the input’s meaning.The section illustrates this with frontend screenshots and examples of editing a subtranslation.Source: G Fixing Erroneous Translations · p. 17, Figure 9 · p. 22, Figure 10 · p. 23
  • The examples also show providing a subtranslation for variable translations.Source: Figure 7 · p. 20
  • Adding parentheses to a subtranslation can fix operator precedence.Figure 8 shows a subtranslation being fixed with parentheses to ensure the intended precedence.Source: Figure 8 · p. 21
Loading 2303.04864v1…