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

• URL: http://arxiv.org/abs/2608.05439v1
• Date: Wed, 05 Aug 2026 22:17:09 GMT
• Title: SCP-NL2TL: Selective Conformal Prediction with Semantic Verification for Natural Language to Temporal Logic Specifications
• Abstract summary: Translating natural language instructions into machine-interpretable formal specifications enables robots and autonomous systems to plan, reason, and formally verify their behavior.<n>Existing translation models typically generate a specification for every input, even when the result is unreliable or fails to capture the user's intent.<n>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.
• Score: 28.546702829415207
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Inference-Time Steering for Cross-Lingual Factual Consistency in LLMs [51.56484100374058]
  Large Language Models (LLMs) demonstrate remarkable multilingual fluency, but their internal knowledge representations remain disproportionately biased toward high-resource languages.<n>We investigate whether these biases can be mitigated at inference time, forcing an English-prompted model to answer as if it were queried in target languages.<n>Experiments on Gemma 3 12B Instruct reveal persona prompting to be the strongest overall intervention, balancing efficacy, safety, and out-of-domain generalization.
  arXiv  Detail & Related papers  (2026-07-21T16:15:05Z)
• VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents [57.240036084348354]
  We introduce VASO, a framework for verification-guided self-evolution of robot skill contracts.<n>VASO verifies logically inconsistent skill contracts, then verifies plans induced by the skill against global and local temporal specifications.<n>On Clearpath Jackal and PX4 quadcopter tasks, VASO reaches 97.2% formal-specification compliance using fewer than 100 optimization samples.
  arXiv  Detail & Related papers  (2026-06-03T20:02:35Z)
• NeuroNL2LTL: A Neurosymbolic Framework for Natural Language Translation of Linear Temporal Logic [0.0]
  We present NeuroNL2LTL, a neurosymbolic architecture unifying learned translation with formal verification.<n>On 200,000+ requirements spanning aerospace, robotics, autonomous vehicles, and ten additional domains, NeuroNL2LTL achieves 28% semantic equivalence with reference specifications.
  arXiv  Detail & Related papers  (2026-05-20T03:31:51Z)
• Uncertainty-Aware Transformers: Conformal Prediction for Language Models [4.464939140209426]
  This article presents an uncertainty quantification framework for transformer-based language models.<n>CONFIDE applies conformal prediction to the internal embeddings of encoder-only architectures like BERT and RoBERTa.<n>We show that early and intermediate transformer layers often yield better-calibrated and more semantically meaningful representations for conformal prediction.
  arXiv  Detail & Related papers  (2026-04-10T02:48:50Z)
• LTLGuard: Formalizing LTL Specifications with Compact Language Models and Lightweight Symbolic Reasoning [2.365021420497964]
  Translating informal requirements into formal specifications is challenging due to the ambiguity and variability of natural language (NL)<n>In this work, we focus on enabling resource-efficient open-weight models to generate correct temporal logic (LTL) specifications from informal requirements.<n>We presentGuard, a modular toolchain that combines constrained generation with formal consistency checking to generate conflict-free specifications from informal input.
  arXiv  Detail & Related papers  (2026-03-05T22:34:45Z)
• STEAD: Robust Provably Secure Linguistic Steganography with Diffusion Language Model [71.35577462669856]
  We propose a robust, provably secure linguistic steganography with diffusion language models (DLMs)<n>We introduce error correction strategies, including pseudo-random error correction and neighborhood search correction, during steganographic extraction.
  arXiv  Detail & Related papers  (2026-01-21T08:58:12Z)
• Do What? Teaching Vision-Language-Action Models to Reject the Impossible [53.40183895299108]
  Vision-Language-Action (VLA) models have demonstrated strong performance on a range of robotic tasks.<n>We propose Instruct-Verify-and-Act (IVA), a framework that detects when an instruction cannot be executed due to a false premise.<n>Our experiments show that IVA improves false premise detection accuracy by 97.56% over baselines.
  arXiv  Detail & Related papers  (2025-08-22T10:54:33Z)
• Evaluating Multilingual and Code-Switched Alignment in LLMs via Synthetic Natural Language Inference [2.172419551358714]
  Large language models (LLMs) are increasingly applied in multilingual contexts, yet their capacity for consistent, logically grounded alignment across languages remains underexplored.<n>We present a framework for multilingual natural language inference that generates synthetic, logic-based premise-hypothesis pairs and translates them into a typologically diverse set of languages.<n>Code-switching does not degrade, and can even improve, performance, suggesting that translation-induced lexical variation may serve as a regularization signal.
  arXiv  Detail & Related papers  (2025-08-20T14:30:34Z)
• SConU: Selective Conformal Uncertainty in Large Language Models [59.25881667640868]
  We propose a novel approach termed Selective Conformal Uncertainty (SConU)<n>We develop two conformal p-values that are instrumental in determining whether a given sample deviates from the uncertainty distribution of the calibration set at a specific manageable risk level.<n>Our approach not only facilitates rigorous management of miscoverage rates across both single-domain and interdisciplinary contexts, but also enhances the efficiency of predictions.
  arXiv  Detail & Related papers  (2025-04-19T03:01:45Z)
• Conformal Linguistic Calibration: Trading-off between Factuality and Specificity [41.45862052156885]
  We present a framework connecting abstention and linguistic calibration through the lens of linguistic pragmatics.<n>Results demonstrate our method produces calibrated outputs with conformal guarantees on factual accuracy.
  arXiv  Detail & Related papers  (2025-02-26T13:01:49Z)
• Decomposing Uncertainty for Large Language Models through Input Clarification Ensembling [69.83976050879318]
  In large language models (LLMs), identifying sources of uncertainty is an important step toward improving reliability, trustworthiness, and interpretability. In this paper, we introduce an uncertainty decomposition framework for LLMs, called input clarification ensembling. Our approach generates a set of clarifications for the input, feeds them into an LLM, and ensembles the corresponding predictions.
  arXiv  Detail & Related papers  (2023-11-15T05:58:35Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.