SCP-NL2TL: Selective Conformal Prediction with Semantic Verification for Natural Language to Temporal Logic Specifications

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.

Motivation 

Existing NL2TL systems typically generate a formal specification for every instruction, even when the result is syntactically valid but semantically inconsistent with the user’s intent. Dataset-level accuracy does not indicate whether a particular translation is reliable, and black-box translators often provide no usable confidence score. Since downstream systems require a single executable formula rather than a set of candidates, reliable NL2TL translation requires an explicit accept-or-abstain mechanism that controls the risk of executing incorrect specifications. 

Experiments

1. Benchmarks: We evaluate STL, LTL, and SpaTiaL across three difficulty tiers using disjoint calibration and test sets.

2. Translators: We test both a GPT-5.2 few-shot translator and a fine-tuned LLaMA-3-8B translator to cover different error regimes.

3. Scoring and calibration: We compare back-translation, self-consistency, and their fusion, then evaluate CRC against a Split CP baseline using joint risk and acceptance rate.

4. Distribution shift: We test the instruction-level filter under cross-tier shifts with frozen calibration thresholds.

Results