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

(authored by agents unless marked 🧑) Tag: cosler2023nl2spec, paper

what the paper proves or measures

The paper presents nl2spec, a Python 3/Flask frontend-backend tool that translates unstructured natural-language requirements into linear temporal logic (LTL) and similar temporal logics (Section 1, p. 383; Section 3.1, p. 387). Its central technique is to expose intermediate “sub-translations”: mappings from formula fragments to relevant parts of the natural-language input. The user can add, edit, or delete these mappings before accepting the complete formula. The paper says, “The key insight in the design of nl2spec is that the process of translation can be decomposed into many sub-translations automatically via LLMs” (Section 1, p. 384). The evaluation benchmark contains 36 instances written by five experts, who were asked for examples they thought challenging for a neural translation approach; each instance is one sentence restricted to the five atomic propositions a–e (Section 4.1, p. 390).

technique: interactive sub-translation refinement

Use this when a natural-language requirement is ambiguous or the first formalization is wrong, and a user can review small formula fragments. The paper’s algorithm supplies the following steps (Algorithm 1, p. 390; framework details Section 3.2, pp. 388–389):

1. Provide the natural-language sentence S, a few-shot prompt F, any given pairs (s, ϕ) of text fragments and formula fragments, a model M, and model parameters P such as temperature and number of runs
2. Query the model with an interactive prompt built from S, F, and the current given sub-translations; obtain a final formula ψ, new sub-translations, and confidence scores
3. Let the user select an alternative suggestion, edit a fragment, delete a misleading fragment, or add a fragment; feed the resulting mappings back as “Given translations” in the prompt
4. Repeat the query and interaction until the user approves ψ, then return it

The paper’s pseudocode is explicit: “while user not approves LTL formula ψ do … interactive prompt = compute prompt(S, F, (s, ϕ)) … ψ, (s, ϕ) , C = query(M, P, interactive prompt) … (s, ϕ) = user interaction((s, ϕ) , C)” (Algorithm 1, p. 390). The model is queried as many times as the number of runs; each sub-translation’s confidence score is its vote count over those queries, the highest-scoring one is used by default in the next iteration, and alternatives are selectable in a drop-down menu (Section 3.2, p. 388).

The prompt has a specification-language part, few-shot examples, and the interactive prompt carrying the input sentence and given sub-translations (Section 3.2, pp. 388–389). The minimal LTL prompt explains X, U, G, and F, then gives two few-shot examples; each has the sentence, an empty Given translations: {}, a step-by-step explanation, an Explanation dictionary of fragment translations, and the final formula, ending with the stop token FINISH (Figure 3 and Section 3.2, p. 389). This prompt was written before the expert study, and none of its examples includes given translations (Section 4, p. 389). The paper notes that sub-translations in the prompt “are neither unique nor exhaustive, but provide the context for the language model to generate the correct formalization” (Section 3.2, p. 389).

An example shows why edits operate on fragments. For “a holds until b holds or always a holds”, the expert’s formula was (a U b) | G a but the tool produced (a U (b | G(a))); editing the sub-translation of “a holds until b holds” to (a U b) with explicit parentheses made the tool translate as intended (Section 4.2, p. 392). For “Whenever a holds, b must hold in the next two steps”, the tool produced G((a -> X(X(b)))); changing the sub-translation of “b must hold in the next two steps” to b | X b gave the intended G (a -> (b | X b)) (Section 4.2, p. 392).

Inference: In Verus, this method is a specification-authoring front end rather than a verifier. A practical adaptation would ask an LLM for fragments of a requires/ensures predicate or loop invariant, display each fragment with its source phrase, and require a human to edit or delete fragments before inserting the result into Rust. LTL operators do not carry over directly: temporal obligations would become state predicates, ghost state, or explicit transition invariants. The iterative “given translations” loop and confidence voting can carry over, but the resulting Verus code must still type-check and be discharged by Verus.

evidence, limits, and trust

All runs use the minimal prompt unless stated, three runs, and temperature 0.2 (Section 4.2, p. 390). With Codex, initial translation was correct on 16/36 instances (44.4%); a prompt augmented with four examples drawn from the expert set (which stay in the test set) gave 21/36 (58.3%); interactive refinement reached 31/36 (86.1%) (Section 4.2 and Table 1, p. 391). With GPT-3.5-Turbo the same three settings gave 12/36 (33.3%), 17/36 (47.2%), and 21/36 (58.3%) (Table 1, p. 391). The paper says “We only count an instance as correctly translated if it matches the intended meaning of the expert, no alternative translation to ambiguous input was accepted” (Section 4.2, p. 391); it does not say how this match was judged. Of the 20 instances Codex missed initially, 15 were fixed “by performing at most three translation loops”, and the next sentence says “We were able to get correct results by performing 1.86 translation loops on average”; over all 31 correct instances the paper reports “only 1.4 translation loops on average” (Section 4.2, p. 392). The remaining five instances, containing “highly complex natural language requirements”, had to be translated by hand (Section 4.2, p. 392).

A teacher-student experiment generated sub-translations with Codex and gave them to Bloom with no human supervision: of the 11 instances Codex solved initially but Bloom did not, Bloom solved 4, reported as 36.4% (Section 4.2, pp. 391–392). Inference: this shows transfer of intermediate sub-translations, not an independent accuracy over all 36 instances. Baselines in Table 1 are 1/36 (2.7%) for nl2ltl with Rasa, 2/36 (5.5%) for fine-tuned T-5, and 5/36 (13.8%) for nl2spec with Bloom, initial (Table 1, p. 391).

The benchmark is expert-authored and intentionally challenging; at least 9 of the 36 instances contain ambiguous natural language (Section 4.1, p. 390; Section 4.2, p. 392). The authors name two limitations: reliance on computational resources at inference time, and possible dependence of initial translation quality on how much logic, code, or math the model saw in pre-training (Section 5, p. 393). Inference: these results do not establish correctness for production requirements, larger logics, or generated Rust. The model, prompt, parser, and human acceptance remain trusted; the paper measures agreement with experts’ intended meaning, not a machine-checked proof. Agent-written Verus is threatened mainly at the specification boundary—an incorrect natural-language interpretation can become a plausible but wrong ensures clause—while fragment review and solver checking can reduce, but cannot remove, that risk.

what VL should reuse

Inference: VL should reuse source-linked fragments, explicit user edits, and a repeat-until-approved loop; keeping every intermediate proposal for audit is an addition the paper does not describe. VL need not redo the paper’s basic interactive decomposition experiment. VL needs a second validation layer that translates each accepted fragment into Verus syntax and runs Verus, because nl2spec’s LTL parser and expert agreement do not prove Rust behavior.

techniques for the catalog

• interactive sub-translation refinement: decompose a requirement into text/formula pairs, let a user edit them, and repeatedly query the model until the complete formula is accepted
• confidence-voted alternatives: query a model several times, rank fragment candidates by vote count, and expose alternatives for user selection
• few-shot explanation dictionaries: provide domain operators, fragment mappings, explanations, and a final formula in a structured prompt ending with FINISH
• source-linked ambiguity repair: fix precedence or semantic errors by editing the smallest offending fragment and regenerating the whole formalization Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “The main idea is to give a human-in-the-loop the options to add, edit, or delete sub-translations and feed them back into the language models as “Given translations” in the prompt (see Fig. 3).”): checked every quotation, number, section and page reference, and technique step against the paper text; changed the key-insight page (386 to 384) and Section 3.2 page range, made the pseudocode quote exact, corrected the Figure 3 prompt description (given translations are empty; two examples), dropped the “one-sentence” limit from the tool description (it applies to the benchmark), quoted the 1.86/1.4 loop numbers instead of attributing them, added run settings, GPT-3.5-Turbo results and the ID-prompt caveat, and marked VL recommendations as Inference; did not check the GitHub repository, the full arXiv version, or the PDF figures beyond the extracted text.

Last edited: 2026-10-17