nl2spec++

Suppose one requirement connects A to B, while another connects B to C. Neither directly describes A and C. Translating each sentence independently preserves the explicit statements, but leaves the relationship we actually want unresolved.

nl2spec++ extends nl2spec with this cross-sentence reasoning step. Its input is two related natural-language sentences and two target entities, one from each sentence. A shared intermediate entity provides the connection; the desired output is a candidate relationship expressed in linear temporal logic (LTL).

Method 1: reason in language, then translate

The model first infers a natural-language statement linking the target entities. The translation module then turns that statement into LTL. Keeping an intermediate explanation in ordinary language makes the proposed relationship easier to inspect before formalization.

Method 2: translate first, then reason over formulas

Each input sentence is translated separately. A second LLM call receives the two formulas and the target entities, and proposes their relationship in LTL. This route makes the formal intermediate representations explicit, but its reasoning step is still performed by a language model, not a theorem prover.

The two routes are alternatives selected by the user. They are not successive stages of one pipeline.

The repository’s formula-reasoning prompt includes an eventual-response example. Read G as “always” and F as “eventually”:

G(A → F B)
G(B → F C)
────────────
G(A → F C)

Whenever A occurs, B must eventually occur; whenever B occurs, C must eventually occur. Together, these requirements imply that A is eventually followed by C. This illustrates a temporal dependency, not a causal claim. It is an explanatory example from the prompt, not a reported benchmark result.

The command-line entry point passes the selected method to src/backend.py. Method 1 calls the semantic reasoning prompt before the translation module; Method 2 translates both inputs before calling the formula reasoning prompt. The repository separates semantic extraction, formula reasoning and translation so the intermediate representations remain inspectable.

The translation path samples candidate formulas, attempts to parse them with an LTLf parser, and selects the most frequent candidate with a frequency-based certainty score. That score reflects agreement among sampled outputs; it is not a calibrated probability of correctness. Parse failures can remain as raw strings, and the final formula-reasoning output in Method 2 does not pass through an equivalent end-to-end proof check.

Formal-looking output can still be wrong. Correct syntax does not establish that a formula follows from the input, and a repeated answer can repeat the same mistake. A further issue is semantic consistency: the prompts use LTL terminology, while parsing uses an LTLf library, so finite- and infinite-trace interpretations need to be made explicit before verification.

Some prompt examples also overreach: temporal ordering alone does not justify a causal explanation. These examples should be audited before treating the system as a reliable specification tool.

The repository identifies broader application scenarios, reasoning over more than two sentences, and a dedicated benchmark as future work. It does not report a comparative benchmark establishing that one route is more accurate than the other. This article explains the checked-in design and code; it does not claim a fresh execution of the legacy model integrations.

The useful connection here is between flexible language understanding and explicit, inspectable constraints. An LLM can propose the hidden relationship; formal tools can then help test whether that proposal is justified. A next step would be an entailment check that searches for a counterexample to the candidate formula, alongside a benchmark that separates translation errors from reasoning errors.

This is the distinction I want the project to make visible: producing a specification is the beginning of validation, not its completion.