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

Translating natural language into formal specifications lets robots and autonomous systems plan, reason, and verify behavior, but current models generate a specification for every input even when it is unreliable. The authors propose a selective translation framework inspired by selective conformal prediction, which generates specifications but also decides when to abstain. Reliability is scored using two black-box signals: fidelity of back-translation into natural language and dispersion of repeated translations under exact semantic equivalence. These signals fail on different errors and jointly separate incorrect translations more sharply than either alone. Conformal risk control calibrates this score into an accept-or-abstain decision with a distribution-free bound on the rate of accepting incorrect specifications. A conformal anomaly detector on instruction embeddings filters out-of-distribution inputs before translation. Experiments across Signal Temporal Logic (STL), Linear Temporal Logic (LTL), and geometric Spatio-Temporal Logic (SpaTiaL) show improved reliability, robustness under cross-tier shifts, and effective uncertainty-aware abstention. The work lays a foundation for trustworthy natural language interfaces by helping AI systems recognize when generated specifications may be unreliable.