Pith. sign in

REVIEW 1 major objections 5 minor 61 references

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

T0 review · 1 major / 5 minor · reviewed 2026-08-08 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read This paper introduces a conformal layer that lets any NL2TL translator either return a specification or abstain, with a finite-sample guarantee that the rate of accepted incorrect formulas stays below a user-chosen α.

desk verdict A well-executed application of conformal risk control to NL2TL with an honest evaluation; the main caveat is that the controlled risk is defined against the benchmark's equivalence oracle, which the authors themselves note is imperfect. read the letter →

arxiv 2608.05439 v1 pith:IYDZSTJY submitted 2026-08-05 cs.AI cs.LG

Yixuan Wang , Licheng Luo , Yu Fu , Kaidi Xu , Yue Dong , Mingyu Cai This is my paper · ORCID
classification cs.AIcs.LG
keywords conformalriskcontrolselectivepredictionnaturallanguagetotemporallogicabstentionback-translationscoringsemanticself-consistencyout-of-distributiondetectionspecifications
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper proposes a selection layer that any natural-language-to-temporal-logic translator can be wrapped in: instead of always emitting a formula, the system decides whether the generated specification is reliable enough to release, and otherwise abstains. Reliability is judged by two black-box scores computed only from the instruction and the generated formula—how well the formula back-translated into English agrees with the original instruction, and how stable the formula is across repeated random translations under semantic equivalence. A conformal risk-control calibration turns the fused score into an acceptance threshold, giving a finite-sample, distribution-free guarantee that the expected rate at which incorrect specifications are accepted for execution is at most a user-chosen $\alpha$. An upstream conformal filter on instruction embeddings also declines out-of-distribution inputs before translation is attempted. Validating on STL, LTL, and SpaTiaL, the paper reports that the risk-calibrated rule meets its budget in every evaluated setting while coverage-calibrated baselines do not.

What carries the argument

The load-bearing object is the conformal risk-control calibration rule applied to a loss that is non-increasing as the threshold tightens: $\ell_\tau = \mathbf{1}[S \le \tau]\,z$. Because lowering $\tau$ only removes accepted samples, the empirical calibration count $N_n(\tau)=\sum_{i=1}^n \mathbf{1}[S_i \le \tau] z_i$ is monotone in $\tau$, and the largest threshold satisfying $(N_n(\tau)+1)/(n+1)\le \alpha$ inherits the finite-sample risk bound under exchangeability. The scores feeding it are $S_{\mathrm{bt}} = 1 - A(x, B(\hat{\varphi}))$, the judge-assessed agreement between the instruction and the back-translation of the candidate formula, and $S_{\mathrm{sc}} = 1 - \frac{1}{k}\max_{1\le j\le k}|\{m : \hat{\varphi}^{(m)} \simeq \hat{\varphi}^{(j)}\}|$, the largest cluster of semantically equivalent samples in $k$ repeated translations; their equal-weight fusion is the default. The out-of-distribution gate is a conformal $p$-value $p(x)=(1+\sum_{i=1}^m \mathbf{1}[D(x_i) \ge D(x)])/(m+1)$ built from average $k$-nearest-neighbor embedding distances, which defers an in-distribution test instruction with probability at most $\delta$.

What would settle it

Run the full pipeline at $\alpha=0.05$ on the 114 instruction strings whose reference formulas conflict, and have independent human annotators judge whether each accepted specification matches the instruction; if a large share of checker-accepted outputs are semantically wrong by human judgment, the risk bound is controlling a proxy quantity rather than the user's intent.

Watch

Extended reading notes

Core claim

The paper's central claim is that the joint risk $R_{\mathrm{joint}} = \mathbb{E}[g(X,\hat{\varphi})\,Z]$, the probability that the input stream contains an accepted-and-wrong specification, can be held at any budget $\alpha$ by calibrating an acceptance threshold on data, with no assumptions about the translator beyond exchangeability of calibration and test pairs. The threshold is $\hat{\tau} = \max\{\tau \in T : \frac{n}{n+1}\hat{R}(\tau)+\frac{1}{n+1} \le \alpha\}$, where $\hat{R}(\tau)$ is the empirical fraction of calibration samples with score at most $\tau$ that are semantically wrong; the $+1$ term accounts for the unseen test point and turns the empirical constraint into a population guarantee. The proof is a leave-one-out symmetry argument over the $n+1$ exchangeable pairs, so the bound holds for any score in $[0,1]$, including the proposed fusion of back-translation fidelity and semantic self-consistency. A second theorem gives the same finite-sample control on the probability that the instruction-embedding filter defers an in-distribution input. If the paper is right, a planner can run with a hard budget on how often it executes a formula that does not match the reference, and abstention—not a prediction set—is what absorbs the risk.

Load-bearing premise

The load-bearing premise is that the benchmark's canonical equivalence checker correctly decides which translations are wrong; the bound controls the rate at which that checker's verdicts are accepted, so if the checker conflicts with human judgment—the paper itself notes 114 instruction strings with conflicting reference formulas—the guarantee does not cover whether the executed formula really matches the user's intent.

Editorial extensions

If this is right

  • With a fixed risk budget $\alpha$, a deployed planner can execute accepted specifications knowing that the expected rate of semantically incorrect releases is bounded by $\alpha$ under exchangeability.
  • Full abstention is the designed fallback: whenever calibration data cannot certify the requested budget, the system returns nothing rather than an unverified formula.
  • The framework applies to any logic generated by the common temporal-logic grammar; only the back-translator and judge rubric are logic-specific.
  • Coverage-based conformal calibration is the wrong objective for single-formula execution: in the paper's tables, risk-calibrated selection stays within its budget across evaluated settings while the coverage-calibrated baseline violates the budget in most cells.
  • The two-score fusion is the strongest score tested, improving error-ranking AUROC over either signal alone and, on STL, lowering the smallest certifiable risk floor from 0.270 to 0.048.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Editorial inference: withheld specifications can be routed to a human, a stronger translator, or a clarification dialogue at zero cost to the risk budget, since abstentions contribute nothing to joint risk.
  • Editorial inference: the two-score recipe of round-trip fidelity plus repeated-sample semantic dispersion transfers to other black-box structured generation tasks, such as text-to-SQL or code synthesis, wherever a canonical equivalence test exists.
  • Editorial inference: the instruction-embedding filter weakens but does not remove the exchangeability requirement; weighting calibration scores under covariate shift would be a natural strengthening for deployment beyond a single distribution.
  • Editorial inference: the framework could be extended to settings where a planner chooses among several accepted formulas, replacing the scalar acceptance decision with a calibrated ranking of candidates.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

1 major / 5 minor

Summary. The paper proposes SCP-NL2TL, a model-agnostic selection layer for natural-language-to-temporal-logic translators. The method computes two black-box reliability scores from an instruction-translation pair--back-translation fidelity and self-consistency over repeated translations--fuses them, and calibrates an acceptance threshold with conformal risk control so that the joint risk E[g(x,φhat)·1[φhat ≠ φ*]] is bounded by a user-chosen α under exchangeability. A conformal p-value filter on instruction embeddings screens out-of-distribution inputs before translation. The authors prove Theorem 1 (risk control) and Theorem 2 (filter validity), and evaluate the framework on STL, LTL, and SpaTiaL with two translators, per-tier calibration, score ablations, and a cross-tier drift protocol.

Significance. If the result holds, this is a useful and practical contribution: it converts any black-box NL2TL translator into an accept-or-abstain system with a finite-sample, distribution-free risk guarantee, without modifying the translator. The appendix proof of Theorem 1 is correct and self-contained, and the empirical evaluation is unusually careful: fixed prompts, 100 random resplits, explicit feasibility floors, per-tier calibration, bootstrap intervals for low-error cells, and a clear separation of score quality (AUROC) from calibration behavior. The fusion score is shown to improve ranking over either channel, and the risk-compliance tables support the claim that the risk-calibrated procedure meets the budget where the coverage-calibrated baseline does not. The main caveat is that the guarantee is defined with respect to the benchmark's canonical equivalence checker, not with respect to true semantic intent.

major comments (1)
  1. [Eq. (8) and Section 4] The central guarantee in Theorem 1 is stated for the loss z_i = 1[φhat_i ≠ φ*_i], where the inequality is evaluated by the benchmark-provided canonical equivalence checker. The abstract's claim that the method bounds 'the rate at which incorrect specifications are accepted for execution' therefore holds only for incorrectness relative to that checker, not for incorrectness relative to a user's semantic intent. The paper itself notes in Section 4 that 'the benchmark itself contains 114 instruction strings paired with conflicting reference formulas.' When the reference formula for an instruction is wrong or one of several conflicting references, a translation that captures the user's intent can be labeled incorrect and vice versa. The conformal guarantee remains valid for the proxy loss, but the operational message for safety-critical deployment is only as trustworthy as the oracle. This gap should be addressed by qualifying the abstract and introduction, by stating explicitly in Section 2 that the guarantee is relative to the benchmark's equivalence oracle, and by discussing how oracle errors affect the interpretation, e.g., the bound controls E[g·1[φhat ≠ φ*_oracle]] rather than the probability that an accepted formula fails to reflect user intent.
minor comments (5)
  1. [Section 4 and Table 4] Please clarify whether the numbers in the 'Abstained' panel are filter-only deferrals or full-pipeline abstentions. The sentence 'On the diagonal the filter defers 0.6%, 5.4%, and 0.7%' appears to attribute the full-pipeline abstention rate to the filter, which is confusing because the CRC threshold also abstains; with m=50 and δ=0.05 the discrete conformal p-value in Eq. (14) rejects at most about 3.9% of exchangeable inputs, so a filter-only 5.4% deferral would be surprising. The text should also reconcile 'returns four below the budget' with the five off-diagonal gated cells in Table 4 that are below 0.10.
  2. [Eq. (5) and Section 3.1] The self-consistency score S_sc takes values in [0, 1-1/k], not [0,1], since with k distinct samples the largest cluster has size 1 and the score equals 1-1/k. The sentence 'the subsequent calibration procedure ... accepts any score in [0,1]' should be phrased to avoid implying that S_sc itself spans [0,1].
  3. [Section 3.2, proof sketch] The main-text proof says the loss ℓτ is 'non-increasing as τ decreases,' which is correct but obscures that the acceptance region grows with τ. Because the conformal risk control theorem is usually stated for a loss that is non-increasing in the threshold parameter, please state the monotonicity direction explicitly to avoid confusion; the appendix proof is self-contained and sound.
  4. [Appendix A.3] The LTL rejected example is left as an unfilled template with placeholders ⟨eval_nl⟩, ⟨pred⟩, ⟨gold⟩, ⟨nl_back⟩, ⟨n⟩, and ⟨S⟩. Please replace it with a concrete traced example, as is done for the STL and SpaTiaL cases.
  5. [Appendix A.1] The sentence 'All results use the fixed prompts, data partitions, and calibration settings described in the main text' appears twice in the same paragraph; remove the duplicate.

Circularity Check

0 steps flagged · score 2.0 of 10

No circular derivation: the risk-control guarantee is a direct application of conformal risk control to a transparently defined loss, and score quality is measured empirically; minor self-citations are not load-bearing.

full rationale

The paper's central guarantee is not circular. Theorem 1 (Section 3.2) defines the loss z_i = 1[phi_hat_i != phi*_i] (Eq. 8) and the empirical joint risk (Eq. 9), then selects the threshold by the conformal risk control rule of Angelopoulos et al. (Eq. 10). The theorem is explicitly 'the conformal risk control theorem of Angelopoulos et al. [18] applied to this loss,' and Appendix A.6 supplies a self-contained leave-one-out proof. This is a standard external result applied to the paper's own loss, not an input renamed as a prediction. The scores (back-translation and self-consistency) are evaluated for ranking quality via AUROC before calibration (Table 1), so their discriminative value is empirical rather than assumed. There are self-citations — the SpaTiaL benchmark and the fine-tuned LLaMA translator come from Luo et al. [10], a paper including two of the present authors, and refs [40]-[44] are also from the same group — but none carries the statistical argument; Theorem 1 would hold for any translator and any fixed score. The paper itself flags the oracle limitation (Section 4: 'the benchmark itself contains 114 instruction strings paired with conflicting reference formulas'), which means the bound controls mismatch against the benchmark equivalence oracle rather than unmodeled oracle error; this is a correctness/scope limitation, not circularity. No fitted parameter is renamed as a prediction, and no uniqueness claim is imported from the authors' prior work.

Assumptions & free parameters 6 free parameters · 4 assumptions · 0 invented entities

The framework's statistical claims rest on two exchangeability assumptions (for CRC and for the OOD filter), on the fidelity of the benchmark equivalence oracle used to label errors, and on the score being fixed at deployment. The method introduces several hyperparameters (k in Eq. 13, k=5 samples in Eq. 5, temperature 1.0, equal fusion weight, δ=0.05) which are reasonable but not tuned in the main text. No new physical or conceptual entities are postulated.

free parameters (6)
  • k (nearest neighbors in OOD filter, Eq. 13) = not stated
    The number of neighbors k in the average k-NN distance of the instruction filter is a hyperparameter; the paper does not state its value or sensitivity analysis.
  • k (self-consistency samples, Eq. 5) = 5
    The number of repeated translator samples for the self-consistency score is fixed to 5, chosen by hand, with no stated sensitivity analysis in the main text.
  • sampling temperature for self-consistency = 1.0
    Temperature for repeated translations is set to 1.0; chosen by hand.
  • fusion weight lambda (Eq. 6) = 0.5 (equal weights)
    Default fusion is equal-weight; the paper reports robustness for lambda in [0.3,0.7] but does not tune or justify 0.5 in detail.
  • filter level delta = 0.05
    The deferral level for the conformal anomaly filter is fixed to 0.05; this is a user-chosen parameter.
  • embedding model = all-mpnet-base-v2
    The instruction embedding model is a fixed design choice; no comparison to other embeddings is provided.
assumptions (4)
  • domain assumption Calibration and test pairs are exchangeable within each group (Theorem 1).
    The joint-risk guarantee of Eq. 11 and Theorem 1 requires exchangeability of calibration and test (x, φ̂) pairs; under covariate shift the guarantee degrades, which the paper addresses only empirically via the filter.
  • domain assumption The benchmark equivalence checker ≡ correctly captures semantic correctness.
    Calibration errors z_i = 1[φ̂_i ≢ φ*_i] (Eq. 8) are defined relative to the benchmark-provided canonical equivalence checker; if the checker is incomplete or wrong, the controlled risk is not true semantic error. The paper notes 114 conflicting reference formulas in the benchmark.
  • domain assumption The test instruction is exchangeable with the deferral-calibration instructions for the filter (Theorem 2).
    The conformal p-value filter validity requires exchangeability of test and deferral-calibration instructions; this is distinct from the CRC exchangeability assumption.
  • domain assumption The score function S is fixed before calibration and identical at deployment.
    The CRC threshold is calibrated on the deployed score; any drift in the back-translator, judge, or sampling protocol would change S and void the guarantee.

how reviews work

0 comments
Cite this review

Pith. "Pith review of SCP-NL2TL: Selective Conformal Prediction with Semantic Verification for Natural Language to Temporal Logic Specifications." pith.science (2026). https://pith.science/paper/IYDZSTJY

@misc{pith2026260805439,
  author       = {Pith},
  title        = {Pith review of: SCP-NL2TL: Selective Conformal Prediction with Semantic Verification for Natural Language to Temporal Logic Specifications},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/IYDZSTJY}},
  note         = {Machine review of arXiv:2608.05439}
}
read the original 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.

Figures

Figures reproduced from arXiv: 2608.05439 by the authors.

Figure 1
Figure 1. Overview of the selective translation framework: instructions are screened before translation (level [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

61 extracted references · 41 canonical work pages

  1. [1]

    Adaptive teaching of temporal logic formulas to preference-based learners

    Zhe Xu, Yuxin Chen, and Ufuk Topcu. Adaptive teaching of temporal logic formulas to preference-based learners. InProceedings of the AAAI Conference on Artificial Intelligence, volume 35, pages 5061–5068, 2021

    work page 2021

  2. [2]

    Learning interpretable temporal properties from positive examples only

    Rajarshi Roy, Jean-Raphaël Gaglione, Nasim Baharisangari, Daniel Neider, Zhe Xu, and Ufuk Topcu. Learning interpretable temporal properties from positive examples only. InProceedings of the AAAI Conference on Artificial Intelligence, volume 37, pages 6507–6515, 2023

    work page 2023

  3. [3]

    Interactive plan selection using linear temporal logic, disjunctive action landmarks, and natural language instruction

    Tathagata Chakraborti, Jungkoo Kang, Francesco Fuggitti, Michael Katz, and Shirin Sohrabi. Interactive plan selection using linear temporal logic, disjunctive action landmarks, and natural language instruction. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 38, pages 23775–23777, 2024

    work page 2024

  4. [4]

    Proba- bilistic model checking of robots deployed in extreme environments

    Xingyu Zhao, Valentin Robu, David Flynn, Fateme Dinmohammadi, Michael Fisher, and Matt Webster. Proba- bilistic model checking of robots deployed in extreme environments. InProceedings of the AAAI Conference on Artificial Intelligence, volume 33, pages 8066–8074, 2019. 9 arXivTemplateA PREPRINT

    work page 2019

  5. [5]

    The temporal logic of programs

    Amir Pnueli. The temporal logic of programs. In18th annual symposium on foundations of computer science (sfcs 1977), pages 46–57. ieee, 1977

    1977

  6. [6]

    Monitoring temporal properties of continuous signals

    Oded Maler and Dejan Nickovic. Monitoring temporal properties of continuous signals. InInternational symposium on formal techniques in real-time and fault-tolerant systems, pages 152–166. Springer, 2004

    2004

  7. [7]

    Spatial: mon- itoring and planning of robotic tasks using spatio-temporal logic specifications.Autonomous Robots, 47(8): 1439–1462, 2023

    Christian Pek, Georg Friedrich Schuppe, Francesco Esposito, Jana Tumova, and Danica Kragic. Spatial: mon- itoring and planning of robotic tasks using spatio-temporal logic specifications.Autonomous Robots, 47(8): 1439–1462, 2023

    work page 2023

  8. [8]

    Deepstl: from english requirements to signal temporal logic

    Jie He, Ezio Bartocci, Dejan Ni ˇckovi´c, Haris Isakovic, and Radu Grosu. Deepstl: from english requirements to signal temporal logic. InProceedings of the 44th International Conference on Software Engineering, pages 610–622, 2022

    work page 2022

Show all 61 references
  1. [9]

    Nl2tl: Transforming natural languages to temporal logics using large language models

    Yongchao Chen, Rujul Gandhi, Yang Zhang, and Chuchu Fan. Nl2tl: Transforming natural languages to temporal logics using large language models. InProceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, pages 15880–15903, 2023

    2023

  2. [10]

    Licheng Luo, Kaier Liang, Yu Xia, and Mingyu Cai. Nl2spatial: Generating geometric spatio-temporal logic specifications from natural language for manipulation tasks.The IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), 2026

    2026

  3. [11]

    Calibrated interpretation: Confidence estimation in semantic parsing.Transactions of the Association for Computational Linguistics, 11:1213–1231, 2023

    Elias Stengel-Eskin and Benjamin Van Durme. Calibrated interpretation: Confidence estimation in semantic parsing.Transactions of the Association for Computational Linguistics, 11:1213–1231, 2023

    2023

  4. [12]

    A unified view of evaluation metrics for structured prediction

    Yunmo Chen, William Walden, Tongfei Chen, Aaron Steven White, and Benjamin Van Durme. A unified view of evaluation metrics for structured prediction. InProceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, pages 12868–12882, 2023

    2023

  5. [13]

    Semantic evaluation for text-to-sql with distilled test suites

    Ruiqi Zhong, Tao Yu, and Dan Klein. Semantic evaluation for text-to-sql with distilled test suites. InProceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP), pages 396–411, 2020

    2020

  6. [14]

    Confidence estimation for error detection in text-to-sql systems

    Oleg Somov and Elena Tutubalina. Confidence estimation for error detection in text-to-sql systems. InProceedings of the AAAI Conference on Artificial Intelligence, volume 39, pages 25137–25145, 2025

    2025

  7. [15]

    Springer, 2005

    Vladimir V ovk, Alexander Gammerman, and Glenn Shafer.Algorithmic learning in a random world. Springer, 2005

    2005

  8. [16]

    Selectivenet: A deep neural network with an integrated reject option

    Yonatan Geifman and Ran El-Yaniv. Selectivenet: A deep neural network with an integrated reject option. In International conference on machine learning, pages 2151–2159. PMLR, 2019

    2019

  9. [17]

    Selective generation for controllable language models.Advances in Neural Information Processing Systems, 37:50494–50527, 2024

    Minjae Lee, Kyungmin Kim, Taesoo Kim, and Sangdon Park. Selective generation for controllable language models.Advances in Neural Information Processing Systems, 37:50494–50527, 2024

    2024

  10. [18]

    Conformal risk control

    Anastasios Angelopoulos, Stephen Bates, Adam Fisch, Lihua Lei, and Tal Schuster. Conformal risk control. In B. Kim, Y . Yue, S. Chaudhuri, K. Fragkiadaki, M. Khan, and Y . Sun, editors,International Conference on Learning Representations, volume 2024, pages 55198–55218, 2024. ...

    2024

  11. [19]

    SConU: Selective conformal uncertainty in large language models

    Zhiyuan Wang, Qingni Wang, Yue Zhang, Tianlong Chen, Xiaofeng Zhu, Xiaoshuang Shi, and Kaidi Xu. SConU: Selective conformal uncertainty in large language models. In Wanxiang Che, Joyce Nabende, Ekaterina Shutova, and Mohammad Taher Pilehvar, editors,Proceedings of the 63rd Ann...

    2025 doi

  12. [20]

    Sorry dave, i’m afraid i can’t do that: Explaining unachievable robot tasks using natural language

    Vasumathi Raman, Constantine Lignos, Cameron Finucane, Kenton CT Lee, Mitchell P Marcus, and Hadas Kress-Gazit. Sorry dave, i’m afraid i can’t do that: Explaining unachievable robot tasks using natural language. In Robotics: science and systems, volume 2, pages 2–1. Berlin, Ge...

    2013

  13. [21]

    Sequence-to-sequence language grounding of non-markovian task specifications

    Nakul Gopalan, Dilip Arumugam, Lawson LS Wong, and Stefanie Tellex. Sequence-to-sequence language grounding of non-markovian task specifications. InRobotics: Science and Systems, volume 2018, 2018

    2018

  14. [22]

    Learning a natural-language to ltl executable semantic parser for grounded robotics

    Christopher Wang, Candace Ross, Yen-Ling Kuo, Boris Katz, and Andrei Barbu. Learning a natural-language to ltl executable semantic parser for grounded robotics. InConference on Robot Learning, pages 1706–1718. PMLR, 2021

    2021

  15. [23]

    nl2spec: Interactively translating unstructured natural language to temporal logics with large language models

    Matthias Cosler, Christopher Hahn, Daniel Mendoza, Frederik Schmitt, and Caroline Trippel. nl2spec: Interactively translating unstructured natural language to temporal logics with large language models. InInternational Conference on Computer Aided Verification, pages 383–396. ...

    2023

  16. [24]

    Translating natural language to temporal logics with large language models and model checkers

    Daniel Mendoza, Christopher Hahn, and Caroline Trippel. Translating natural language to temporal logics with large language models and model checkers. In2024 Formal Methods in Computer-Aided Design (FMCAD), pages 1–11. IEEE, 2024

    2024

  17. [25]

    Enhancing transformation from natural language to signal temporal logic using llms with diverse external knowledge

    Yue Fang, Zhi Jin, Jie An, Hongshen Chen, Xiaohong Chen, and Naijun Zhan. Enhancing transformation from natural language to signal temporal logic using llms with diverse external knowledge. InFindings of the Association for Computational Linguistics: ACL 2025, pages 10446–10458, 2025

    2025

  18. [26]

    Grammar-forced translation of natural language to temporal logic using llms.arXiv preprint arXiv:2512.16814, 2025

    William English, Dominic Simon, Sumit Kumar Jha, and Rickard Ewetz. Grammar-forced translation of natural language to temporal logic using llms.arXiv preprint arXiv:2512.16814, 2025

    2025

  19. [27]

    Nl2ltl–a python package for converting natural language (nl) instructions to linear temporal logic (ltl) formulas

    Francesco Fuggitti and Tathagata Chakraborti. Nl2ltl–a python package for converting natural language (nl) instructions to linear temporal logic (ltl) formulas. InProceedings of the AAAI Conference on Artificial Intelligence, volume 37, pages 16428–16430, 2023

    2023

  20. [28]

    Conformalnl2ltl: Translating natural language instructions into temporal logic formulas with conformal correctness guarantees.arXiv preprint arXiv:2504.21022, 2025

    David Smith Sundarsingh, Jun Wang, Jyotirmoy V Deshmukh, and Yiannis Kantaros. Conformalnl2ltl: Translating natural language instructions into temporal logic formulas with conformal correctness guarantees.arXiv preprint arXiv:2504.21022, 2025

    2025

  21. [29]

    Api is enough: Conformal prediction for large language models without logit-access

    Jiayuan Su, Jing Luo, Hongwei Wang, and Lu Cheng. Api is enough: Conformal prediction for large language models without logit-access. InFindings of the Association for Computational Linguistics: EMNLP 2024, pages 979–995, 2024

    2024

  22. [30]

    Conu: Conformal uncertainty in large language models with correctness coverage guarantees

    Zhiyuan Wang, Jinhao Duan, Lu Cheng, Yue Zhang, Qingni Wang, Xiaoshuang Shi, Kaidi Xu, Heng Tao Shen, and Xiaofeng Zhu. Conu: Conformal uncertainty in large language models with correctness coverage guarantees. InFindings of the Association for Computational Linguistics: EMNLP...

    2024

  23. [31]

    Conformal language modeling

    Victor Quach, Adam Fisch, Tal Schuster, Adam Yala, Jae Ho Sohn, Tommi Jaakkola, and Regina Barzilay. Conformal language modeling. InInternational Conference on Learning Representations, volume 2024, pages 11654–11681, 2024

    2024

  24. [32]

    Language models with conformal factuality guarantees.arXiv preprint arXiv:2402.10978, 2024

    Christopher Mohri and Tatsunori Hashimoto. Language models with conformal factuality guarantees.arXiv preprint arXiv:2402.10978, 2024

    2024 arXiv

  25. [33]

    Prompt risk control: A rigorous framework for responsible deployment of large language models

    Thomas Zollo, Todd Morrill, Zhun Deng, Jake Snell, Toniann Pitassi, and Richard Zemel. Prompt risk control: A rigorous framework for responsible deployment of large language models. InInternational Conference on Learning Representations, volume 2024, pages 4045–4067, 2024

    2024

  26. [34]

    Large language model validity via enhanced conformal prediction methods.Advances in Neural Information Processing Systems, 37:114812–114842, 2024

    John J Cherian, Isaac Gibbs, and Emmanuel J Candès. Large language model validity via enhanced conformal prediction methods.Advances in Neural Information Processing Systems, 37:114812–114842, 2024

    2024

  27. [35]

    Detecting hallucinations in large language models using semantic entropy.Nature, 630(8017):625–630, 2024

    Sebastian Farquhar, Jannik Kossen, Lorenz Kuhn, and Yarin Gal. Detecting hallucinations in large language models using semantic entropy.Nature, 630(8017):625–630, 2024

    2024

  28. [36]

    Non-exchangeable conformal risk control

    António Farinhas, Chrysoula Zerva, Dennis Ulmer, and Andre Martins. Non-exchangeable conformal risk control. InInternational Conference on Learning Representations, volume 2024, pages 50952–50966, 2024

    2024

  29. [37]

    Conformal prediction under covariate shift.Advances in neural information processing systems, 32, 2019

    Ryan J Tibshirani, Rina Foygel Barber, Emmanuel Candes, and Aaditya Ramdas. Conformal prediction under covariate shift.Advances in neural information processing systems, 32, 2019

    2019

  30. [38]

    Conformal prediction beyond exchangeability.The Annals of Statistics, 51(2):816–845, 2023

    Rina Foygel Barber, Emmanuel J Candes, Aaditya Ramdas, and Ryan J Tibshirani. Conformal prediction beyond exchangeability.The Annals of Statistics, 51(2):816–845, 2023

    2023

  31. [39]

    Karen Leung, Nikos Aréchiga, and Marco Pavone. Backpropagation through signal temporal logic specifications: Infusing logical structure into gradient-based methods.The International Journal of Robotics Research, 42(6): 356–370, 2023

    2023

  32. [40]

    Tlinet: Differentiable neural network temporal logic inference.arXiv preprint arXiv:2405.06670, 2024

    Danyang Li, Mingyu Cai, Cristian-Ioan Vasile, and Roberto Tron. Tlinet: Differentiable neural network temporal logic inference.arXiv preprint arXiv:2405.06670, 2024

    2024 arXiv

  33. [41]

    Learning signal temporal logic through neural network for interpretable classification

    Danyang Li, Mingyu Cai, Cristian-Ioan Vasile, and Roberto Tron. Learning signal temporal logic through neural network for interpretable classification. In2023 American Control Conference (ACC), pages 1907–1914. IEEE, 2023

    1907

  34. [42]

    Licheng Luo, Kaier Liang, Cristian-Ioan Vasile, and Mingyu Cai. Differentiable spatial: Symbolic learning and reasoning with geometric temporal logic for manipulation tasks.The IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), 2026

    2026

  35. [43]

    Conformal prediction for signal temporal logic inference.arXiv preprint arXiv:2509.25473, 2025

    Danyang Li, Yixuan Wang, Matthew Cleaveland, Mingyu Cai, and Roberto Tron. Conformal prediction for signal temporal logic inference.arXiv preprint arXiv:2509.25473, 2025. Accepted at the 65th IEEE Conference on Decision and Control. 11 arXivTemplateA PREPRINT

    2025

  36. [44]

    Conformalized signal temporal logic inference under covariate shift.arXiv preprint arXiv:2603.27062, 2026

    Yixuan Wang, Danyang Li, Matthew Cleaveland, Roberto Tron, and Mingyu Cai. Conformalized signal temporal logic inference under covariate shift.arXiv preprint arXiv:2603.27062, 2026. Accepted at the 65th IEEE Conference on Decision and Control

    2026

  37. [45]

    Conformal temporal logic planning using large language models.ACM Transactions on Cyber-Physical Systems, 2023

    Jun Wang, Jiaming Tong, Kaiyuan Tan, Yevgeniy V orobeychik, and Yiannis Kantaros. Conformal temporal logic planning using large language models.ACM Transactions on Cyber-Physical Systems, 2023

    2023

  38. [46]

    Probabilistically correct language-based multi-robot planning using conformal prediction.IEEE Robotics and Automation Letters, 10(1):160–167, 2024

    Jun Wang, Guocheng He, and Yiannis Kantaros. Probabilistically correct language-based multi-robot planning using conformal prediction.IEEE Robotics and Automation Letters, 10(1):160–167, 2024

    2024

  39. [47]

    Robots that ask for help: Uncertainty alignment for large language model planners.arXiv preprint arXiv:2307.01928, 2023

    Allen Z Ren, Anushri Dixit, Alexandra Bodrova, Sumeet Singh, Stephen Tu, Noah Brown, Peng Xu, Leila Takayama, Fei Xia, Jake Varley, et al. Robots that ask for help: Uncertainty alignment for large language model planners.arXiv preprint arXiv:2307.01928, 2023

    2023 arXiv

  40. [48]

    Safe planning in dynamic environments using conformal prediction.IEEE Robotics and Automation Letters, 8(8):5116–5123, 2023

    Lars Lindemann, Matthew Cleaveland, Gihyun Shim, and George J Pappas. Safe planning in dynamic environments using conformal prediction.IEEE Robotics and Automation Letters, 8(8):5116–5123, 2023

    2023

  41. [49]

    Testing for outliers with conformal p-values.The Annals of Statistics, 51(1):149–178, 2023

    Stephen Bates, Emmanuel Candès, Lihua Lei, Yaniv Romano, and Matteo Sesia. Testing for outliers with conformal p-values.The Annals of Statistics, 51(1):149–178, 2023

    2023

  42. [50]

    Selection by prediction with conformal p-values.Journal of Machine Learning Research, 24(244):1–41, 2023

    Ying Jin and Emmanuel J Candès. Selection by prediction with conformal p-values.Journal of Machine Learning Research, 24(244):1–41, 2023

    2023

  43. [51]

    Inductive conformal anomaly detection for sequential detection of anomalous sub-trajectories.Annals of Mathematics and Artificial Intelligence, 74(1):67–94, 2015

    Rikard Laxhammar and Göran Falkman. Inductive conformal anomaly detection for sequential detection of anomalous sub-trajectories.Annals of Mathematics and Artificial Intelligence, 74(1):67–94, 2015

    2015

  44. [52]

    Selective conformal risk control.arXiv preprint arXiv:2512.12844, 2025

    Yunpeng Xu, Wenge Guo, and Zhi Wei. Selective conformal risk control.arXiv preprint arXiv:2512.12844, 2025

    2025 arXiv

  45. [53]

    Out-of-distribution detection with deep nearest neighbors

    Yiyou Sun, Yifei Ming, Xiaojin Zhu, and Yixuan Li. Out-of-distribution detection with deep nearest neighbors. In Kamalika Chaudhuri, Stefanie Jegelka, Le Song, Csaba Szepesvari, Gang Niu, and Sivan Sabato, editors, Proceedings of the 39th International Conference on Machine Le...

    2022

  46. [54]

    MIT press, 2008

    Christel Baier and Joost-Pieter Katoen.Principles of model checking. MIT press, 2008

    2008

  47. [55]

    Springer, 2017

    Calin Belta, Boyan Yordanov, and Ebru Aydin Gol.Formal methods for discrete-time dynamical systems, volume 89. Springer, 2017

    2017

  48. [56]

    Shifting attention to relevance: Towards the predictive uncertainty quantification of free-form large language models

    Jinhao Duan, Hao Cheng, Shiqi Wang, Alex Zavalny, Chenan Wang, Renjing Xu, Bhavya Kailkhura, and Kaidi Xu. Shifting attention to relevance: Towards the predictive uncertainty quantification of free-form large language models. InProceedings of the 62nd Annual Meeting of the Ass...

    2024

  49. [57]

    Lang2ltl: Translating natural language commands to temporal specification with large language models

    Jason Xinyu Liu, Ziyi Yang, Benjamin Schornstein, Sam Liang, Ifrah Idrees, Stefanie Tellex, and Ankit Shah. Lang2ltl: Translating natural language commands to temporal specification with large language models. In Workshop on Language and Robotics at CoRL 2022, 2022

    2022

  50. [58]

    Revisiting round-trip translation for quality estimation

    Jihyung Moon, Hyunchang Cho, and Eunjeong L Park. Revisiting round-trip translation for quality estimation. In Proceedings of the 22nd Annual Conference of the European Association for Machine Translation, pages 91–104, 2020

    2020

  51. [59]

    Judging llm-as-a-judge with mt-bench and chatbot arena.Advances in neural information processing systems, 36:46595–46623, 2023

    Lianmin Zheng, Wei-Lin Chiang, Ying Sheng, Siyuan Zhuang, Zhanghao Wu, Yonghao Zhuang, Zi Lin, Zhuohan Li, Dacheng Li, Eric Xing, et al. Judging llm-as-a-judge with mt-bench and chatbot arena.Advances in neural information processing systems, 36:46595–46623, 2023

    2023

  52. [60]

    Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou

    Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc V Le, Ed H. Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou. Self-consistency improves chain of thought reasoning in language models. InThe Eleventh International Conference on Learning Representations, 2023. URL https://op...

    2023

  53. [61]

    If ( prop_1 ) then at a time within the next 12 to 50 time units ultimately ( prop_2 )

    James A Hanley and Barbara J McNeil. The meaning and use of the area under a receiver operating characteristic (roc) curve.Radiology, 143(1):29–36, 1982. 12 arXivTemplateA PREPRINT A Appendix A.1 Reproducing Results All reported results use the fixed prompts, data partitions, ...

    1982

Pith tools

Reviewed August 8, 2026 · model on record in the stance chip above.