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

# SCP-NL2TL: Selective Conformal Prediction with Semantic Verification for Natural Language to Temporal Logic Specifications
Source: [https://arxiv.org/html/2608.05439](https://arxiv.org/html/2608.05439)
Yixuan Wang1, Licheng Luo1, Yu Fu1, Kaidi Xu2, Yue Dong1, Mingyu Cai1 1University of California, Riverside, Riverside, CA, USA 2City University of Hong Kong, Hong Kong SAR, China ywang1457@ucr\.edu, lichengl@ucr\.edu, yfu093@ucr\.edu kaidixu at cityu\.edu\.hk, yue\.dong@ucr\.edu, mingyuc@ucr\.edu

###### 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\. Project materials are available at[sites\.google\.com/ucr\.edu/scpnl2tl](https://sites.google.com/ucr.edu/scpnl2tl?usp=sharing)\.

*Keywords*Natural Language to Temporal Logic Translation⋅\\cdotConformal Risk Control⋅\\cdotSelective Prediction

## 1Introduction

Translating natural language instructions into machine\-interpretable formal specifications enables robots and autonomous systems to plan, reason, and formally verify their behavior\[[57](https://arxiv.org/html/2608.05439#bib.bib41),[41](https://arxiv.org/html/2608.05439#bib.bib42),[6](https://arxiv.org/html/2608.05439#bib.bib43),[58](https://arxiv.org/html/2608.05439#bib.bib44)\]\. Formal languages such as Linear Temporal Logic \(LTL\), Signal Temporal Logic \(STL\), and geometric Spatio\-Temporal Logic \(SpaTiaL\) provide representations of temporal and spatial requirements\[[37](https://arxiv.org/html/2608.05439#bib.bib21),[32](https://arxiv.org/html/2608.05439#bib.bib33),[36](https://arxiv.org/html/2608.05439#bib.bib35)\], but writing them requires formal methods expertise\. Recent natural language to temporal logic \(NL2TL\) systems have made this process more accessible using semantic parsing, sequence models, and, more recently, pretrained language models with structured intermediate representations\[[20](https://arxiv.org/html/2608.05439#bib.bib4),[7](https://arxiv.org/html/2608.05439#bib.bib5),[31](https://arxiv.org/html/2608.05439#bib.bib6)\]\. Although these methods substantially improve translation accuracy and structural validity, they invariably generate a specification for every input\.

Always producing a specification is undesirable in safety\-critical applications\. A formula may be syntactically valid yet semantically incorrect by assigning an incorrect predicate, argument, temporal operator, interval, logical scope, or spatial relation, causing downstream planners or verifiers to execute behavior that does not reflect the user’s intent\. A practical NL2TL system should therefore determine not only what specification to generate, but also whether it is sufficiently reliable to be executed\. Standard evaluation metrics offer no such judgment, as exact\-match accuracy characterizes average benchmark performance rather than the trustworthiness of an individual translation\[[43](https://arxiv.org/html/2608.05439#bib.bib45),[8](https://arxiv.org/html/2608.05439#bib.bib46),[60](https://arxiv.org/html/2608.05439#bib.bib47),[42](https://arxiv.org/html/2608.05439#bib.bib48)\]\. Conformal prediction \(CP\) supplies the statistical machinery for such a judgment\. From any heuristic score and a set of calibration examples, it produces a prediction set that covers the true label at a user\-specified rate, requiring only that calibration and test data be exchangeable\[[48](https://arxiv.org/html/2608.05439#bib.bib25)\]\. The guarantee, however, is stated over sets, and a planner executes one formula rather than weighing several\[[17](https://arxiv.org/html/2608.05439#bib.bib49),[23](https://arxiv.org/html/2608.05439#bib.bib50)\]; a set of candidate specifications has nothing to hand it\. Recent work has redirected this machinery from covering an answer toward declining to give one\. Conformal risk control generalizes the coverage target to any bounded monotone loss\[[1](https://arxiv.org/html/2608.05439#bib.bib24)\], and selective conformal procedures add a second decision ahead of the first, testing whether the calibration data speak for a given test point and withholding a response when they do not\[[55](https://arxiv.org/html/2608.05439#bib.bib39)\]\. Across this line, abstention becomes an outcome the procedure is calibrated to produce rather than an admission that it failed\.

We propose a selective layer to any translator that either returns or withholds its generated formula, calibrating the decision so the rate of incorrect specifications reaching execution satisfies a user\-defined risk budget\. Unlike prior conformal methods that calibrate prediction sets using model confidence, our framework treats the translator as a black box and directly controls the risk of the single specification executed by the planner\. Instead of relying on token likelihoods, we score translations using two complementary semantic signals: back\-translation, which measures agreement with the instruction, and repeated sampling, which measures semantic consistency across translations\. An instruction\-level conformal test further rejects out\-of\-distribution inputs before translation\. Across STL, LTL, and SpaTiaL, our method consistently satisfies the target risk budget, while coverage\-calibrated baselines do not, and the instruction\-level filter further improves robustness under distribution shift\. The core contributions can be summarized as follows:

- •To the best of our knowledge, this is the first selective translation framework for NL2TL that augments any translator with an accept\-or\-abstain mechanism and bounds the rate at which incorrect temporal logic specifications are accepted for execution\.
- •We introduce a semantic consistency score that combines back\-translation fidelity and semantic agreement across repeated translations, improving discrimination between correct and incorrect specifications\.
- •We incorporate an instruction\-level conformal anomaly detector before calibration to identify out\-of\-distribution inputs, bound in\-distribution deferrals, and improve robustness under distribution shift\.

Related Work\.Translating natural language into formal task specifications has been studied using grammar\-based methods, semantic parsing, and sequence models for robotics and cyber\-physical systems\[[39](https://arxiv.org/html/2608.05439#bib.bib1),[18](https://arxiv.org/html/2608.05439#bib.bib2),[49](https://arxiv.org/html/2608.05439#bib.bib3),[20](https://arxiv.org/html/2608.05439#bib.bib4)\]\. Recent approaches leverage pretrained language models, structured intermediate representations, retrieval augmentation, model\-checker feedback, and grammar\-constrained decoding to improve translation accuracy and structural validity\[[7](https://arxiv.org/html/2608.05439#bib.bib5),[10](https://arxiv.org/html/2608.05439#bib.bib14),[33](https://arxiv.org/html/2608.05439#bib.bib15),[13](https://arxiv.org/html/2608.05439#bib.bib16),[12](https://arxiv.org/html/2608.05439#bib.bib17),[31](https://arxiv.org/html/2608.05439#bib.bib6),[16](https://arxiv.org/html/2608.05439#bib.bib38)\]\. These methods focus on generating or refining executable specifications, but they always return a formula regardless of its reliability\. ConformalNL2LTL attains a guaranteed translation success rate by building the formula through conformal QA steps that escalate uncertain decisions to a stronger model or the user\[[46](https://arxiv.org/html/2608.05439#bib.bib37)\]\. Our work is complementary: instead of modifying the translator, we develop a model\-agnostic selection layer that determines whether a generated specification should be accepted or withheld\.

Conformal prediction has recently been applied to language models for generation sets, prompt selection, API\-only uncertainty estimation, response validity, factuality, and selective generation\[[44](https://arxiv.org/html/2608.05439#bib.bib11),[54](https://arxiv.org/html/2608.05439#bib.bib10),[38](https://arxiv.org/html/2608.05439#bib.bib7),[34](https://arxiv.org/html/2608.05439#bib.bib8),[61](https://arxiv.org/html/2608.05439#bib.bib9),[9](https://arxiv.org/html/2608.05439#bib.bib20)\]\. Related work has also studied semantic uncertainty\[[15](https://arxiv.org/html/2608.05439#bib.bib12)\], conformal procedures under non\-exchangeability and distribution shift\[[14](https://arxiv.org/html/2608.05439#bib.bib13),[47](https://arxiv.org/html/2608.05439#bib.bib18),[3](https://arxiv.org/html/2608.05439#bib.bib19)\], and conformal significance testing for uncertainty outlier detection\[[55](https://arxiv.org/html/2608.05439#bib.bib39)\]\. A parallel line acquires specifications from system behavior rather than language, learning STL formulas through differentiable robustness and neural structures\[[24](https://arxiv.org/html/2608.05439#bib.bib54),[26](https://arxiv.org/html/2608.05439#bib.bib55),[25](https://arxiv.org/html/2608.05439#bib.bib56),[30](https://arxiv.org/html/2608.05439#bib.bib57)\], with conformal prediction certifying the inferred formulas\[[27](https://arxiv.org/html/2608.05439#bib.bib53),[53](https://arxiv.org/html/2608.05439#bib.bib52)\]\. Conformal risk control further extends conformal calibration from coverage guarantees to bounded monotone losses\[[1](https://arxiv.org/html/2608.05439#bib.bib24)\]\. The language\-model frameworks calibrate over a prediction set and derive their nonconformity from model confidence, token likelihoods, or sampled responses, none of which is available for a black\-box translator whose output is a single executable formula\. Conformal prediction has also entered language\-instructed robot planning, calibrating when an LLM planner should proceed, seek help, or escalate\[[51](https://arxiv.org/html/2608.05439#bib.bib58),[50](https://arxiv.org/html/2608.05439#bib.bib59),[40](https://arxiv.org/html/2608.05439#bib.bib60),[28](https://arxiv.org/html/2608.05439#bib.bib61)\]\.

Selective conformal procedures add a decision ahead of the conformal one\. SConU tests each incoming sample against the uncertainty distribution of the calibration set and declines to answer when the evidence for exchangeability is insufficient\[[55](https://arxiv.org/html/2608.05439#bib.bib39)\], building on conformal outlier testing\[[4](https://arxiv.org/html/2608.05439#bib.bib30),[21](https://arxiv.org/html/2608.05439#bib.bib31)\]and on rank\-based anomaly detection under exchangeability\[[22](https://arxiv.org/html/2608.05439#bib.bib28)\]\. A related line pursues conditional rather than marginal risk guarantees through two\-stage calibration, at the cost of a modified exchangeability requirement\[[56](https://arxiv.org/html/2608.05439#bib.bib32)\]\. Nearest neighbours in embedding space serve as an out\-of\-distribution statistic in the detection literature independently of conformal calibration\[[45](https://arxiv.org/html/2608.05439#bib.bib27)\]\. We place such a statistic inside the admission gate, computed from the instruction alone so that screening precedes translation, and calibrate what follows it on the rate at which incorrect specifications are accepted\.

## 2Background and Problem

Formal Logic Languages\.Temporal Logic \(TL\) specifications as formal languages provide mathematically precise descriptions of desired system behaviors, enabling automated planning and formal verification for autonomous and cyber\-physical systems\[[37](https://arxiv.org/html/2608.05439#bib.bib21),[2](https://arxiv.org/html/2608.05439#bib.bib22),[5](https://arxiv.org/html/2608.05439#bib.bib23)\]\. Unlike natural language, which is inherently ambiguous, a formal specification has well\-defined syntax and semantics, allowing its correctness to be rigorously analyzed and verified\. LetΦ\\Phidenote the space of well\-formed formulas in a target formal language\. Although numerous formal specification languages have been proposed, including LTL\[[37](https://arxiv.org/html/2608.05439#bib.bib21)\], STL\[[32](https://arxiv.org/html/2608.05439#bib.bib33)\], and SpaTiaL\[[36](https://arxiv.org/html/2608.05439#bib.bib35)\], they share a common compositional structure\. A specification is recursively constructed from*atomic predicates*,*Boolean operators*, and*domain\-specific operators*, such as temporal or spatial modalities:

φ::=μ∣¬φ∣φ1∧φ2∣φ1∨φ2∣𝒪\(φ\),\\varphi::=\\mu\\mid\\neg\\varphi\\mid\\varphi\_\{1\}\\land\\varphi\_\{2\}\\mid\\varphi\_\{1\}\\lor\\varphi\_\{2\}\\mid\\mathcal\{O\}\(\\varphi\),\(1\)whereμ\\muis an atomic predicate and𝒪\\mathcal\{O\}denotes one or more logic\-specific operators\. For example, LTL employs temporal operators such asEventually\(𝐅\\mathbf\{F\}\),Always\(𝐆\\mathbf\{G\}\), andUntil\(𝐔\\mathbf\{U\}\); STL augments these operators with bounded time intervals over continuous\-valued signals; and SpaTiaL further introduces geometric predicates and spatial operators\. Each logic pairs this grammar with a formal semantics specifying when a system trajectory satisfies a specification, which is what makes generated formulas executable and verifiable downstream\.

Natural Language to Formal Specification\.

Given a natural language instructionu∈𝒰u\\in\\mathcal\{U\}, NL2TL aims to generate a formal specificationφ^=fθ​\(u\)∈Φ\\hat\{\\varphi\}=f\_\{\\theta\}\(u\)\\in\\Phi\. Most approaches learn the conditional distributionpθ​\(φ\|u\)p\_\{\\theta\}\(\\varphi\|u\)and predict the most likely specification\[[7](https://arxiv.org/html/2608.05439#bib.bib5),[10](https://arxiv.org/html/2608.05439#bib.bib14),[33](https://arxiv.org/html/2608.05439#bib.bib15),[31](https://arxiv.org/html/2608.05439#bib.bib6)\], but the predicted formula may be syntactically valid while failing to preserve the semantic intent of the instruction, and likelihood underpθp\_\{\\theta\}offers no measure of this semantic correctness\[[11](https://arxiv.org/html/2608.05439#bib.bib62)\]\.

Conformal Prediction \(CP\)\.CP provides a model\-agnostic framework for quantifying prediction reliability with finite\-sample, distribution\-free guarantees\[[48](https://arxiv.org/html/2608.05439#bib.bib25)\]\. Given a calibration set and a nonconformity scores​\(x,y\)s\(x,y\), CP computes a threshold from calibration scores and constructs a prediction set𝒞α​\(x\)=\{y:s​\(x,y\)≤q^\},\\mathcal\{C\}\_\{\\alpha\}\(x\)=\\\{y:s\(x,y\)\\leq\\hat\{q\}\\\},which satisfiesPr⁡\(Y∈𝒞α​\(X\)\)≥1−α\\Pr\\\!\\left\(Y\\in\\mathcal\{C\}\_\{\\alpha\}\(X\)\\right\)\\geq 1\-\\alphaunder exchangeability\. While this guarantee ensures the correct label is contained in the prediction set with high probability, it is not directly suitable for NL2TL, where downstream planners typically require a single executable formal specification rather than a set of candidates\. This limitation motivates conformal methods tailored to selective and reliable formal specification generation\.

Problem Formulation\.Letx∈𝒳x\\in\\mathcal\{X\}be a natural\-language instruction and letΦ\\Phibe the space of well\-formed formulas in a target specification language, as in the preliminaries; the formulation applies to any logic generated by the grammar in Eq\.[1](https://arxiv.org/html/2608.05439#S2.E1), with STL, LTL, and SpaTiaL serving as our experimental instances\. A translatorφ^=f​\(x\)∈Φ\\hat\{\\varphi\}=f\(x\)\\in\\Phiis treated as a black box: the framework uses only the final pair\(x,φ^\)\(x,\\hat\{\\varphi\}\), with no access to parameters, likelihoods, or internal states\. The translator may be of any construction\[[31](https://arxiv.org/html/2608.05439#bib.bib6),[29](https://arxiv.org/html/2608.05439#bib.bib36),[7](https://arxiv.org/html/2608.05439#bib.bib5)\]; only the instruction and the final formula enter the framework\. We augmentffwith a selection functiong​\(x,φ^\)∈\{0,1\}g\(x,\\hat\{\\varphi\}\)\\in\\\{0,1\\\}, whereg=1g=1indicates thatφ^\\hat\{\\varphi\}is returned andg=0g=0indicates abstention\. Letφ⋆\\varphi^\{\\star\}denote the reference formula and define the translation error asz​\(x,φ^,φ⋆\)=𝟏​\[φ^≢φ⋆\]z\(x,\\hat\{\\varphi\},\\varphi^\{\\star\}\)=\\mathbf\{1\}\\\!\\left\[\\hat\{\\varphi\}\\not\\equiv\\varphi^\{\\star\}\\right\], where≡\\equivis the semantic\-equivalence criterion of the target benchmark\. The selective translator is evaluated by its joint risk and coverage,

ℛjoint=𝐄​\[g​\(x,φ^\)⋅z​\(x,φ^,φ⋆\)\],𝒞=𝐏​\(g​\(x,φ^\)=1\)\.\\mathcal\{R\}\_\{\\mathrm\{joint\}\}=\\mathbf\{E\}\\\!\\left\[\\,g\(x,\\hat\{\\varphi\}\)\\cdot z\(x,\\hat\{\\varphi\},\\varphi^\{\\star\}\)\\,\\right\],\\qquad\\mathcal\{C\}=\\mathbf\{P\}\\\!\\left\(g\(x,\\hat\{\\varphi\}\)=1\\right\)\.\(2\)The joint risk is the probability that a translation is both accepted and incorrect, taken over the full input stream rather than over the accepted subset; an abstention contributes zero regardless of the underlying error\.

Challenges and Motivation\.Designing a conformal framework for NL2TL differs fundamentally from standard classification\. First, the output spaceΦ\\Phiis effectively unbounded, making prediction sets impractical while downstream planners require a single executable specification or abstention\. Second, the objective is selective risk rather than coverage: standard conformal prediction guarantees that the correct specification belongs to a prediction set but does not control the probability that an accepted translation is incorrect, nor the joint rate at which incorrect translations reach execution\. Third, conventional nonconformity scores depend on model confidences or token likelihoods, which are unavailable for black\-box translators and often poorly aligned with semantic correctness\. Therefore, reliable NL2TL requires a framework that \(i\) performs accept\-or\-abstain decisions instead of prediction\-set construction, \(ii\) calibrates acceptance risk rather than set coverage, and \(iii\) uses scores computable solely from the instruction and the generated specification\.

## 3Methodology

![Refer to caption](https://arxiv.org/html/2608.05439v1/x1.png)Figure 1:Overview of the selective translation framework: instructions are screened before translation \(levelδ\\delta\), scored by two complementary signals after it, and returned only when a threshold calibrated to the joint\-risk budgetα\\alphaadmits the evidence\.Conformal risk control \(CRC\)\[[1](https://arxiv.org/html/2608.05439#bib.bib24)\]extends conformal calibration from coverage guarantees to arbitrary bounded monotone losses by selecting the largest acceptance threshold whose expected loss remains below a prescribed budget under exchangeability\. However, CRC provides only the calibration mechanism, not the scoring function, selection criterion, or robustness to distribution shift\. Building on CRC, we propose a black\-box conformal selection framework that augments any NL2TL translator with an accept\-or\-abstain decision layer: an instruction\-level screen, two semantic scores, and a calibrated threshold \(Fig\.[1](https://arxiv.org/html/2608.05439#S3.F1)\)\. The objective is to maximize acceptance subject to a prescribed budgetα∈\(0,1\)\\alpha\\in\(0,1\)on the joint risk of Eq\.[2](https://arxiv.org/html/2608.05439#S2.E2):

maxg⁡𝒞s\.t\.ℛjoint≤α\.\\max\_\{g\}\\;\\mathcal\{C\}\\qquad\\text\{s\.t\.\}\\qquad\\mathcal\{R\}\_\{\\mathrm\{joint\}\}\\leq\\alpha\.\(3\)
### 3\.1Semantic Consistency Scoring

The decision function in Eq\.[3](https://arxiv.org/html/2608.05439#S3.E3)requires a scalar nonconformity score computed from the instruction–translation pair\(x,φ^\)\(x,\\hat\{\\varphi\}\)that assigns higher values to less reliable translations\. Our default score is based on back\-translation\. A back\-translatorBB\(an LLM prompted with the target logic\) convertsφ^\\hat\{\\varphi\}into natural language,u^=B​\(φ^\)\\hat\{u\}=B\(\\hat\{\\varphi\}\), and an LLM judge evaluates its semantic consistency with the original instruction across four dimensions: logical structure, temporal operators, time constraints, and overall meaning\. The average agreementA​\(x,u^\)∈\[0,1\]A\(x,\\hat\{u\}\)\\in\[0,1\]defines the nonconformity score

Sbt​\(x,φ^\)=1−A​\(x,B​\(φ^\)\)\.S\_\{\\mathrm\{bt\}\}\(x,\\hat\{\\varphi\}\)=1\-A\\left\(x,B\(\\hat\{\\varphi\}\)\\right\)\.\(4\)Invalid or unparsable formulas receive the maximum score,Sbt=1S\_\{\\mathrm\{bt\}\}=1, enforcing syntactic correctness before semantic evaluation\. This design isolates logic\-specific knowledge within the back\-translator, while the judge operates entirely in natural language, making the scoring pipeline applicable to any target logic generated by Eq\.[1](https://arxiv.org/html/2608.05439#S2.E1)\. The approach combines the round\-trip principle from machine translation\[[35](https://arxiv.org/html/2608.05439#bib.bib26)\]with the LLM\-as\-judge paradigm\[[59](https://arxiv.org/html/2608.05439#bib.bib51)\]\. Because back\-translation inspects only the final output, a complementary score measures the stability of repeated stochastic translations\. Givenkksamples, translator uncertainty is measured by

Ssc​\(x\)=1−1k​max1≤j≤k⁡\|\{m:φ^\(m\)≃φ^\(j\)\}\|,S\_\{\\mathrm\{sc\}\}\(x\)=1\-\\frac\{1\}\{k\}\\,\\max\_\{1\\leq j\\leq k\}\\;\\Bigl\|\\bigl\\\{\\,m:\\hat\{\\varphi\}^\{\(m\)\}\\simeq\\hat\{\\varphi\}^\{\(j\)\}\\,\\bigr\\\}\\Bigr\|,\(5\)where the maximum is the size of the largest cluster of mutually equivalent samples,≃\\simeqdenotes semantic equivalence under logic\-specific canonicalization, and invalid formulas are equivalent only to themselves\. This extends self\-consistency\[[52](https://arxiv.org/html/2608.05439#bib.bib40)\]to formal specifications, where equivalence can be checked exactly\[[15](https://arxiv.org/html/2608.05439#bib.bib12)\]\. SinceSbtS\_\{\\mathrm\{bt\}\}detects semantic mismatches whileSscS\_\{\\mathrm\{sc\}\}captures translation uncertainty, their equal\-weight fusion

Sfu=12​\(Sbt\+Ssc\)S\_\{\\mathrm\{fu\}\}=\\tfrac\{1\}\{2\}\\left\(S\_\{\\mathrm\{bt\}\}\+S\_\{\\mathrm\{sc\}\}\\right\)\(6\)provides the default reliability score\. When repeated sampling is unavailable, such as for deterministic or offline translators,SbtS\_\{\\mathrm\{bt\}\}alone can be used without changing the subsequent calibration procedure, which accepts any score in\[0,1\]\[0,1\]\.

### 3\.2Risk\-Calibrated Selection

The score orders translations by suspicion but does not say where acceptance should stop; that boundary must come from data\. A threshold is calibrated on translations whose outcomes are known,

𝒟cal\\displaystyle\\mathcal\{D\}\_\{\\mathrm\{cal\}\}=\{\(xi,φ^i,φi⋆\)\}i=1n,\\displaystyle=\\\{\(x\_\{i\},\\hat\{\\varphi\}\_\{i\},\\varphi\_\{i\}^\{\\star\}\)\\\}\_\{i=1\}^\{n\},\(7\)Si\\displaystyle S\_\{i\}=S​\(xi,φ^i\),zi=𝟏​\[φ^i≢φi⋆\],\\displaystyle=S\(x\_\{i\},\\hat\{\\varphi\}\_\{i\}\),\\qquad z\_\{i\}=\\mathbf\{1\}\\\!\\left\[\\hat\{\\varphi\}\_\{i\}\\not\\equiv\\varphi\_\{i\}^\{\\star\}\\right\],\(8\)whereSSis the deployed consistency score, either the fusionSfuS\_\{\\mathrm\{fu\}\}or the output\-onlySbtS\_\{\\mathrm\{bt\}\}\. A candidate thresholdτ\\tauaccepts every translation scoring at or below it, and its empirical joint risk on the calibration set is

ℛ^​\(τ\)=1n​∑i=1n𝟏​\[Si≤τ\]​zi\.\\widehat\{\\mathcal\{R\}\}\(\\tau\)=\\frac\{1\}\{n\}\\sum\_\{i=1\}^\{n\}\\mathbf\{1\}\\\!\\left\[S\_\{i\}\\leq\\tau\\right\]z\_\{i\}\.\(9\)
Every calibration sample contributes to this sum: an abstention counts zero, an accepted error counts one\. The quantity is therefore an average over the full sample rather than over the accepted subset, which is what permits the direct application of conformal risk control\. Following the calibration rule ofAngelopouloset al\.\[[1](https://arxiv.org/html/2608.05439#bib.bib24)\], the threshold is

τ^=max⁡\{τ∈𝒯:nn\+1​ℛ^​\(τ\)\+1n\+1≤α\},\\hat\{\\tau\}=\\max\\Bigl\\\{\\tau\\in\\mathcal\{T\}:\\tfrac\{n\}\{n\+1\}\\,\\widehat\{\\mathcal\{R\}\}\(\\tau\)\+\\tfrac\{1\}\{n\+1\}\\leq\\alpha\\Bigr\\\},\(10\)where𝒯\\mathcal\{T\}is the set of distinct calibration scores together with−∞\-\\infty, and ties are resolved by admitting all samples that share a score\. The correction term accounts for the unseen test point and is what turns an empirical constraint into a population guarantee\. At test time,

g​\(x,φ^\)=𝟏​\[S​\(x,φ^\)≤τ^\]\.g\(x,\\hat\{\\varphi\}\)=\\mathbf\{1\}\\\!\\left\[S\(x,\\hat\{\\varphi\}\)\\leq\\hat\{\\tau\}\\right\]\.\(11\)
###### Theorem 1\(Joint risk control\)\.

Fix a calibration group\. If the calibration pairs of this group and the test pair are exchangeable andτ^\\hat\{\\tau\}is chosen by Eq\.[10](https://arxiv.org/html/2608.05439#S3.E10)on this group’s calibration scores, then the decision rule of Eq\.[11](https://arxiv.org/html/2608.05439#S3.E11)satisfies, for test inputs of the same group,

ℛjoint=𝐄​\[g​\(X,φ^\)⋅Z\]≤α\.\\mathcal\{R\}\_\{\\mathrm\{joint\}\}=\\mathbf\{E\}\\\!\\left\[\\,g\(X,\\hat\{\\varphi\}\)\\cdot Z\\,\\right\]\\leq\\alpha\.

###### Proof\.

The lossℓτ=𝟏​\[S≤τ\]​z\\ell\_\{\\tau\}=\\mathbf\{1\}\[S\\leq\\tau\]\\,zis bounded in\[0,1\]\[0,1\]and non\-increasing asτ\\taudecreases, since lowering the threshold can only remove accepted samples\. The claim is the conformal risk control theorem ofAngelopouloset al\.\[[1](https://arxiv.org/html/2608.05439#bib.bib24)\]applied to this loss\. ∎

The guarantee in Theorem[1](https://arxiv.org/html/2608.05439#Thmtheorem1)holds in expectation over the calibration and test samples\. Consequently, a threshold that fully utilizes the risk budget will achieve expected risk close toα\\alpha, while individual realizations may exceedα\\alpha\. Feasibility depends on both the calibration size and score distribution\. Since the empirical risk is evaluated at resolution1n\+1\\tfrac\{1\}\{n\+1\}, risk budgets below this level cannot be certified, analogous to the minimum conformalpp\-value attainable withnncalibration samples\[[55](https://arxiv.org/html/2608.05439#bib.bib39),[48](https://arxiv.org/html/2608.05439#bib.bib25)\]\. Moreover, tied scores force samples to enter the acceptance region together\. If the smallest nonempty acceptance region containsL0L\_\{0\}calibration errors, a feasible threshold exists only when

α≥αℓ=L0\+1n\+1\.\\alpha\\geq\\alpha\_\{\\ell\}=\\frac\{L\_\{0\}\+1\}\{n\+1\}\.\(12\)Otherwise, Eq\.[10](https://arxiv.org/html/2608.05439#S3.E10)returnsτ^=−∞\\hat\{\\tau\}=\-\\infty, causing the system to abstain on every input rather than provide an uncertifiable guarantee\. Sinceαℓ\\alpha\_\{\\ell\}is determined entirely by the calibration data, feasibility can be assessed before deployment\. It can be improved by increasing the calibration set or relaxing the risk budget\. Calibrating each group separately in this way yields group\-conditional guarantees, at the cost of fewer calibration samples per group and thus a potentially largerαℓ\\alpha\_\{\\ell\}\.

Coverage is maximized by construction through the largest feasible threshold in Eq\.[10](https://arxiv.org/html/2608.05439#S3.E10)\. Its performance is naturally bounded by two references\. For a translator with error rateppunder budgetα\\alpha, the maximum achievable acceptance rate ismin⁡\(1,1−p\+α\)\\min\(1,\\,1\-p\+\\alpha\), attained by a perfect score that ranks all correct translations above all incorrect ones\. At the other extreme, an uninformative score achieves acceptance rateα/p\\alpha/pby accepting a random subset with the population error rate\. The realized acceptance rate therefore quantifies how closely the score approaches the optimal ranking\.

### 3\.3Filtering Out\-of\-Distribution Instructions

Theorem[1](https://arxiv.org/html/2608.05439#Thmtheorem1)assumes exchangeability between calibration and test data, an assumption that may fail under distribution shift\. We therefore introduce an upstream input filter that defers instructions outside the calibration distribution before translation and scoring\. Unlike the CRC threshold in Eq\.[10](https://arxiv.org/html/2608.05439#S3.E10), which abstains when translation evidence is insufficient, the filter abstains when no statistical guarantee can be provided\.

The filter measures the atypicality of an instruction using its embedding\. Scores are computed against a fixed reference set𝒳ref\\mathcal\{X\}\_\{\\mathrm\{ref\}\}of training\-sourced instructions, disjoint from the instructions on which the deferral level is calibrated and from the test stream\. Lete​\(x\)∈ℝde\(x\)\\in\\mathbb\{R\}^\{d\}denote the normalized embedding of instructionxx, and define its averagekk\-nearest\-neighbor distance to the reference set as

D​\(x\)=1k​∑xj∈𝒩k​\(x\)‖e​\(x\)−e​\(xj\)‖2,D\(x\)=\\frac\{1\}\{k\}\\sum\_\{x\_\{j\}\\in\\mathcal\{N\}\_\{k\}\(x\)\}\\bigl\\\|e\(x\)\-e\(x\_\{j\}\)\\bigr\\\|\_\{2\},\(13\)where𝒩k​\(x\)\\mathcal\{N\}\_\{k\}\(x\)is the set ofkknearest reference embeddings\. The same function scores themmdeferral\-calibration instructionsx1,…,xmx\_\{1\},\\ldots,x\_\{m\}and any test instruction, and the conformalpp\-value of a test instruction is

p​\(x\)=1\+∑i=1m𝟏​\[D​\(xi\)≥D​\(x\)\]m\+1,p\(x\)=\\frac\{1\+\\sum\_\{i=1\}^\{m\}\\mathbf\{1\}\\\!\\left\[D\(x\_\{i\}\)\\geq D\(x\)\\right\]\}\{m\+1\},\(14\)
###### Theorem 2\(Filter validity\)\.

If the test instruction is exchangeable with the deferral\-calibration instructions, then the filter defers it with probability at mostδ\\delta,

𝐏​\(p​\(X\)<δ\)≤δ\.\\mathbf\{P\}\\\!\\left\(p\(X\)<\\delta\\right\)\\leq\\delta\.

###### Proof\.

The score functionDDis fixed by𝒳ref\\mathcal\{X\}\_\{\\mathrm\{ref\}\}and depends on none ofx1,…,xmx\_\{1\},\\ldots,x\_\{m\}or the test instruction, so exchangeability of the instructions carries over to their scores\. The rank ofD​\(X\)D\(X\)among\{D​\(x1\),…,D​\(xm\),D​\(X\)\}\\\{D\(x\_\{1\}\),\\ldots,D\(x\_\{m\}\),D\(X\)\\\}is then uniformly distributed up to ties, and ties only enlargep​\(X\)p\(X\)through the inequality in Eq\.[14](https://arxiv.org/html/2608.05439#S3.E14), so𝐏​\(p​\(X\)<δ\)≤δ\\mathbf\{P\}\(p\(X\)<\\delta\)\\leq\\delta\. ∎

Theorem[2](https://arxiv.org/html/2608.05439#Thmtheorem2)guarantees that an in\-distribution instruction is deferred with probability at mostδ\\delta\. Under distribution shift, the filter removes detected atypical inputs before translation; Theorem[1](https://arxiv.org/html/2608.05439#Thmtheorem1)applies to the retained stream to the extent that its exchangeability with the calibration data is preserved\. Since no finite\-sample procedure can detect every shifted input, the filter replaces the assumption of no distribution shift with the weaker assumption that significant shifts are detected, and the residual risk under partial detection is evaluated experimentally\.

## 4Experimental Results

Table 1:Error\-detection AUROC by scoring channel, grouped by information source\. Best values in each column are shown in bold\. Darker cells indicate higher AUROC within each formalism\. TheΔ\\Deltarow reports the fusion margin over the best single channel\.†SpaTiaL D2 contains only seven incorrect translations, too few to estimate ranking quality reliably\. The bootstrap 95% confidence interval forSbtS\_\{\\mathrm\{bt\}\}spans\[0\.49,0\.96\]\[0\.49,0\.96\], so the reported values indicate at most the direction of the ranking\. No per\-column boldface orΔ\\Deltais shown for this column\.

#### Tasks and data\.

Three specification languages instantiate the framework: STL and interval\-free LTL from the NL2TL benchmark\[[7](https://arxiv.org/html/2608.05439#bib.bib5)\], and SpaTiaL from the NL2SpaTiaL benchmark\[[31](https://arxiv.org/html/2608.05439#bib.bib6)\]\. Each language is divided into three difficulty tiers \(D2–D4\)\. For SpaTiaL, tiers are determined during data generation by controlling the depth and branching of logical trees\[[31](https://arxiv.org/html/2608.05439#bib.bib6)\]\. For STL and LTL, tiers are defined post hoc by the number of atomic propositions in the reference formula \(at most two, three, and at least four\), serving as a proxy for logical complexity\. The tier labels indicate increasing difficulty within each language and are not comparable across languages\. For each random resplit 200 examples per tier are assigned to calibration and 150 disjoint examples to testing\. Paraphrases associated with the same reference formula are always kept in the same partition to prevent semantic leakage\. Translation correctness is determined using the benchmark\-provided canonical equivalence checker, which accounts for commutativity, De Morgan transformations, and argument\-order normalization\.

#### LLM Translators\.

Two translators spanning a wide reliability range are evaluated\. The first is the fine\-tuned LLaMA\-3\-8B model ofLuoet al\.\[[31](https://arxiv.org/html/2608.05439#bib.bib6)\], equipped with tier\-specific LoRA adapters, achieving a raw error rate of approximately15%15\\%\. The second is GPT\-5\.2 prompted with twenty in\-context examples for STL and LTL, following the few\-shot setup of the unfine\-tuned baselines inChenet al\.\[[7](https://arxiv.org/html/2608.05439#bib.bib5)\], with prompts and exemplars developed independently, yielding a48%48\\%error rate under semantic\-equivalence evaluation\. For completeness, the fine\-tuned T5 model ofChenet al\.\[[7](https://arxiv.org/html/2608.05439#bib.bib5)\]\(approximately2%2\\%error\) is included only to verify the applicability of the self\-consistency score, as its error rate is too low for meaningful tier\-level risk evaluation\.

#### Scoring and calibration configuration\.

Back\-translation uses GPT\-5\.2 with a prompt frozen before any evaluation run; judging uses GPT\-5\.4 with the four\-dimensional rubric defined above; self\-consistency drawsk=5k=5samples at temperature1\.01\.0\. STL and LTL share the same back\-translation and judging prompts, while SpaTiaL uses its own back\-translation prompt and a categorical rubric\. Within each language, prompts and rubric texts are fixed once and identical across translators and evaluation runs\. Thresholds are calibrated per language and tier\. Every reported risk and coverage figure is the mean over 100 random calibration–test resplits, with its standard error; the resplit protocol, the filtering levelδ=0\.05\\delta=0\.05, and the rule that marks a cell as borderline when its mean lies within one standard error ofα\\alphawere all fixed before either arm of any comparison was inspected\.

#### Baseline and metrics\.

The baseline adapts standard conformal calibration to selective prediction by applying the coverage\-based conformal quantile rule to the same nonconformity score and using the resulting threshold for acceptance\. Thus, both methods share the score, data, and decision rule, differing only in the calibration objective\. They are compared using three metrics: the joint risk in Eq\.[9](https://arxiv.org/html/2608.05439#S3.E9), the acceptance rate, and the number of resplits in which the realized joint risk exceedsα\\alpha\. The exceedance count reflects the expectation\-level nature of the guarantee rather than a failure\. The guarantee constrains the mean risk over resplits, not each realization, so a method that spends its budget operates nearα\\alphaand individual resplits land on either side; the count locates the operating point relative to the budget rather than measuring compliance\. Score quality is evaluated independently of calibration\. Let𝒫\\mathcal\{P\}and𝒩\\mathcal\{N\}denote the correct and incorrect translations within a tier\. We report

AUROC​\(S\)=1\|𝒫\|​\|𝒩\|​∑p∈𝒫∑q∈𝒩\(𝟏​\[S​\(q\)\>S​\(p\)\]\+12​𝟏​\[S​\(q\)=S​\(p\)\]\),\\displaystyle\\mathrm\{AUROC\}\(S\)=\\frac\{1\}\{\|\\mathcal\{P\}\|\\,\|\\mathcal\{N\}\|\}\\sum\_\{p\\in\\mathcal\{P\}\}\\sum\_\{q\\in\\mathcal\{N\}\}\\Bigl\(\\mathbf\{1\}\\\!\\left\[S\(q\)\>S\(p\)\\right\]\+\\tfrac\{1\}\{2\}\\mathbf\{1\}\\\!\\left\[S\(q\)=S\(p\)\\right\]\\Bigr\),\(15\)which equals the area under the ROC curve\[[19](https://arxiv.org/html/2608.05439#bib.bib29)\]\. AUROC measures the probability that the score ranks an incorrect translation above a correct one, assigning half credit to ties\. It ranges from0\.50\.5\(random ranking\) to11\(perfect separation\), is invariant to monotone score transformations, and is independent of any acceptance threshold or risk budget, making it well suited for comparing scoring methods before calibration\. Results are reported per tier, with bootstrap confidence intervals for low\-error cases and uninformative intervals explicitly marked\.

Table 2:From score to selective prediction\. AUROC↑\\uparrowis computed over all tiers\. The acceptance rate atα=0\.10\\alpha=0\.10and the feasibility floorαℓ\\alpha\_\{\\ell\}are calibrated on the three tiers of each language merged into a single calibration set \(n=600n=600\), and are therefore not comparable to the per\-tier compliance tables\.Table 3:Joint\-risk compliance under the stated calibration sizes\. Entries report mean joint risk±\\pmstandard error over 100 random calibration/test splits\. Green cells indicate clear CRC compliance; red cells indicate violations by more than one standard error; gray cells lie within one standard error of the target risk budget\. Uncolored Split CP cells are numerically below the risk budget but carry no joint\-risk guarantee\.*No sel\.*accepts all translations, and‡denotes full abstention when no valid CRC threshold exists\.TierNosel\.MethodRisk budgetα\\alpha0\.050\.100\.150\.200\.250\.30\(a\) STLGPT\-5\.2 few\-shot translatorD20\.423CRCabst\.‡0\.069±\\pm0\.006 ✓0\.133±\\pm0\.003 ✓0\.190±\\pm0\.004 ✓0\.243±\\pm0\.005 ✓0\.293±\\pm0\.005 ✓Split CP0\.349±\\pm0\.003 ✗0\.326±\\pm0\.003 ✗0\.312±\\pm0\.003 ✗0\.275±\\pm0\.003 ✗0\.252±\\pm0\.003†0\.237±\\pm0\.003D30\.434CRC0\.046±\\pm0\.002 ✓0\.097±\\pm0\.004†0\.151±\\pm0\.004†0\.192±\\pm0\.004 ✓0\.250±\\pm0\.005†0\.301±\\pm0\.005†Split CP0\.371±\\pm0\.003 ✗0\.329±\\pm0\.003 ✗0\.306±\\pm0\.003 ✗0\.296±\\pm0\.003 ✗0\.293±\\pm0\.003 ✗0\.278±\\pm0\.003D40\.551CRC0\.012±\\pm0\.003 ✓0\.094±\\pm0\.003 ✓0\.143±\\pm0\.003 ✓0\.184±\\pm0\.004 ✓0\.235±\\pm0\.004 ✓0\.291±\\pm0\.004 ✓Split CP0\.485±\\pm0\.004 ✗0\.373±\\pm0\.004 ✗0\.292±\\pm0\.004 ✗0\.233±\\pm0\.003 ✗0\.205±\\pm0\.0030\.183±\\pm0\.003\(b\) SpaTiaLfine\-tuned LLaMA translatorD20\.0372CRC0\.034±\\pm0\.001 ✓0\.035±\\pm0\.001 ✓0\.035±\\pm0\.001 ✓0\.035±\\pm0\.001 ✓0\.035±\\pm0\.001 ✓0\.035±\\pm0\.001 ✓Split CP0\.017±\\pm0\.0010\.016±\\pm0\.0010\.016±\\pm0\.0010\.016±\\pm0\.0010\.016±\\pm0\.0010\.013±\\pm0\.001D30\.149CRC0\.049±\\pm0\.002†0\.095±\\pm0\.004 ✓0\.140±\\pm0\.003 ✓0\.149±\\pm0\.002 ✓0\.149±\\pm0\.002 ✓0\.149±\\pm0\.002 ✓Split CP0\.052±\\pm0\.001 ✗0\.050±\\pm0\.0010\.046±\\pm0\.0010\.046±\\pm0\.0010\.040±\\pm0\.0010\.035±\\pm0\.001D40\.309CRC0\.046±\\pm0\.002 ✓0\.088±\\pm0\.003 ✓0\.138±\\pm0\.004 ✓0\.190±\\pm0\.004 ✓0\.242±\\pm0\.004 ✓0\.274±\\pm0\.005 ✓Split CP0\.066±\\pm0\.002 ✗0\.061±\\pm0\.0020\.055±\\pm0\.0020\.039±\\pm0\.0010\.034±\\pm0\.0010\.034±\\pm0\.001Scoring Ablation\.Although CRC can calibrate any score in\[0,1\]\[0,1\], its practical efficiency depends on both error\-ranking quality and score resolution\. We therefore evaluate ranking quality before calibration and then examine the operating behavior induced by each score\. Table[1](https://arxiv.org/html/2608.05439#S4.T1)reports per\-tier AUROC for the three proposed scores—back\-translation \(SbtS\_\{\\mathrm\{bt\}\}\), self\-consistency \(SscS\_\{\\mathrm\{sc\}\}\), and their fusion \(SfuS\_\{\\mathrm\{fu\}\}\)—together with four ablations: a direct judge without back\-translation, a single\-question judge, cosine similarity between instruction and back\-translation embeddings, and mean/max ensembles of the judge\-based scores\.

Three observations emerge\. First, judge\-side variants offer little benefit: on STL, back\-translation, direct judging, and single\-question judging achieve similar AUROCs \(0\.6340\.634–0\.6350\.635\), while ensembling improves only marginally to0\.6560\.656, indicating correlated errors\. Second, self\-consistency provides complementary information\. AlthoughSscS\_\{\\mathrm\{sc\}\}alone achieves AUROCs of0\.6550\.655\(STL\) and0\.8670\.867\(SpaTiaL\), combining it with back\-translation yields the best overall performance \(0\.7060\.706and0\.9200\.920\), consistently across STL tiers and robust to mixing weightsλ∈\[0\.3,0\.7\]\\lambda\\in\[0\.3,0\.7\]\. Third, the gain reflects complementary failure modes rather than averaging\. On STL,77\.8%77\.8\\%of inconsistent translation samples are erroneous, while among consistent samples, where self\-consistency is uninformative, back\-translation still distinguishes errors \(AUROC0\.6000\.600\), with37\.5%37\.5\\%of confidently generated translations remaining incorrect\. Thus, self\-consistency detects uncertain failures, whereas back\-translation detects confident semantic mismatches\.

The remaining errors are largely intrinsic to the task\. Invalid formulas are assigned the maximum score by construction, but syntactically valid convention errors and genuinely ambiguous instructions often remain indistinguishable\. The benchmark itself contains 114 instruction strings paired with conflicting reference formulas, limiting the achievable discriminability of any score derived solely from the instruction and translation\. The self\-consistency score also requires sufficient translation errors for reliable ranking; the fine\-tuned T5 baseline \(≈2%\\approx 2\\%error\) contains too few negatives for meaningful AUROC estimation and is therefore used only to verify the applicability of the score\.

Table[2](https://arxiv.org/html/2608.05439#S4.T2)translates ranking into selective prediction, reporting acceptance atα=0\.10\\alpha=0\.10and the minimum certifiable riskαℓ\\alpha\_\{\\ell\}, which AUROC alone does not determine\. On STL, self\-consistency and back\-translation have similar AUROCs, yetSscS\_\{\\mathrm\{sc\}\}cannot certify risks below0\.2700\.270because many tied scores concentrate calibration errors, causing complete abstention atα=0\.10\\alpha=0\.10, whereasSbtS\_\{\\mathrm\{bt\}\}accepts28\.0%28\.0\\%of inputs\. The fusion inherits the continuous resolution of back\-translation, reducing the certifiable floor to0\.0480\.048and increasing acceptance to34\.7%34\.7\\%\. On SpaTiaL, where back\-translation already achievesαℓ=0\.008\\alpha\_\{\\ell\}=0\.008, the fusion preserves this guarantee while improving acceptance by 14 percentage points\. On LTL, error rates of0\.5030\.503–0\.6490\.649placeαℓ\\alpha\_\{\\ell\}above0\.100\.10for every score, and the calibration abstains in full at this budget; the complete LTL results appear in the appendix\. Effective calibration thus requires accurate ranking and sufficient score resolution together, and the fusion supplies both wherever any score does\.

Table 4:Deployment drift onSTLwith frozenτ\\tau,α=0\.10\\alpha=0\.10, gate levelδ=0\.05\\delta=0\.05, and 100 reseeds\. Columns denote the calibration tier and rows denote the test tier\. The three panels report joint risk without gating, joint risk with gating, and abstention rate\. Bold entries are the in\-distribution diagonal; off\-diagonal entries are cross\-tier shifts\.Risk Control\.Table[3](https://arxiv.org/html/2608.05439#S4.T3)compares CRC calibration with coverage calibration on two translators\. A cell is compliant if its mean joint risk does not exceed the budget\. For the few\-shot translator, with unconditional error rates of0\.4230\.423,0\.4340\.434, and0\.5510\.551across the STL tiers, the calibration target decides the outcome\. CRC satisfies the budget in all eighteen settings, with joint risk rising toward each budget asα\\alphawidens and several operating points within one standard error of their targets, the position of an expectation\-level guarantee spending its budget in full; the single infeasible cell, the easiest tier atα=0\.05\\alpha=0\.05, lies below the feasibility floor of Eq\.[12](https://arxiv.org/html/2608.05439#S3.E12)and abstains in full\. Using the same score and data, Split CP violates the budget in thirteen cells\. Its risk may decrease asα\\alphaincreases because the relaxed coverage target can produce a stricter acceptance threshold; it tracks coverage rather than joint risk\.

The fine\-tuned translator, with error rates of0\.0370\.037,0\.1490\.149, and0\.3090\.309, inverts the reading: many budgets already exceed the unconditional error, so compliance on the easier tiers reflects the translator rather than the selection\. The deepest tier shows the mechanism at work, abstaining on approximately23%23\\%of inputs atα=0\.10\\alpha=0\.10to reduce joint risk from0\.3090\.309to0\.0880\.088; acceptance rates for all cells appear in the appendix ledger\. Split CP reports lower risk on this translator, decreasing from0\.0660\.066to0\.0340\.034on the deepest tier asα\\alphaincreases because acceptance becomes more restrictive, yet it still violates the two tightest budgets\. Abstention thus arises from two mechanisms: a threshold declining individual translations, active throughout the feasible cells, and a budget below the feasibility floor, which declines the entire stream and occurs once\.

Deployment Drift\.

The acceptance threshold guarantees risk only under exchangeability, and the instruction\-level filter rejects out\-of\-distribution inputs before translation\. Table[4](https://arxiv.org/html/2608.05439#S4.T4)evaluates the full pipeline on STL under the cross\-tier protocol ofWanget al\.\[[55](https://arxiv.org/html/2608.05439#bib.bib39)\]\. Each column fixes a calibration tier, threshold andkkNN reference included, and each row supplies the test stream, replaced off the diagonal by another tier’s without recalibration\. On the diagonal the filter defers0\.6%0\.6\\%,5\.4%5\.4\\%, and0\.7%0\.7\\%of clean in\-distribution inputs across the three tiers, consistent with the levelδ=0\.05\\delta=0\.05up to Monte Carlo variation atm=50m=50\. All six shifted settings raise joint risk \(0\.1090\.109–0\.1510\.151\) over their diagonals\. The filter reduces risk in five of the six and returns four below the budget, and the largest recovery, from0\.1230\.123to0\.0760\.076, occurs where the deepest\-tier stream meets the intermediate calibration\.

Some instructions the filter rejects would have been rejected by the CRC threshold as well and therefore do not affect execution\. Both settings that test the intermediate stream are of this kind, with the filter adding0\.8%0\.8\\%abstention against the shallow calibration and none against the deep one, so protection there falls entirely to the threshold\. Intermediate instructions sit inside both neighboring reference distributions, and detectability is directional in general, with deeper streams standing out against shallower references while the reverse shift passes the filter, the pattern anticipated in the Sec\.[3](https://arxiv.org/html/2608.05439#S3)\. In the remaining four settings the filter rejects5\.2%5\.2\\%–15\.6%15\.6\\%of inputs the threshold would have accepted, and39%39\\%–72%72\\%of these are incorrect translations that read plausibly, reflecting the distinct evidence the two components use, instruction typicality and translation reliability\. Abstention alone still overstates the filter, as the two settings on the shallowest stream abstain at39\.5%39\.5\\%and32\.1%32\.1\\%with identical gated risk because the extra rejections fall on correct translations\. Screening before translation also avoids3131–474474downstream model calls per150150shifted instructions\.

## References

- \[1\]\(2024\)Conformal risk control\.InInternational Conference on Learning Representations,B\. Kim, Y\. Yue, S\. Chaudhuri, K\. Fragkiadaki, M\. Khan, and Y\. Sun \(Eds\.\),Vol\.2024,pp\. 55198–55218\.External Links:[Link](https://proceedings.iclr.cc/paper_files/paper/2024/file/f3549ef9b5ff520a7e41ff3cc306ab2b-Paper-Conference.pdf)Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p2.1),[§1](https://arxiv.org/html/2608.05439#S1.p6.1),[§3\.2](https://arxiv.org/html/2608.05439#S3.SS2.1.p1.3),[§3\.2](https://arxiv.org/html/2608.05439#S3.SS2.p2.3),[§3](https://arxiv.org/html/2608.05439#S3.p1.1)\.
- \[2\]C\. Baier and J\. Katoen\(2008\)Principles of model checking\.MIT press\.Cited by:[§2](https://arxiv.org/html/2608.05439#S2.p1.1)\.
- \[3\]R\. F\. Barber, E\. J\. Candes, A\. Ramdas, and R\. J\. Tibshirani\(2023\)Conformal prediction beyond exchangeability\.The Annals of Statistics51\(2\),pp\. 816–845\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p6.1)\.
- \[4\]S\. Bates, E\. Candès, L\. Lei, Y\. Romano, and M\. Sesia\(2023\)Testing for outliers with conformal p\-values\.The Annals of Statistics51\(1\),pp\. 149–178\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p7.1)\.
- \[5\]C\. Belta, B\. Yordanov, and E\. A\. Gol\(2017\)Formal methods for discrete\-time dynamical systems\.Vol\.89,Springer\.Cited by:[§2](https://arxiv.org/html/2608.05439#S2.p1.1)\.
- \[6\]T\. Chakraborti, J\. Kang, F\. Fuggitti, M\. Katz, and S\. Sohrabi\(2024\)Interactive plan selection using linear temporal logic, disjunctive action landmarks, and natural language instruction\.pp\. 23775–23777\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p1.1)\.
- \[7\]Y\. Chen, R\. Gandhi, Y\. Zhang, and C\. Fan\(2023\)Nl2tl: transforming natural languages to temporal logics using large language models\.InProceedings of the 2023 Conference on Empirical Methods in Natural Language Processing,pp\. 15880–15903\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p1.1),[§1](https://arxiv.org/html/2608.05439#S1.p5.1),[§2](https://arxiv.org/html/2608.05439#S2.p3.4),[§2](https://arxiv.org/html/2608.05439#S2.p5.12),[§4](https://arxiv.org/html/2608.05439#S4.SS0.SSS0.Px1.p1.1),[§4](https://arxiv.org/html/2608.05439#S4.SS0.SSS0.Px2.p1.3)\.
- \[8\]Y\. Chen, W\. Walden, T\. Chen, A\. S\. White, and B\. Van Durme\(2023\)A unified view of evaluation metrics for structured prediction\.pp\. 12868–12882\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p2.1)\.
- \[9\]J\. J\. Cherian, I\. Gibbs, and E\. J\. Candès\(2024\)Large language model validity via enhanced conformal prediction methods\.Advances in Neural Information Processing Systems37,pp\. 114812–114842\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p6.1)\.
- \[10\]M\. Cosler, C\. Hahn, D\. Mendoza, F\. Schmitt, and C\. Trippel\(2023\)Nl2spec: interactively translating unstructured natural language to temporal logics with large language models\.InInternational Conference on Computer Aided Verification,pp\. 383–396\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p5.1),[§2](https://arxiv.org/html/2608.05439#S2.p3.4)\.
- \[11\]J\. Duan, H\. Cheng, S\. Wang, A\. Zavalny, C\. Wang, R\. Xu, B\. Kailkhura, and K\. Xu\(2024\)Shifting attention to relevance: towards the predictive uncertainty quantification of free\-form large language models\.pp\. 5050–5063\.Cited by:[§2](https://arxiv.org/html/2608.05439#S2.p3.4)\.
- \[12\]W\. English, D\. Simon, S\. K\. Jha, and R\. Ewetz\(2025\)Grammar\-forced translation of natural language to temporal logic using llms\.arXiv preprint arXiv:2512\.16814\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p5.1)\.
- \[13\]Y\. Fang, Z\. Jin, J\. An, H\. Chen, X\. Chen, and N\. Zhan\(2025\)Enhancing transformation from natural language to signal temporal logic using llms with diverse external knowledge\.InFindings of the Association for Computational Linguistics: ACL 2025,pp\. 10446–10458\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p5.1)\.
- \[14\]A\. Farinhas, C\. Zerva, D\. Ulmer, and A\. Martins\(2024\)Non\-exchangeable conformal risk control\.InInternational Conference on Learning Representations,Vol\.2024,pp\. 50952–50966\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p6.1)\.
- \[15\]S\. Farquhar, J\. Kossen, L\. Kuhn, and Y\. Gal\(2024\)Detecting hallucinations in large language models using semantic entropy\.Nature630\(8017\),pp\. 625–630\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p6.1),[§3\.1](https://arxiv.org/html/2608.05439#S3.SS1.p1.10)\.
- \[16\]F\. Fuggitti and T\. Chakraborti\(2023\)NL2LTL–a python package for converting natural language \(nl\) instructions to linear temporal logic \(ltl\) formulas\.pp\. 16428–16430\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p5.1)\.
- \[17\]Y\. Geifman and R\. El\-Yaniv\(2019\)Selectivenet: a deep neural network with an integrated reject option\.pp\. 2151–2159\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p2.1)\.
- \[18\]N\. Gopalan, D\. Arumugam, L\. L\. Wong, and S\. Tellex\(2018\)Sequence\-to\-sequence language grounding of non\-markovian task specifications\.\.InRobotics: Science and Systems,Vol\.2018\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p5.1)\.
- \[19\]J\. A\. Hanley and B\. J\. McNeil\(1982\)The meaning and use of the area under a receiver operating characteristic \(roc\) curve\.\.Radiology143\(1\),pp\. 29–36\.Cited by:[§4](https://arxiv.org/html/2608.05439#S4.SS0.SSS0.Px4.p1.6)\.
- \[20\]J\. He, E\. Bartocci, D\. Ničković, H\. Isakovic, and R\. Grosu\(2022\)Deepstl: from english requirements to signal temporal logic\.InProceedings of the 44th International Conference on Software Engineering,pp\. 610–622\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p1.1),[§1](https://arxiv.org/html/2608.05439#S1.p5.1)\.
- \[21\]Y\. Jin and E\. J\. Candès\(2023\)Selection by prediction with conformal p\-values\.Journal of Machine Learning Research24\(244\),pp\. 1–41\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p7.1)\.
- \[22\]R\. Laxhammar and G\. Falkman\(2015\)Inductive conformal anomaly detection for sequential detection of anomalous sub\-trajectories\.Annals of Mathematics and Artificial Intelligence74\(1\),pp\. 67–94\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p7.1)\.
- \[23\]M\. Lee, K\. Kim, T\. Kim, and S\. Park\(2024\)Selective generation for controllable language models\.Advances in Neural Information Processing Systems37,pp\. 50494–50527\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p2.1)\.
- \[24\]K\. Leung, N\. Aréchiga, and M\. Pavone\(2023\)Backpropagation through signal temporal logic specifications: infusing logical structure into gradient\-based methods\.The International Journal of Robotics Research42\(6\),pp\. 356–370\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p6.1)\.
- \[25\]D\. Li, M\. Cai, C\. Vasile, and R\. Tron\(2023\)Learning signal temporal logic through neural network for interpretable classification\.pp\. 1907–1914\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p6.1)\.
- \[26\]D\. Li, M\. Cai, C\. Vasile, and R\. Tron\(2024\)Tlinet: differentiable neural network temporal logic inference\.arXiv preprint arXiv:2405\.06670\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p6.1)\.
- \[27\]D\. Li, Y\. Wang, M\. Cleaveland, M\. Cai, and R\. Tron\(2025\)Conformal prediction for signal temporal logic inference\.arXiv preprint arXiv:2509\.25473\.Note:Accepted at the 65th IEEE Conference on Decision and ControlCited by:[§1](https://arxiv.org/html/2608.05439#S1.p6.1)\.
- \[28\]L\. Lindemann, M\. Cleaveland, G\. Shim, and G\. J\. Pappas\(2023\)Safe planning in dynamic environments using conformal prediction\.IEEE Robotics and Automation Letters8\(8\),pp\. 5116–5123\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p6.1)\.
- \[29\]J\. X\. Liu, Z\. Yang, B\. Schornstein, S\. Liang, I\. Idrees, S\. Tellex, and A\. Shah\(2022\)Lang2ltl: translating natural language commands to temporal specification with large language models\.Cited by:[§2](https://arxiv.org/html/2608.05439#S2.p5.12)\.
- \[30\]L\. Luo, K\. Liang, C\. Vasile, and M\. Cai\(2026\)Differentiable spatial: symbolic learning and reasoning with geometric temporal logic for manipulation tasks\.The IEEE/RSJ International Conference on Intelligent Robots and Systems \(IROS\)\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p6.1)\.
- \[31\]L\. Luo, K\. Liang, Y\. Xia, and M\. Cai\(2026\)NL2SpaTiaL: generating geometric spatio\-temporal logic specifications from natural language for manipulation tasks\.The IEEE/RSJ International Conference on Intelligent Robots and Systems \(IROS\)\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p1.1),[§1](https://arxiv.org/html/2608.05439#S1.p5.1),[§2](https://arxiv.org/html/2608.05439#S2.p3.4),[§2](https://arxiv.org/html/2608.05439#S2.p5.12),[§4](https://arxiv.org/html/2608.05439#S4.SS0.SSS0.Px1.p1.1),[§4](https://arxiv.org/html/2608.05439#S4.SS0.SSS0.Px2.p1.3)\.
- \[32\]O\. Maler and D\. Nickovic\(2004\)Monitoring temporal properties of continuous signals\.pp\. 152–166\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p1.1),[§2](https://arxiv.org/html/2608.05439#S2.p1.1)\.
- \[33\]D\. Mendoza, C\. Hahn, and C\. Trippel\(2024\)Translating natural language to temporal logics with large language models and model checkers\.In2024 Formal Methods in Computer\-Aided Design \(FMCAD\),pp\. 1–11\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p5.1),[§2](https://arxiv.org/html/2608.05439#S2.p3.4)\.
- \[34\]C\. Mohri and T\. Hashimoto\(2024\)Language models with conformal factuality guarantees\.arXiv preprint arXiv:2402\.10978\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p6.1)\.
- \[35\]J\. Moon, H\. Cho, and E\. L\. Park\(2020\)Revisiting round\-trip translation for quality estimation\.InProceedings of the 22nd Annual Conference of the European Association for Machine Translation,pp\. 91–104\.Cited by:[§3\.1](https://arxiv.org/html/2608.05439#S3.SS1.p1.7)\.
- \[36\]C\. Pek, G\. F\. Schuppe, F\. Esposito, J\. Tumova, and D\. Kragic\(2023\)SpaTiaL: monitoring and planning of robotic tasks using spatio\-temporal logic specifications\.Autonomous Robots47\(8\),pp\. 1439–1462\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p1.1),[§2](https://arxiv.org/html/2608.05439#S2.p1.1)\.
- \[37\]A\. Pnueli\(1977\)The temporal logic of programs\.In18th annual symposium on foundations of computer science \(sfcs 1977\),pp\. 46–57\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p1.1),[§2](https://arxiv.org/html/2608.05439#S2.p1.1)\.
- \[38\]V\. Quach, A\. Fisch, T\. Schuster, A\. Yala, J\. H\. Sohn, T\. Jaakkola, and R\. Barzilay\(2024\)Conformal language modeling\.InInternational Conference on Learning Representations,Vol\.2024,pp\. 11654–11681\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p6.1)\.
- \[39\]V\. Raman, C\. Lignos, C\. Finucane, K\. C\. Lee, M\. P\. Marcus, and H\. Kress\-Gazit\(2013\)Sorry dave, i’m afraid i can’t do that: explaining unachievable robot tasks using natural language\.\.InRobotics: science and systems,Vol\.2,pp\. 2–1\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p5.1)\.
- \[40\]A\. Z\. Ren, A\. Dixit, A\. Bodrova, S\. Singh, S\. Tu, N\. Brown, P\. Xu, L\. Takayama, F\. Xia, J\. Varley,et al\.\(2023\)Robots that ask for help: uncertainty alignment for large language model planners\.arXiv preprint arXiv:2307\.01928\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p6.1)\.
- \[41\]R\. Roy, J\. Gaglione, N\. Baharisangari, D\. Neider, Z\. Xu, and U\. Topcu\(2023\)Learning interpretable temporal properties from positive examples only\.pp\. 6507–6515\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p1.1)\.
- \[42\]O\. Somov and E\. Tutubalina\(2025\)Confidence estimation for error detection in text\-to\-sql systems\.pp\. 25137–25145\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p2.1)\.
- \[43\]E\. Stengel\-Eskin and B\. Van Durme\(2023\)Calibrated interpretation: confidence estimation in semantic parsing\.Transactions of the Association for Computational Linguistics11,pp\. 1213–1231\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p2.1)\.
- \[44\]J\. Su, J\. Luo, H\. Wang, and L\. Cheng\(2024\)Api is enough: conformal prediction for large language models without logit\-access\.InFindings of the Association for Computational Linguistics: EMNLP 2024,pp\. 979–995\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p6.1)\.
- \[45\]Y\. Sun, Y\. Ming, X\. Zhu, and Y\. Li\(2022\-17–23 Jul\)Out\-of\-distribution detection with deep nearest neighbors\.InProceedings of the 39th International Conference on Machine LearningInternational symposium on formal techniques in real\-time and fault\-tolerant systemsWorkshop on Language and Robotics at CoRL 2022Proceedings of the AAAI Conference on Artificial IntelligenceProceedings of the 63rd Annual Meeting of the Association for Computational Linguistics \(Volume 1: Long Papers\)The Eleventh International Conference on Learning RepresentationsProceedings of the AAAI Conference on Artificial IntelligenceProceedings of the AAAI Conference on Artificial IntelligenceProceedings of the AAAI Conference on Artificial IntelligenceProceedings of the AAAI Conference on Artificial IntelligenceProceedings of the 2023 Conference on Empirical Methods in Natural Language ProcessingProceedings of the 2020 Conference on Empirical Methods in Natural Language Processing \(EMNLP\)Proceedings of the AAAI Conference on Artificial IntelligenceInternational conference on machine learning2023 American Control Conference \(ACC\)Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics \(Volume 1: Long Papers\),K\. Chaudhuri, S\. Jegelka, L\. Song, C\. Szepesvari, G\. Niu, S\. Sabato, W\. Che, J\. Nabende, E\. Shutova, and M\. T\. Pilehvar \(Eds\.\),Proceedings of Machine Learning Research, Vol\.162373537383339,pp\. 20827–20840\.External Links:[Link](https://proceedings.mlr.press/v162/sun22d.html)Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p7.1)\.
- \[46\]D\. S\. Sundarsingh, J\. Wang, J\. V\. Deshmukh, and Y\. Kantaros\(2025\)Conformalnl2ltl: translating natural language instructions into temporal logic formulas with conformal correctness guarantees\.arXiv preprint arXiv:2504\.21022\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p5.1)\.
- \[47\]R\. J\. Tibshirani, R\. Foygel Barber, E\. Candes, and A\. Ramdas\(2019\)Conformal prediction under covariate shift\.Advances in neural information processing systems32\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p6.1)\.
- \[48\]V\. Vovk, A\. Gammerman, and G\. Shafer\(2005\)Algorithmic learning in a random world\.Springer\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p2.1),[§2](https://arxiv.org/html/2608.05439#S2.p4.3),[§3\.2](https://arxiv.org/html/2608.05439#S3.SS2.p3.6)\.
- \[49\]C\. Wang, C\. Ross, Y\. Kuo, B\. Katz, and A\. Barbu\(2021\)Learning a natural\-language to ltl executable semantic parser for grounded robotics\.InConference on Robot Learning,pp\. 1706–1718\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p5.1)\.
- \[50\]J\. Wang, G\. He, and Y\. Kantaros\(2024\)Probabilistically correct language\-based multi\-robot planning using conformal prediction\.IEEE Robotics and Automation Letters10\(1\),pp\. 160–167\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p6.1)\.
- \[51\]J\. Wang, J\. Tong, K\. Tan, Y\. Vorobeychik, and Y\. Kantaros\(2023\)Conformal temporal logic planning using large language models\.ACM Transactions on Cyber\-Physical Systems\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p6.1)\.
- \[52\]X\. Wang, J\. Wei, D\. Schuurmans, Q\. V\. Le, E\. H\. Chi, S\. Narang, A\. Chowdhery, and D\. Zhou\(2023\)Self\-consistency improves chain of thought reasoning in language models\.External Links:[Link](https://openreview.net/forum?id=1PL1NIMMrw)Cited by:[§3\.1](https://arxiv.org/html/2608.05439#S3.SS1.p1.10)\.
- \[53\]Y\. Wang, D\. Li, M\. Cleaveland, R\. Tron, and M\. Cai\(2026\)Conformalized signal temporal logic inference under covariate shift\.arXiv preprint arXiv:2603\.27062\.Note:Accepted at the 65th IEEE Conference on Decision and ControlCited by:[§1](https://arxiv.org/html/2608.05439#S1.p6.1)\.
- \[54\]Z\. Wang, J\. Duan, L\. Cheng, Y\. Zhang, Q\. Wang, X\. Shi, K\. Xu, H\. T\. Shen, and X\. Zhu\(2024\)Conu: conformal uncertainty in large language models with correctness coverage guarantees\.InFindings of the Association for Computational Linguistics: EMNLP 2024,pp\. 6886–6898\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p6.1)\.
- \[55\]Z\. Wang, Q\. Wang, Y\. Zhang, T\. Chen, X\. Zhu, X\. Shi, and K\. Xu\(2025\-07\)SConU: selective conformal uncertainty in large language models\.Vienna, Austria,pp\. 19052–19075\.External Links:[Link](https://aclanthology.org/2025.acl-long.934/),[Document](https://dx.doi.org/10.18653/v1/2025.acl-long.934),ISBN 979\-8\-89176\-251\-0Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p2.1),[§1](https://arxiv.org/html/2608.05439#S1.p6.1),[§1](https://arxiv.org/html/2608.05439#S1.p7.1),[§3\.2](https://arxiv.org/html/2608.05439#S3.SS2.p3.6),[§4](https://arxiv.org/html/2608.05439#S4.SS0.SSS0.Px4.p9.10)\.
- \[56\]Y\. Xu, W\. Guo, and Z\. Wei\(2025\)Selective conformal risk control\.arXiv preprint arXiv:2512\.12844\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p7.1)\.
- \[57\]Z\. Xu, Y\. Chen, and U\. Topcu\(2021\)Adaptive teaching of temporal logic formulas to preference\-based learners\.pp\. 5061–5068\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p1.1)\.
- \[58\]X\. Zhao, V\. Robu, D\. Flynn, F\. Dinmohammadi, M\. Fisher, and M\. Webster\(2019\)Probabilistic model checking of robots deployed in extreme environments\.pp\. 8066–8074\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p1.1)\.
- \[59\]L\. Zheng, W\. Chiang, Y\. Sheng, S\. Zhuang, Z\. Wu, Y\. Zhuang, Z\. Lin, Z\. Li, D\. Li, E\. Xing,et al\.\(2023\)Judging llm\-as\-a\-judge with mt\-bench and chatbot arena\.Advances in neural information processing systems36,pp\. 46595–46623\.Cited by:[§3\.1](https://arxiv.org/html/2608.05439#S3.SS1.p1.7)\.
- \[60\]R\. Zhong, T\. Yu, and D\. Klein\(2020\)Semantic evaluation for text\-to\-sql with distilled test suites\.pp\. 396–411\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p2.1)\.
- \[61\]T\. Zollo, T\. Morrill, Z\. Deng, J\. Snell, T\. Pitassi, and R\. Zemel\(2024\)Prompt risk control: a rigorous framework for responsible deployment of large language models\.InInternational Conference on Learning Representations,Vol\.2024,pp\. 4045–4067\.Cited by:[§1](https://arxiv.org/html/2608.05439#S1.p6.1)\.

## Appendix AAppendix

### A\.1Reproducing Results

All reported results use the fixed prompts, data partitions, and calibration settings described in the main text\. Additional implementation details and complete result tables are provided below\. The submitted code package contains the data, scoring outputs, and the full calibration pipeline\. Running the entry script as described in its README regenerates the CP results and compliance tables from the shipped scored files, without network or API access, and reconciles them against the reported numbers\. All results use the fixed prompts, data partitions, and calibration settings described in the main text\.

### A\.2Computing infrastructure\.

All local computation ran on a single workstation with one NVIDIA RTX 4080 GPU \(16 GB\), Ubuntu 22\.04, Python 3\.8, and PyTorch 2\.4\.1\+cu121\. Translation and back\-translation used GPT\-5\.2\-2025\-12\-11 and judging used GPT\-5\.4\-2026\-03\-05 through their public APIs; instruction embeddings used all\-mpnet\-base\-v2\. Calibration, resplitting, and table generation are CPU\-only and complete in minutes\.

### A\.3Example Prompt

One accepted and one rejected translation per language, traced through the back\-translation scoring pipeline\. LTL shares the STL prompts unchanged; SpaTiaL uses its own back\-translation prompt and a categorical rubric, shown after the examples\. Rejected examples parse and read fluently; the judge locates the error in a single rubric dimension\.

STL — accepted\. Instructionxx:“If \( prop\_1 \) then at a time within the next 12 to 50 time units ultimately \( prop\_2 \)\.” Candidateφ^\\hat\{\\varphi\}:globally \( prop\_1 imply finally \[12,50\] prop\_2 \) Back\-translationu^\\hat\{u\}:“At all times, if prop\_1 holds, then prop\_2 must hold at some time between 12 and 50 time units from then\.” Judge:logical9595, temporal9292, time constraints100100, overall9595⇒Sbt=0\.045\\;\\Rightarrow\\;S\_\{\\mathrm\{bt\}\}=0\.045; the calibrated threshold admits it and the formula is returned\.STL — rejected\. Instructionxx:“On condition that \( prop\_1 \), then \( prop\_2 \) and this scenario has to always hold for the first 3 to 12 time units\.” Candidateφ^\\hat\{\\varphi\}:globally \[3,12\] \( prop\_1 imply prop\_2 \)reference:globally \( prop\_1 imply globally \[3,12\] prop\_2 \) Back\-translationu^\\hat\{u\}:“Between 3 and 12 time units from now, it must always be the case that if prop\_1 holds then prop\_2 holds\.” Judge:logical9595, temporal7070, time constraints4040, overall6868⇒Sbt=0\.318\\;\\Rightarrow\\;S\_\{\\mathrm\{bt\}\}=0\.318; the threshold does not admit it and the translation is withheld\. The interval is attached to the outergloballyrather than to the inner one governing prop\_2\.

LTL — accepted\. Instructionxx:“if at some time \(prop\_1\), never \(prop\_2\)” Candidateφ^\\hat\{\\varphi\}:\( finally prop\_1 imply globally \( negation prop\_2 \) \) Back\-translationu^\\hat\{u\}:“If eventually prop\_1 happens, then from now on it is always the case that prop\_2 does not happen\.” Judge:logical9292, temporal9696, time constraints100100, overall9595⇒Sbt=0\.043\\;\\Rightarrow\\;S\_\{\\mathrm\{bt\}\}=0\.043; admitted and returned\.LTL — rejected\. Instructionxx:“⟨\\langleeval\_nl⟩\\rangle” Candidateφ^\\hat\{\\varphi\}:⟨\\langlepred⟩\\ranglereference:⟨\\langlegold⟩\\rangle Back\-translationu^\\hat\{u\}:“⟨\\langlenl\_back⟩\\rangle” Judge:logical⟨n⟩\\langle n\\rangle, temporal⟨n⟩\\langle n\\rangle, time constraints⟨n⟩\\langle n\\rangle, overall⟨n⟩\\langle n\\rangle⇒Sbt=⟨S⟩\\;\\Rightarrow\\;S\_\{\\mathrm\{bt\}\}=\\langle S\\rangle; withheld\. The prediction moves the parenthesization ofuntil, scoping it over the first argument alone\.

STL — back\-translation prompt \(system\): You translate Signal Temporal Logic \(STL\) formulas into precise English\. Operators: globally/finally/until \(may carry a time interval \[a,b\], b can be “infinite”\), and/or/imply/equal/negation\. Atomic propositions are placeholders prop\_1, prop\_2, …Rules:keep every prop\_i symbol exactly as\-is \(never merge, never pronominalize\); state every time interval with its exact numbers; do not add or drop conditions; output one English sentence, nothing else\. Write plain English only: never include formula notation, brackets, operator words as symbols, or interval syntax like \[a,b\] — always express intervals as English phrases such as ‘between a and b time units from now’\.

STL — judge prompt \(system\): You are a semantic\-equivalence judge\. You will receive two English sentences describing a temporal\-logic specification: A — an original human instruction; B — a machine paraphrase\. Rate how well B matches A on four dimensions, each an INTEGER 0–100:logical\_structure\(boolean connectives and nesting: and/or/imply/equal/negation, grouping\);temporal\_operators\(temporal semantics: always/globally, eventually/finally, until\);time\_constraints\(time\-interval numbers and bounds; if BOTH sentences state no time constraint, score 100\);overall\_meaning\(overall semantic equivalence\)\. Return ONLY valid JSON\{"logical\_structure": n, "temporal\_operators": n, "time\_constraints": n, "overall\_meaning": n\}\.User:A \(original\):⟨\\langleinstructionxx⟩\\rangleB \(paraphrase\):⟨\\langleback\-translationu^\\hat\{u\}⟩\\rangle

SpaTiaL — accepted\. Instructionxx:“From time 11 through time 25, make sure obj\_r stays strictly inside the region reg\_sort\.” Candidateφ^\\hat\{\\varphi\}:G\[11,25\]\(enclIn\(obj\_r, reg\_sort\)\) Back\-translationu^\\hat\{u\}:“It is always the case, at every time point from 11 through 25, that obj\_r is enclosed in reg\_sort\.” Judge:object match, spatial partial, temporal match, quantifier/negation match⇒Sbt=0\.125\\;\\Rightarrow\\;S\_\{\\mathrm\{bt\}\}=0\.125; admitted and returned\. The single partial reflects the strictness nuance between “strictly inside” and “enclosed”\.SpaTiaL — rejected\. Instructionxx:“Ensure that at some point between time 12 and time 17, there is a continuous 10\-time\-unit period during which obj\_y overlaps obj\_r the entire time\.” Candidateφ^\\hat\{\\varphi\}:F\[12,17\]\(G\[20,30\]\(ovlp\(obj\_y, obj\_r\)\)\)reference:F\[12,17\]\(G\[0,10\]\(ovlp\(obj\_y, obj\_r\)\)\) Back\-translationu^\\hat\{u\}:“At some time between 12 and 17, it will be the case that, at all times between 20 and 30, ovlp\(obj\_y, obj\_r\) holds\.” Judge:object match, spatial match, temporal mismatch, quantifier/negation partial⇒Sbt=0\.375\\;\\Rightarrow\\;S\_\{\\mathrm\{bt\}\}=0\.375; withheld\. The inner window is written as absolute\[20,30\]where the instruction requires a relative ten\-unit window\.

SpaTiaL — back\-translation prompt \(system\): You are a formal\-language interpreter\. Your only task is to render a logical formula as plain English\.Rules:describe exactly what the formula states — nothing more, nothing less\. Do NOT invent objects, relations, or constraints absent from the formula\. Do NOT guess the user’s original intent or paraphrase loosely\. Do NOT omit any part of the formula \(every sub\-expression must appear in your output\)\. Use neutral, literal language\. Faithfulness to the formula takes priority over fluency\. Output one concise paragraph\.

SpaTiaL — judge prompt \(system\)\(output schema abridged\): You are a semantic\-equivalence judge for spatial\-temporal logic descriptions\. You will receive two natural\-language sentences: A — an original instruction written by a human; B — a machine\-generated paraphrase of a formal logic formula\. Assess how well B captures the meaning of A across four dimensions\. For each dimension output exactly one label from \{match, partial, mismatch\} and one short reason \(≤\\leq20 words\)\.object\(same physical objects / regions present in both\);spatial\(spatial relationships: touching, overlapping, inside, far from, between, left of, right of, above, below, oriented …\);temporal\(temporal / logical operators and structure: always G, eventually F, until U, implies, not, and, or …\);quantifier\_negation\(negations and implicit universal / existential quantifiers consistent\)\. Return ONLY valid JSON with a\{"label", "reason"\}pair per dimension\. Labels are averaged as11/0\.50\.5/0to giveSbtS\_\{\\mathrm\{bt\}\}\.User:identical to the STL judge template\.

### A\.4Additional Results: LTL

Linear Temporal Logic instantiates the framework a third time, with nothing changed: the same scoring pipeline, judge prompts, canonical equivalence construction, and calibration machinery are applied to an interval\-free logic, using the few\-shot GPT\-5\.2 translator and the tier construction of the STL benchmark\. What the language contributes to the evaluation is an operating regime the first two could not reach: raw error rates of0\.6490\.649,0\.5030\.503, and0\.5030\.503across the three tiers place the translator well past the point where selection is comfortable, and every component of the framework is thereby exercised at full load\.

The scoring layer transfers intact \(Table[5](https://arxiv.org/html/2608.05439#A1.T5)\)\. Back\-translation reaches an overall AUROC of0\.6930\.693and the fusion0\.7120\.712, within the range the STL setting attains, and the fusion improves the ranking on the two deeper tiers and overall\. The one cell where it does not, the shallowest tier, is itself informative: errors there are almost entirely structural,52\.9%52\.9\\%operator confusions and41\.9%41\.9\\%scope or nesting errors, with predicate, connective, and negation errors nearly absent\. Both signals inspect a translation whose predicates are trivially right and whose few operators read plausibly in either arrangement, so the tier compresses exactly the failure mode that consistency evidence sees least well\. Deeper tiers disperse their errors across content, connective errors rise from7\.0%7\.0\\%to25\.0%25\.0\\%with depth, and the ranking recovers accordingly\.

The calibration layer answers with feasibility rather than performance \(Table[6](https://arxiv.org/html/2608.05439#A1.T6)\)\. With errors this dense, the smallest certifiable risk level rises toαℓ=0\.184\\alpha\_\{\\ell\}=0\.184on the shallowest tier, and four cells across the grid fall below their floors\. The procedure abstains on the entire stream in each, which is the designed response: a budget the calibration data cannot certify is withheld, announced before deployment, and priced against its remedies\. Where budgets are feasible the rule spends them fully; the deepest tier tracks its budget within one standard error at every level of the grid, from0\.0480\.048atα=0\.05\\alpha=0\.05to0\.3040\.304at0\.300\.30, the cleanest budget\-exhaustion profile among the three languages\. Across all eighteen cells the risk\-calibrated arm records no violation, while the coverage\-calibrated arm exceeds the budget in thirteen; atα=0\.05\\alpha=0\.05on the shallowest tier the contrast is starkest, with the coverage arm passing9090incorrect formulas per150150instructions downstream against none for the risk\-calibrated arm\.

The tier profile also completes an observation begun in the main text\. Across four translator–language configurations the difficulty gradient now takes four shapes: rising with depth, falling with depth, U\-shaped, and here reversed, with the shallowest tier hardest\. The same translator that finds STL’s deepest tier hardest finds LTL’s shallowest tier hardest, so the direction is a property of the configuration, not of structural depth, and the error composition above explains why: a six\-word instruction concentrates its entire difficulty in operator arrangement, while longer instructions spread it across content\. Difficulty along a structural axis cannot be assumed in advance, which is the case for calibrating each tier separately rather than pooling across a heterogeneous stream\.

Table 5:Error\-detection AUROC by scoring channel onLTLusing the GPT\-5\.2 few\-shot translator\. Best values in each column are shown in bold\. Darker cells indicate higher AUROC\. TheΔ\\Deltarow reports the margin of12​\(Ssc\+Sbt\)\\tfrac\{1\}\{2\}\(S\_\{\\mathrm\{sc\}\}\+S\_\{\\mathrm\{bt\}\}\)over the best single channel in each column\.Table 6:Risk\-control compliance matrix onLTL\(GPT\-5\.2 few\-shot translator, deployed scoreSfuS\_\{\\mathrm\{fu\}\},ncal=200n\_\{\\mathrm\{cal\}\}=200\)\. Values are mean joint risk±\\pmstandard error over 100 random calibration/test splits\. Green cells indicate clear CRC compliance, red cells indicate violations by more than one standard error, and gray cells indicate results within one standard error ofα\\alpha\. Uncolored Split CP entries carry no compliance claim\. The symbol‡denotes full abstention when no valid CRC threshold exists\.TierNosel\.MethodRisk budgetα\\alpha0\.050\.100\.150\.200\.250\.30D20\.649CRCabst\.‡abst\.‡abst\.‡0\.186±\\pm0\.007 ✓0\.243±\\pm0\.005 ✓0\.297±\\pm0\.005†Split CP0\.608±\\pm0\.003 ✗0\.565±\\pm0\.004 ✗0\.528±\\pm0\.003 ✗0\.493±\\pm0\.004 ✗0\.450±\\pm0\.004 ✗0\.412±\\pm0\.004 ✗D30\.503CRCabst\.‡0\.077±\\pm0\.005 ✓0\.139±\\pm0\.004 ✓0\.190±\\pm0\.004 ✓0\.245±\\pm0\.004 ✓0\.298±\\pm0\.005†Split CP0\.399±\\pm0\.004 ✗0\.329±\\pm0\.004 ✗0\.276±\\pm0\.004 ✗0\.229±\\pm0\.003 ✗0\.193±\\pm0\.0030\.159±\\pm0\.003D40\.503CRC0\.048±\\pm0\.002†0\.098±\\pm0\.003†0\.148±\\pm0\.004†0\.198±\\pm0\.004†0\.249±\\pm0\.004†0\.304±\\pm0\.005†Split CP0\.346±\\pm0\.003 ✗0\.272±\\pm0\.004 ✗0\.223±\\pm0\.003 ✗0\.180±\\pm0\.0040\.138±\\pm0\.0030\.110±\\pm0\.002✗ count:CRC: 0/18\(8†, 4 abst\.\)Split CP: 13/18Table 7:Wrong translations executed per 150 test instructions, with the per\-row budgetα⋅150\\alpha\\cdot 150\. Each entry is the mean joint risk of the corresponding compliance matrix scaled by the test\-set size; the two tables carry the same information in different units\. A ✓ marks clear CRC compliance, ✗ marks a violation by more than one standard error, and†marks a result within one standard error of the budget\. Unmarked Split CP entries carry no compliance claim\. Entries are means over 100 resplits, not per\-run guarantees\.
### A\.5Executed\-Error Counts

Table[7](https://arxiv.org/html/2608.05439#A1.T7)restates the compliance matrices in executed\-error counts, so the unit change alters no conclusion but makes the stake concrete\. Atα=0\.05\\alpha=0\.05the coverage\-calibrated arm passes up to9191incorrect formulas per150150instructions downstream, against at most7\.37\.3for the risk\-calibrated arm across the nine settings; on LTL’s shallowest tier the risk\-calibrated arm withholds the entire stream at this budget, so the corresponding count is zero by construction\. The count scale also separates the two failure geographies: the coverage arm exceeds its budget almost everywhere the translator is weak and nowhere it is strong, while the risk\-calibrated arm sits under or within one standard error of every budget except a single cell, STL D3 atα=0\.20\\alpha=0\.20, which lands0\.70\.7formulas over a budget of3030, the sampling position of an expectation\-level guarantee rather than a failure of control\.

### A\.6Proof of Theorem[1](https://arxiv.org/html/2608.05439#Thmtheorem1)

This appendix gives the complete proof of Theorem[1](https://arxiv.org/html/2608.05439#Thmtheorem1)\. Fix one calibration group and letnnbe its calibration size\. Write

\(S1,Z1\),…,\(Sn,Zn\),\(Sn\+1,Zn\+1\)\(S\_\{1\},Z\_\{1\}\),\\ldots,\(S\_\{n\},Z\_\{n\}\),\(S\_\{n\+1\},Z\_\{n\+1\}\)for the score and error pairs of the calibration examples and one test example, whereZi=𝟏​\[φ^i≢φi⋆\]Z\_\{i\}=\\mathbf\{1\}\[\\widehat\{\\varphi\}\_\{i\}\\not\\equiv\\varphi\_\{i\}^\{\\star\}\]\. Then\+1n\+1pairs are exchangeable within the group\.

For a thresholdτ\\tau, define the calibration error count

Nn​\(τ\)=∑i=1n𝟏​\[Si≤τ\]​Zi\.N\_\{n\}\(\\tau\)=\\sum\_\{i=1\}^\{n\}\\mathbf\{1\}\[S\_\{i\}\\leq\\tau\]\\,Z\_\{i\}\.SinceR^n​\(τ\)=Nn​\(τ\)/n\\widehat\{R\}\_\{n\}\(\\tau\)=N\_\{n\}\(\\tau\)/n, the constraint in Eq\.[10](https://arxiv.org/html/2608.05439#S3.E10)is equivalent to

Nn​\(τ\)\+1n\+1≤α\.\\frac\{N\_\{n\}\(\\tau\)\+1\}\{n\+1\}\\leq\\alpha\.Let

Kα=max⁡\{k∈\{0,…,n\}:k\+1n\+1≤α\},K\_\{\\alpha\}=\\max\\left\\\{k\\in\\\{0,\\ldots,n\\\}:\\frac\{k\+1\}\{n\+1\}\\leq\\alpha\\right\\\},when this set is nonempty\. A threshold is feasible precisely whenNn​\(τ\)≤KαN\_\{n\}\(\\tau\)\\leq K\_\{\\alpha\}\. If the set definingKαK\_\{\\alpha\}is empty, thenα<1/\(n\+1\)\\alpha<1/\(n\+1\), no threshold satisfies the calibration constraint, and the procedure abstains on every test input; more generally, when1/\(n\+1\)≤α<αℓ1/\(n\+1\)\\leq\\alpha<\\alpha\_\{\\ell\}in Eq\.[12](https://arxiv.org/html/2608.05439#S3.E12), the only feasible operating point is full abstention, soτ^=−∞\\widehat\{\\tau\}=\-\\inftyandg≡0g\\equiv 0\.We therefore assume below thatKαK\_\{\\alpha\}is well defined\.

For eachj∈\{1,…,n\+1\}j\\in\\\{1,\\ldots,n\+1\\\}, regard thejj\-th pair as the test example and the remainingnnpairs as the calibration sample\. Letτ^\(−j\)\\widehat\{\\tau\}^\{\(\-j\)\}be the largest feasible threshold selected from the distinct scores of the remaining sample together with−∞\-\\infty, and define the leave\-one\-out test loss

Aj=Zj​1​\[Sj≤τ^\(−j\)\]\.A\_\{j\}=Z\_\{j\}\\,\\mathbf\{1\}\\bigl\[S\_\{j\}\\leq\\widehat\{\\tau\}^\{\(\-j\)\}\\bigr\]\.
We first establish the deterministic bound

∑j=1n\+1Aj≤Kα\+1\.\\sum\_\{j=1\}^\{n\+1\}A\_\{j\}\\leq K\_\{\\alpha\}\+1\.\(16\)For anys∈\[0,1\]s\\in\[0,1\], letC​\(s\)=∑i=1n\+1Zi​1​\[Si≤s\]C\(s\)=\\sum\_\{i=1\}^\{n\+1\}Z\_\{i\}\\,\\mathbf\{1\}\[S\_\{i\}\\leq s\]be the number of errors in the full sample whose scores do not exceedss\. SupposeAj=1A\_\{j\}=1, so thatZj=1Z\_\{j\}=1andSj≤τ^\(−j\)S\_\{j\}\\leq\\widehat\{\\tau\}^\{\(\-j\)\}\. Feasibility ofτ^\(−j\)\\widehat\{\\tau\}^\{\(\-j\)\}gives

∑i≠jZi​1​\[Si≤τ^\(−j\)\]≤Kα,\\sum\_\{i\\neq j\}Z\_\{i\}\\,\\mathbf\{1\}\\bigl\[S\_\{i\}\\leq\\widehat\{\\tau\}^\{\(\-j\)\}\\bigr\]\\leq K\_\{\\alpha\},and the full\-sample count atτ^\(−j\)\\widehat\{\\tau\}^\{\(\-j\)\}adds at most thejj\-th error itself, so

C​\(Sj\)≤C​\(τ^\(−j\)\)≤Kα\+1\.C\(S\_\{j\}\)\\leq C\\bigl\(\\widehat\{\\tau\}^\{\(\-j\)\}\\bigr\)\\leq K\_\{\\alpha\}\+1\.Thus every index withAj=1A\_\{j\}=1is an error whose score lies among the firstKα\+1K\_\{\\alpha\}\+1errors in the nondecreasing ordering of the full sample, and there are at mostKα\+1K\_\{\\alpha\}\+1such indices, which proves Eq\.[16](https://arxiv.org/html/2608.05439#A1.E16)\. The argument uses only the counting functionCCand covers tied scores without modification\.

The map from then\+1n\+1pairs toAjA\_\{j\}applies the same selection rule to every held\-out index:τ^\(−j\)\\widehat\{\\tau\}^\{\(\-j\)\}is the largest feasible threshold among the distinct scores of the remainingnnpairs and−∞\-\\infty\. In particular, forj=n\+1j=n\+1the held\-out construction coincides with the deployed calibration, so

An\+1=Zn\+1​1​\[Sn\+1≤τ^\]\.A\_\{n\+1\}=Z\_\{n\+1\}\\,\\mathbf\{1\}\\bigl\[S\_\{n\+1\}\\leq\\widehat\{\\tau\}\\bigr\]\.Exchangeability of the pairs therefore implies𝔼​\[A1\]=⋯=𝔼​\[An\+1\]\\mathbb\{E\}\[A\_\{1\}\]=\\cdots=\\mathbb\{E\}\[A\_\{n\+1\}\], and

𝔼​\[Zn\+1​1​\[Sn\+1≤τ^\]\]=1n\+1​𝔼​\[∑j=1n\+1Aj\]≤Kα\+1n\+1≤α,\\mathbb\{E\}\\bigl\[Z\_\{n\+1\}\\,\\mathbf\{1\}\[S\_\{n\+1\}\\leq\\widehat\{\\tau\}\]\\bigr\]=\\frac\{1\}\{n\+1\}\\,\\mathbb\{E\}\\Bigl\[\\sum\_\{j=1\}^\{n\+1\}A\_\{j\}\\Bigr\]\\leq\\frac\{K\_\{\\alpha\}\+1\}\{n\+1\}\\leq\\alpha,where the first inequality is Eq\.[16](https://arxiv.org/html/2608.05439#A1.E16)and the second follows from the definition ofKαK\_\{\\alpha\}\. The deployed rule in Eq\.[11](https://arxiv.org/html/2608.05439#S3.E11)isg​\(X,φ^\)=𝟏​\[Sn\+1≤τ^\]g\(X,\\widehat\{\\varphi\}\)=\\mathbf\{1\}\[S\_\{n\+1\}\\leq\\widehat\{\\tau\}\]\. HenceRjoint=𝔼​\[g​\(X,φ^\)​Zn\+1\]=𝔼​\[Zn\+1​1​\[Sn\+1≤τ^\]\]≤αR\_\{\\mathrm\{joint\}\}=\\mathbb\{E\}\\bigl\[g\(X,\\widehat\{\\varphi\}\)\\,Z\_\{n\+1\}\\bigr\]=\\mathbb\{E\}\\bigl\[Z\_\{n\+1\}\\,\\mathbf\{1\}\[S\_\{n\+1\}\\leq\\widehat\{\\tau\}\]\\bigr\]\\leq\\alpha\. This proves Theorem[1](https://arxiv.org/html/2608.05439#Thmtheorem1)\.□\\square