SCP-NL2TL: Selective Conformal Prediction with Semantic Verification for Natural Language to Temporal Logic Specifications
SCP-NL2TL combines semantic verification and conformal risk control to abstain from unsafe NL-to-temporal-logic translations.
Key Findings
Methodology
SCP-NL2TL treats any translator as a black box. An embedding-based k-nearest-neighbor conformal anomaly detector first screens atypical instructions. Accepted inputs are translated, then scored using back-translation fidelity, Sbt, and semantic agreement among five stochastic translations, Ssc. Their default fusion Sfu=(Sbt+Ssc)/2 is calibrated by Conformal Risk Control (CRC), which selects an accept-or-abstain threshold under a joint-risk budget α.
Key Results
- Across STL, fused scoring achieved AUROC 0.706, compared with 0.655 for self-consistency and 0.634 for back-translation. On SpaTiaL, fusion reached 0.920 versus 0.867 and 0.871, showing that the channels detect partially different errors.
- With 600 pooled calibration examples and α=0.10, fusion accepted 34.7% of STL translations and 88.9% of SpaTiaL translations. The corresponding feasibility floors were αℓ=0.0483 and 0.0083.
- Experiments covered STL, interval-free LTL, and SpaTiaL across D2–D4 tiers. GPT-5.2 had about 48% error and fine-tuned LLaMA-3-8B about 15%; selective calibration improved risk compliance under the evaluated cross-tier shifts.
Significance
The paper changes the operational objective from always producing an answer to recognizing when execution is unsafe. This matters for robots, autonomous vehicles, and industrial controllers, where a syntactically valid but semantically wrong formula can trigger harmful behavior. Unlike average exact-match accuracy, joint risk Rjoint=P(accepted and incorrect) directly measures the probability that an erroneous specification reaches the planner, with a finite-sample, distribution-free expectation guarantee under exchangeability.
Technical Contribution
The framework replaces inaccessible token likelihoods with signals computed from the final instruction–formula pair. It combines LLM back-translation, exact semantic clustering of repeated outputs, and an instruction-level conformal anomaly gate. CRC calibrates the bounded loss 1[S≤τ]z; Theorem 1 establishes Rjoint≤α under exchangeability, while Theorem 2 bounds the deferral probability for in-distribution instructions. The design is translator- and logic-agnostic.
Novelty
The authors present this as the first selective NL2TL framework that calibrates an accept-or-abstain decision for a single executable formula and directly controls accepted-error risk. Its fundamental novelty is architectural rather than a new translator: semantic verification, stochastic equivalence, CRC thresholding, and pre-translation anomaly screening are assembled into a model-agnostic safety layer applicable to STL, LTL, and SpaTiaL.
Limitations
- Theorem 1 requires exchangeability between calibration and test pairs and controls expectation-level risk, not every individual deployment. The anomaly detector cannot identify every subtle or adversarial distribution shift.
- LLM back-translation and judging introduce prompt sensitivity, evaluator bias, latency, and cost. Small calibration sets, tied scores, or very small α can make the feasibility floor high and force universal abstention.
Future Work
Future research should develop conditional guarantees under non-exchangeable and drifting environments, stronger formal-semantic verifiers, cheaper back-translation, and adaptive risk budgets. Larger real-robot and closed-loop studies are needed, along with calibrated escalation to users or stronger models. Important topics include missed-shift detection, groupwise calibration, adversarial instructions, and explicit cost–coverage–safety trade-offs.
AI Executive Summary
Natural-language interfaces promise to let users instruct robots without learning formal methods. Yet translating “avoid the obstacle, then reach the goal within ten seconds” into STL, LTL, or SpaTiaL is not merely a language task: a wrong predicate, temporal interval, scope, or spatial relation can produce an executable but unsafe plan. Existing NL2TL systems generally return a formula for every input, while exact-match accuracy describes averages rather than the trustworthiness of one decision.
SCP-NL2TL adds a calibrated safety gate around any black-box translator. An instruction-level conformal anomaly detector uses normalized embeddings and k-nearest-neighbor distance to defer atypical inputs before translation. For retained inputs, back-translation fidelity Sbt measures whether an LLM-rendered explanation preserves logical structure, temporal operators, time constraints, and overall meaning. Five temperature-1.0 translations are grouped by exact semantic equivalence to compute self-consistency Ssc. CRC then selects the largest score threshold whose empirical joint risk, corrected by 1/(n+1), fits the user budget α.
The evaluation uses STL and interval-free LTL from NL2TL and SpaTiaL from NL2SpaTiaL, with D2–D4 tiers, 200 calibration and 150 test examples per tier, and 100 random resplits. Fusion obtains AUROC 0.706 on STL and 0.920 on SpaTiaL. At α=0.10 with 600 pooled calibration samples, acceptance is 0.347 and 0.889, respectively. The system therefore turns uncertainty into an explicit operational action: execute, or abstain. Its guarantees still depend on exchangeability, and its LLM-based verification incurs cost and possible bias, but the work establishes a practical foundation for safer language-driven formal planning.
Deep Analysis
Background
LTL expresses discrete temporal requirements with F, G, and U; STL adds bounded intervals over continuous signals; SpaTiaL adds geometric and spatial operators. Prior NL2TL systems use semantic parsing, sequence models, pretrained language models, structured intermediates, retrieval, model-checker feedback, and grammar-constrained decoding. These methods improve generation and syntax, but usually always emit a formula and evaluate average accuracy rather than per-instance executability.
Core Problem
For instruction x, generated formula φ̂, and reference φ⋆, error is z=1[φ̂≢φ⋆]. The goal is to maximize coverage C=P(g=1) subject to joint risk Rjoint=E[gz]≤α. The formula space is effectively unbounded, so prediction sets are impractical for planners. Black-box translators also expose neither reliable token likelihoods nor internal uncertainty, requiring semantic signals from only x and φ̂.
Innovation
The work makes four distinctions from standard practice. It selects a single executable formula rather than constructing a prediction set; separates semantic mismatch through back-translation from generation instability through repeated semantic equivalence; calibrates acceptance with CRC rather than a coverage quantile; and screens the instruction itself before translation. These components address both unreliable outputs and failures of the exchangeability assumption under distribution shift.
Methodology
- �� Screening: compute normalized instruction embedding e(x), average k-nearest-neighbor distance D(x) to a disjoint training reference set, and conformal p-value; defer when p(x)<δ, with δ=0.05 in experiments.
- �� Translation: obtain φ̂ from any black-box NL2TL model; unparsable formulas receive Sbt=1.
- �� Verification: GPT-5.2 back-translates φ̂; gpt-4o judges four dimensions, giving Sbt=1−A.
- �� Stability: sample k=5 outputs at temperature 1.0, cluster by logic-specific canonical semantic equivalence, and compute Ssc=1−largest-cluster-size/k.
- �� Selection: use Sfu or Sbt on calibration data, define loss 1[S≤τ]z, and select the largest feasible τ̂ under Eq. (10). Accept when S≤τ̂. Theorem 1 gives Rjoint≤α under exchangeability.
Experiments
Datasets are NL2TL STL, interval-free LTL, and NL2SpaTiaL SpaTiaL, each divided into D2–D4. STL/LTL tiers reflect atomic-proposition counts; SpaTiaL tiers reflect logical-tree depth and branching. Each tier contributes 200 calibration and 150 test examples per split, with paraphrases kept together. Canonical equivalence handles commutativity, De Morgan transformations, and argument-order normalization. Models include few-shot GPT-5.2, fine-tuned LLaMA-3-8B, and a low-error fine-tuned T5 check. Metrics are AUROC, joint risk, acceptance, and risk exceedances.
Results
Fusion reached AUROC 0.706 on STL and 0.920 on SpaTiaL, improving over the best single channel by roughly 0.051 and 0.049. With α=0.10, pooled calibration gave acceptance rates of 0.347 and 0.889, with feasibility floors 0.0483 and 0.0083. STL self-consistency alone accepted 0%, illustrating excessive conservatism; fusion recovered coverage. The paper reports better compliance than coverage-calibrated baselines under evaluated shifts.
Applications
The method can gate robot task planners, autonomous-vehicle rule interfaces, industrial control constraints, and human–robot collaboration. A system can screen unfamiliar instructions, verify generated formulas, execute only accepted specifications, and escalate abstentions to a user, stronger model, or formal engineer. Deployment requires fixed prompts, representative calibration data, canonical equivalence checking, and language- or risk-specific thresholds.
Limitations & Outlook
Guarantees are marginal and expectation-based, and require calibration–test exchangeability. Embedding kNN screening detects atypicality but cannot guarantee detection of all gradual, semantic, or adversarial shifts. Ties and small calibration sets raise the feasibility floor; very stringent budgets may cause total abstention. GPT-based back-translation, judging, and repeated sampling add computation and possible evaluator bias. Benchmark results and cross-tier shifts do not yet establish closed-loop safety in physical robots.
Plain Language Accessible to non-experts
Imagine an airport that converts travelers’ handwritten trip plans into routes used by an automated transport system. The first checkpoint asks whether the trip looks like journeys the airport has seen before; an unusual plan is paused rather than processed blindly. For ordinary-looking plans, the system converts the machine route back into everyday language and checks whether it still matches the traveler’s intention. It also plans the route five times. If the five routes mostly mean the same thing, confidence rises; if they scatter, the plan is suspicious.
The airport does not choose a cutoff by intuition. It studies a collection of past plans whose correct routes are known, then sets the strictest rule that keeps the fraction of wrong routes released below a chosen budget. A rejected plan is not a failure: it is a safety decision requesting clarification. In the paper, this combined check separates wrong STL and SpaTiaL translations with scores of 0.706 and 0.920, while releasing 34.7% and 88.9% of outputs at a 10% risk budget.
ELI14 Explained like you're 14
Suppose you tell a game robot: “Pick up the key, avoid the monster, and reach the door within ten seconds.” The robot must turn that sentence into exact rules. If it misunderstands “ten seconds” as “ten minutes,” the rule may look perfectly legal but still make the robot lose.
SCP-NL2TL is like a translator with a panic button. First it asks whether your request resembles examples it has seen. If it is totally unfamiliar, it pauses. Then it translates the rule back into normal language: does it still sound like what you asked? It also translates the same request five times. If the answers agree, that is reassuring; if they jump around, something may be wrong.
A practice set with known answers determines the release line. Good-enough rules go to the robot; questionable ones trigger “Please explain that again!” The paper tests STL, LTL, and SpaTiaL. The combined error-detection score reaches 0.920 on SpaTiaL, so the two checks work better together than alone.
Is it perfect? Nope! New kinds of sentences can still confuse it, and asking several language models costs time. But for a robot or self-driving car, stopping before a dangerous guess is often much smarter than confidently doing the wrong thing!
Glossary
Selective Conformal Prediction
A reliability framework that lets a model answer or abstain. Calibration data provide statistical control over accepted errors.
SCP-NL2TL uses it to decide whether a generated formula may reach the planner.
Conformal Risk Control (CRC)
A conformal method for calibrating bounded monotone losses, not only prediction-set coverage. It converts a score into a risk-constrained threshold.
The paper applies it to loss 1[S≤τ]z.
Back-translation
The generated formal formula is translated back into natural language for comparison with the original instruction. It tests semantic fidelity rather than token confidence.
It produces Sbt.
Self-consistency
Repeated stochastic outputs are compared to see whether they share the same meaning. Exact equivalence is determined after logic-specific canonicalization.
Five samples produce Ssc.
Joint risk
The probability that an output is both accepted and incorrect: Rjoint=E[gz]. It measures errors that actually reach execution.
CRC constrains this quantity by α.
STL, LTL, SpaTiaL
Signal Temporal Logic, Linear Temporal Logic, and geometric Spatio-Temporal Logic. They formalize temporal, signal-based, and spatial requirements.
They test cross-language generality.
Open Questions Unanswered questions from this research
- 1 How can selective translation obtain conditional guarantees under persistent drift and non-exchangeability, rather than relying on detection of only conspicuous outliers?
- 2 How should LLM back-translation and judging be audited or replaced with formal semantic validators to control prompt sensitivity and evaluator bias?
- 3 In closed-loop robots, how should risk budget, abstention rate, latency, and user-escalation cost be optimized jointly?
Applications
Immediate Applications
Robot planning gate
A robot can screen a user instruction, generate STL/LTL/SpaTiaL, verify its meaning, and execute only accepted formulas. Abstentions can request clarification or human approval. Prerequisites include representative calibration data, fixed prompts, and an equivalence checker.
Industrial and autonomous-system rules
Engineers can translate operating requirements into formal constraints and use CRC to regulate which constraints enter verification or planning. Separate calibration by language and safety tier can align acceptance with the consequence of failure.
Long-term Vision
Trustworthy natural-language control
The longer-term vision is a cross-logic interface that generates formal requirements, reports calibrated uncertainty, asks for clarification, and leaves an auditable trail. Obstacles include real-world distribution shift, computational cost, adversarial language, and physical-system validation.
Abstract
Translating natural language instructions into machine-interpretable formal specifications enables robots and autonomous systems to plan, reason, and formally verify their behavior. However, existing translation models typically generate a specification for every input, even when the result is unreliable or fails to capture the user's intent, creating risks in safety-critical applications. Inspired by selective conformal prediction, we propose a selective translation framework that not only generates formal specifications but also determines when they can be trusted. Reliability is scored by two complementary black-box signals, the fidelity of the specification back-translated into natural language and the dispersion of repeated translations under exact semantic equivalence, which fail on different errors and jointly separate incorrect translations more sharply than either alone. Conformal risk control calibrates this score into a decision that accepts a specification or abstains, with a distribution-free bound on the rate at which incorrect specifications are accepted for execution, and a conformal anomaly detector on instruction embeddings screens out-of-distribution inputs before any translation is attempted. The proposed framework is general across formal specification languages, with experiments on Signal Temporal Logic (STL), Linear Temporal Logic (LTL), and geometric Spatio-Temporal Logic (SpaTiaL) demonstrating improved translation reliability, robustness under the evaluated cross-tier shifts, and effective uncertainty-aware abstention. This work establishes a foundation for trustworthy natural language interfaces by enabling AI systems to recognize when generated specifications may not be reliable.