Enhancing Transformation from Natural Language to Signal Temporal Logic Using LLMs with Diverse External Knowledge

Hongshen Chen; Jie An; Naijun Zhan; Xiaohong Chen; Yue Fang; Zhi Jin

REVIEW 4 major objections 5 minor 2 cited by

Enhancing Transformation from Natural Language to Signal Temporal Logic Using LLMs with Diverse External Knowledge

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

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

Pith's one-line read Natural-language requirements can be translated into Signal Temporal Logic most accurately by generating a draft with a fine-tuned LLM and refining it with GPT-4 guided by similar NL-STL examples, the paper claims.

desk verdict Solid dataset and pipeline for NL-to-STL, but the DeepSTL gain may be inflated by retrieval from a template-generated benchmark with likely train/test overlap. read the letter →

arxiv 2505.20658 v2 pith:6DHBEE23 submitted 2025-05-27 cs.CL

Yue Fang , Zhi Jin , Jie An , Hongshen Chen , Xiaohong Chen , Naijun Zhan This is my paper

classification cs.CL

keywords naturallanguagetoSignalTemporalLogicSTLtranslationdatasetconstructionwithLLMsgenerate-then-refineretrieval-augmentedrefinementformalspecificationgenerationLLMfine-tuning

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

Signal Temporal Logic (STL) is a formal language for specifying the timing and value constraints of cyber-physical systems, but writing STL formulas by hand is slow and error-prone. This paper attacks the bottleneck from two sides: it builds STL-DivEn, a 16,000-pair dataset of natural-language requirements paired with STL formulas, and it introduces KGST, a generate-then-refine translation method. In KGST, a fine-tuned large language model first drafts an STL formula, then GPT-4 rewrites that draft using the five most similar NL-STL pairs retrieved from the training set as reference knowledge. On STL-DivEn and on the existing DeepSTL test set, KGST reports the highest formula accuracy, template accuracy, BLEU, and human-judged correctness among the tested methods. The intended payoff is that engineers could convert everyday requirements into machine-checkable specifications without being logicians.

What carries the argument

The load-bearing mechanism is a generate-then-refine loop with an external knowledge base. The first stage is a fine-tuned LLaMA-3-8B generator; the second is GPT-4 prompting with the top-5 nearest NL-STL pairs retrieved from the training set by similarity, plus the original sentence and the draft formula. The external pairs supply concrete operator-scope patterns, timing intervals, and identifier conventions that the draft may have gotten wrong. The dataset itself is the second piece of machinery: STL-DivEn's construction, with hand-crafted seeds, k-means exemplar selection, GPT-4 augmentation, ROUGE-based diversity filtering, and human validation, is designed so that retrieved references cover varied formula shapes and vocabulary. The ablation results, which show that removing either fine-tuning or refinement lowers accuracy and that GPT-4 self-refinement without external references performs worse, are what carry the claim that both stages matter.

What would settle it

Take the 2,000 test sentences from STL-DivEn, compute their ROUGE similarity to the top-5 retrieved training pairs, and rerun KGST with the retrieval pool restricted to pairs whose similarity to the test sentence is below 0.5, or replaced by random pairs; if formula accuracy drops toward the no-refinement level, the measured gains come from retrieval rather than from general translation ability.

Watch

Extended reading notes

Core claim

The paper's central claim is that retrieval-guided refinement, not a stronger single model, is what pushes NL-to-STL translation past previous limits. The authors construct STL-DivEn by hand-writing 120 seed pairs, clustering them to choose representative exemplars, asking GPT-4 to generate new pairs from those exemplars, filtering by syntax checks and ROUGE-diversity thresholds, and validating by human annotators. They then fine-tune LLaMA-3-8B on the dataset to produce a preliminary formula for a new natural-language sentence, retrieve the top-5 most similar NL-STL pairs from the training set, and instruct GPT-4 to correct the preliminary formula against those references. The reported result is that this pipeline achieves STL formula accuracy of 0.5587 on STL-DivEn and 0.4538 on DeepSTL, ahead of GPT-4, DeepSeek, and self-refinement, with human correctness ratings of 62.4% and 54.6%. The authors interpret the gap between KGST and GPT-4-based self-refinement as evidence that external formula examples carry information the model's internal knowledge lacks.

Load-bearing premise

The evaluation assumes that the random training/test split keeps test sentences from being near-duplicates of the retrieved training references, and that exact token-aligned formula matching measures correctness; if either assumption fails, KGST's reported edge could reflect copying from memory rather than translation skill.

Editorial extensions

If this is right

A 16,000-pair NL-STL corpus now exists that is more diverse in vocabulary, formula structure, and identifier usage than DeepSTL, giving the field a common training and evaluation resource.
A fine-tuned draft followed by external-knowledge refinement is a practical recipe: on both STL-DivEn and DeepSTL it outperforms prompting strong LLMs directly and outperforms self-refinement.
Because KGST's gains hold on DeepSTL, a dataset generated from grammar templates rather than LLMs, the method is not tied to the style of its own training data.
Scaling experiments reported in the paper show formula accuracy rising with dataset size, implying that further dataset expansion is a plausible route to better translation.
The refinement step specifically reduces operator misuse, value errors, syntax violations, and semantic mismatches, per the paper's error-tracking analysis.

Reading between the lines

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

Beyond the paper's own claims, the retrieval design suggests that a test sentence with a near-duplicate training sentence could be answered largely by copying; measuring KGST on a deduplicated split would separate retrieval memory from genuine translation skill.
The same retrieve-and-refine pattern should transfer to other formal-specification tasks, such as LTL, timed automata, or executable assertions, since the only ingredient it needs is a corpus of reference pairs and a judge LLM.
If exact token-aligned accuracy were replaced by semantic equivalence checks, for example by monitoring the predicted and reference formulas on random signals, absolute accuracies would probably shift, though the ranking of a retrieval-guided pipeline over self-refinement might persist.

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.

Desk Editor's Note

read the letter

The paper gives you two things worth having: a new 16k-pair NL-STL dataset called STL-DivEn, built with a sensible generate-filter-validate loop, and a generate-then-refine pipeline (KGST) that fine-tunes LLaMA-3-8B and then has GPT-4 refine the draft using retrieved NL-STL pairs. The reported gains over GPT-4 and DeepSeek on STL-DivEn are plausible, and the ablations show both fine-tuning and refinement contribute. The diversity statistics make a real case that STL-DivEn is richer than DeepSTL, and the human evaluation supports the direction. The authors also acknowledge the dataset's GPT-4 origin and that it may not cover real-world requirement patterns, which is honest.

The soft spots are mostly in the evaluation. There are no error bars or significance tests anywhere, and the STL Formula Accuracy metric in Appendix B is confusing as written—the example doesn't line up with its own template. There are also numerical mismatches between the text and Table 1 (e.g., GPT-4 BLEU on STL-DivEn is 0.0831 in the table but 0.1931 in the text; DeepSeek template accuracy differs too). These should be fixed before publication.

The bigger concern is the DeepSTL result. DeepSTL is template-generated, and the paper's own statistics show 120k sentences from a vocabulary of only 265 words—so exact or near-exact duplicates are likely across the random 14k/2k split. Since KGST retrieves top-5 similar pairs from the training split and feeds them to GPT-4, a test sentence with a near-identical training match puts the ground-truth STL directly in the refinement context. That could explain the large jump from 0.25 to 0.45 on DeepSTL. The stress-test note about STL-DivEn itself does not land the same way: the ROUGE < 0.5 filter is applied against the full growing seed set, so within STL-DivEn no two pairs should be near-duplicates of each other. The same-model concern (GPT-4 generates the data and does the refinement) is real but partly mitigated by the external DeepSTL benchmark and the human evaluation.

This is a useful engineering contribution for the NL-to-STL subfield, and the dataset is probably worth having regardless of the pipeline. It deserves serious peer review, but the reviewers should ask for a deduplication analysis on DeepSTL, significance testing or error bars, and a cleaned-up metric definition. I would engage with it, and if the authors release the code and data, I'd likely cite it.

Referee Report

4 major / 5 minor

Summary. The paper introduces STL-DivEn, a 16,000-pair natural-language-to-STL dataset constructed through a seed set, clustering-based exemplar selection, GPT-4-driven augmentation, ROUGE-based diversity filtering, and human validation. It also proposes KGST, a generate-then-refine framework that fine-tunes LLaMA-3-8B to produce a preliminary STL formula and then uses GPT-4, guided by the top-5 most similar NL-STL pairs retrieved from the training set, to refine it. The authors report that KGST achieves the best STL Formula Accuracy, Template Accuracy, and BLEU on both STL-DivEn (0.5587, 0.5627, 0.2142) and DeepSTL (0.4538, 0.4939, 0.5686) compared to baselines, and that human evaluation marks KGST's outputs correct on 62.4% of STL-DivEn and 54.6% of DeepSTL test cases. The central claim is that KGST substantially improves NL-to-STL transformation accuracy and that STL-DivEn is a more diverse and useful dataset than existing benchmarks.

Significance. If the results hold, the paper would provide a valuable public dataset and a transferable pipeline for a practically relevant but data-scarce task. The strength is that the method is evaluated on both the self-created dataset and an established external benchmark (DeepSTL), and the repository is publicly available. However, the quantitative evidence as presented does not yet fully establish the central claim: the evaluation lacks train/test deduplication safeguards, the primary metric is a strict token-level match that penalizes semantically equivalent formulas, no variance or significance testing is reported, and the self-created test set shares its generation model (GPT-4) with KGST's refinement stage. These gaps leave open the possibility that the reported gains are inflated by retrieval of near-duplicate references or by GPT-4 self-consistency rather than by genuine translation skill.

major comments (4)

[Section 5.1 / Section 4.1] The STL-DivEn construction pipeline filters new pairs against the growing seed set using a ROUGE threshold of 0.5 (Section 4.1), but the later random split of 16,000 pairs into 14,000 training and 2,000 test instances (Section 5.1) is not accompanied by any documented cross-split deduplication. Because KGST retrieves the top-5 NL-STL pairs from the training set and places them in the GPT-4 refinement prompt (Section 4.2, Figure 8), a test sentence that has a near-duplicate in the training set would put the reference STL formula directly into the refinement context. The reported STL Formula Accuracy of 0.5587 on STL-DivEn and 0.4538 on DeepSTL could therefore overstate the method's translation ability. Please report the maximum ROUGE-L or embedding similarity between each test sentence and its retrieved training references, and run an ablation that removes retrieved pairs with high similarity to the input (or retrieves from a disjoint pool) to quantify the effect of near-duplicate exposure.
[Appendix B / Section 5.1] The STL Formula Accuracy metric defined in Appendix B is a token-level alignment score: it treats formulas as token sequences and counts the number of tokens that appear in the same positions in the reference and prediction. This penalizes semantically equivalent formulas that differ in variable names, operator ordering, or syntactically different but logically equivalent forms (e.g., the disjunctive form of |z2|>0.5 as z2<-0.5 or z2>0.5). Table 5's Case 2 is a concrete example where the KGST output and the ground truth are semantically equivalent yet would not receive a perfect token-alignment score. Since Table 1 relies on this metric for the main quantitative comparison, the paper should supplement it with a semantic-equivalence evaluation, such as a monitor-based equivalence check on sampled signals or a human-labeled semantic correctness sample, and report the correlation between token accuracy and semantic correctness.
[Sections 5.2.1 and 5.2.2] Tables 1 and 2 report single point estimates without standard deviations, confidence intervals, or significance tests. The differences between KGST and the strongest baselines on STL-DivEn are moderate (0.5587 vs. 0.4790 for formula accuracy; 62.4% vs. 55.0% in human evaluation), and the human evaluation is based on 100 pairs with five annotators but does not report inter-annotator agreement or how individual labels are aggregated. Please report means and variances over multiple fine-tuning seeds and refinement runs, and provide a paired significance test (e.g., McNemar's test on the same test instances) for the headline comparisons with KGST.
[Sections 4.2 and 5.2.1] The STL-DivEn test set was generated by GPT-4 with human validation, and KGST's refinement stage also uses GPT-4 to rewrite the preliminary formula. On STL-DivEn, some of KGST's advantage may therefore reflect GPT-4's preference for formulas that resemble its own generation style rather than a generalizable improvement in NL-to-STL translation. The large gain on DeepSTL mitigates this concern, but it is based on a single external benchmark whose 16,000-sample subset was not described in enough detail. Please validate on an additional external or human-authored held-out test set, or replace the GPT-4 refinement with a different model in a controlled experiment, to separate model-consistency effects from genuine translation improvement.

minor comments (5)

[Appendix B] The metric example describes the formula as 'eventually (a < 5)' and 'eventually (b < 5)', but the formula and template are written with 'G' instead of 'F' and the subsequent token-alignment explanation refers to 'G'. Please correct this inconsistency so the example matches the intended temporal operator.
[Section 5.3.1 / Table 3] The 'N-gram diversity' statistic used to support the dataset diversity claim is not defined in the main text. Please state its definition (e.g., ratio of distinct n-grams to total n-grams), the value of n used, and the averaging procedure so that Table 3 is reproducible.
[Section 5.2.2] The human evaluation section does not explain how the five annotators' labels are combined into the reported correctness percentage. Please clarify whether the result is a majority vote, full agreement, or an average over annotators, and report inter-annotator agreement (e.g., Fleiss' kappa).
[Section 5.1] For DeepSTL, the paper says 14,000 training and 2,000 test samples are randomly selected, but DeepSTL contains 120,000 sentences (Table 3b). Please clarify how the 16,000-sample subset was sampled from the full DeepSTL dataset and whether the split was stratified by template or operator distribution.
[Section 4.1] The choices of k=5 for k-means clustering and the ROUGE threshold of 0.5 are presented without justification or sensitivity analysis. Please report how these hyperparameters were chosen and whether the dataset statistics change materially for nearby values.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: KGST's gain is measured against held-out splits and an external benchmark, with no fitted quantity defined in terms of its own prediction.

full rationale

The paper's derivation chain is a dataset-construction pipeline plus a generate-then-refine model, not a formal derivation in which an output is defined from an input. The STL-DivEn dataset is built from manually written seeds, GPT-4 augmentation, ROUGE-based filtering against the growing seed set, and two-stage human validation; the KGST framework is evaluated on held-out test splits (14,000/2,000) of STL-DivEn and on the external DeepSTL benchmark, so the central comparison has independent content. No equation in the paper defines a predicted formula in terms of the same fitted value, and no load-bearing claim rests on a self-citation: the cited prior systems (DeepSTL, NL2TL, Self-Refine) are external baselines, and DeepSTL is an independently constructed benchmark. The retrieval of the top-5 similar pairs from the training split is a designed component of the method; Table 4's ablations show that the full KGST (0.5587) improves over both retrieval-only (0.5360) and fine-tuning-only (0.4956) variants, so the reported result is not identical to retrieval alone. The Limitations section concedes that the dataset is generated by GPT-4 rather than drawn from real-world requirement documents; that is a domain-coverage and bias caveat, not a circularity. A potential train/test near-duplicate leakage in STL-DivEn would be an evaluation-validity concern, but the paper's ROUGE<0.5 generation filter and random split do not by themselves exhibit a test sample whose reference formula is placed in the retrieved context, and no specific reduction can be quoted; per the evidence standard, this cannot be counted as a demonstrated circular step.

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

The central empirical claims rest on the quality and neutrality of the NL-STL datasets and the evaluation metrics. The paper introduces no new physical or theoretical entity, so invented_entities is empty. The free parameters and assumptions above are the choices a replication attempt would have to fix or question, especially the retrieval count K=5, the ROUGE threshold 0.5, and the assumption that GPT-4-generated, human-validated test data measures general NL-to-STL ability.

free parameters (4)

Retrieval count K = 5
KGST fixes the number of top similar NL-STL reference pairs to 5; no sensitivity analysis is reported, so the result depends on this hand-chosen value.
Cluster count k for seed selection = 5
Section 4.1 uses k-means with five centers without justification or ablation for the number of clusters.
ROUGE diversity threshold = 0.5
New NL-STL pairs are accepted only when ROUGE score against current seed pairs is below 0.5; this threshold directly shapes dataset composition and diversity claims.
Seed set size = 120
The manual seed set is fixed at 120 pairs, 40 from each of three domains; final dataset diversity is constrained by this starting point.

assumptions (5)

standard math The STL syntax and semantics in Section 3, including the G/F/U operators and the satisfaction relation, are the correct target formalism.
Standard formalization, cited to Maler and Ničković (2004); the paper uses it without modification.
domain assumption Token-level formula accuracy and template accuracy are valid proxies for semantic correctness of NL-to-STL translation.
Appendix B defines the metrics by token alignment; no semantic equivalence check is used, so the evaluation assumes exact canonical syntax matters.
domain assumption GPT-4-generated NL-STL pairs that pass syntax checks and human validation constitute correct ground truth.
Dataset construction uses GPT-4 as generator and human annotators as validators; the paper's own Limitations section notes the data may be biased or unrepresentative of real-world CPS requirements.
domain assumption Retrieving the top-5 similar pairs from the training split is a legitimate use of external knowledge and does not leak test information.
Section 5.1 states reference pairs come from the corresponding training set; no train/test deduplication is reported, so leakage-free retrieval is assumed.
ad hoc to paper ROUGE score below 0.5 against the growing seed set guarantees sufficient diversity of new NL-STL pairs.
Section 4.1 uses this threshold as the diversity filter; no validation shows that this prevents near-duplicate test/training sentences or covers real-world pattern diversity.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Enhancing Transformation from Natural Language to Signal Temporal Logic Using LLMs with Diverse External Knowledge." pith.science (2026). https://pith.science/paper/6DHBEE23

@misc{pith2026250520658,
  author       = {Pith},
  title        = {Pith review of: Enhancing Transformation from Natural Language to Signal Temporal Logic Using LLMs with Diverse External Knowledge},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/6DHBEE23}},
  note         = {Machine review of arXiv:2505.20658}
}

read the original abstract

Temporal Logic (TL), especially Signal Temporal Logic (STL), enables precise formal specification, making it widely used in cyber-physical systems such as autonomous driving and robotics. Automatically transforming NL into STL is an attractive approach to overcome the limitations of manual transformation, which is time-consuming and error-prone. However, due to the lack of datasets, automatic transformation currently faces significant challenges and has not been fully explored. In this paper, we propose an NL-STL dataset named STL-Diversity-Enhanced (STL-DivEn), which comprises 16,000 samples enriched with diverse patterns. To develop the dataset, we first manually create a small-scale seed set of NL-STL pairs. Next, representative examples are identified through clustering and used to guide large language models (LLMs) in generating additional NL-STL pairs. Finally, diversity and accuracy are ensured through rigorous rule-based filters and human validation. Furthermore, we introduce the Knowledge-Guided STL Transformation (KGST) framework, a novel approach for transforming natural language into STL, involving a generate-then-refine process based on external knowledge. Statistical analysis shows that the STL-DivEn dataset exhibits more diversity than the existing NL-STL dataset. Moreover, both metric-based and human evaluations indicate that our KGST approach outperforms baseline models in transformation accuracy on STL-DivEn and DeepSTL datasets.

Figures

Figures reproduced from arXiv: 2505.20658 by the authors.

**Figure 2.** Architecture of Knowledge Guide STL Trans [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗

**Figure 3.** Tracking errors before and after refinement. [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗

Figures from the paper (7 more)

**Figure 4.** Figure 4: Impact of iteration rounds on refinement. [PITH_FULL_IMAGE:figures/full_fig_p008_4.png]

**Figure 5.** Figure 5: Scaling effect of STL-DivEn dataset on STL [PITH_FULL_IMAGE:figures/full_fig_p008_5.png]

**Figure 9.** Figure 9: The prompts in the feedback part of Self [PITH_FULL_IMAGE:figures/full_fig_p012_9.png]

**Figure 6.** Figure 6: Evolution Prompts for GPT-4 in NL-STL Pairs [PITH_FULL_IMAGE:figures/full_fig_p012_6.png]

**Figure 7.** Figure 7: The prompt for Baseline Models to generate [PITH_FULL_IMAGE:figures/full_fig_p012_7.png]

**Figure 8.** Figure 8: The prompts in the refinement part of KGST. [PITH_FULL_IMAGE:figures/full_fig_p012_8.png]

**Figure 12.** Figure 12: Scaling effect of STL-DivEn on three evalu [PITH_FULL_IMAGE:figures/full_fig_p013_12.png]

Discussion (0). Sign in to comment.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

STeP: Signal Temporal Logic for Precise Specifications for Action Generation with Vision Language Models
cs.RO 2026-07 conditional novelty 6.0 of 10

A hierarchical planner where a vision-language model decomposes instructions into subtasks, compiles them into Signal Temporal Logic specifications, and uses those specifications to select, monitor, and repair low-lev...
BT-TL-DMPs: A Novel Robot TAMP Framework Combining Behavior Tree, Temporal Logic and Dynamical Movement Primitives
cs.RO 2025-07 reject novelty 4.0 of 10

A hierarchical robot planning framework that generates behavior trees from temporal logic specifications and optimizes dynamic movement primitives to satisfy spatiotemporal constraints while preserving demonstrated mo...

Reference graph

Works this paper leans on

42 extracted references · 24 canonical work pages · cited by 2 Pith papers

[1]

Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. 2023. Gpt-4 technical report. arXiv preprint arXiv:2303.08774

arXiv 2023
[2]

Chaima Boufaied, Maris Jukss, Domenico Bianculli, Lionel Claude Briand, and Yago Isasi Parache. 2021. Signal-based properties of cyber-physical systems: Taxonomy and logic-based characterization. J. Syst. Softw., 174:110881

work page 2021
[3]

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

work page 2023
[4]

Mike Conover, Matt Hayes, Ankit Mathur, Xiangrui Meng, Jianwei Xie, Jun Wan, Ali Ghodsi, Patrick Wendell, and Matei Zaharia. 2023. Hello dolly: Democratizing the magic of chatgpt with open models. Databricks blog. March, 24

work page 2023
[5]

Matthias Cosler, Christopher Hahn, Daniel Mendoza, Frederik Schmitt, and Caroline Trippel. 2023. nl2spec: Interactively translating unstructured natural language to temporal logics with large language models. In CAV 2023 , volume 13965 of LNCS, pages 383--396. Springer

work page 2023
[6]

Matthew B Dwyer, George S Avrunin, and James C Corbett. 1999. Patterns in property specifications for finite-state verification. In ICSE 1999, pages 411--420

work page 1999
[7]

Gidon Ernst, Paolo Arcaini, Ismail Bennani, Aniruddh Chandratre, Alexandre Donz \'e , Georgios Fainekos, Goran Frehse, Khouloud Gaaloul, Jun Inoue, Tanmay Khandait, Logan Mathesen, Claudio Menghi, Giulia Pedrielli, Marc Pouzet, Masaki Waga, Shakiba Yaghoubi, Yoriyuki Yamagata, and Zhenya Zhang. 2021. https://doi.org/10.29007/xwl1 ARCH-COMP 2021 category r...

doi:10.29007/xwl1 2021
[8]

Gidon Ernst, Paolo Arcaini, Ismail Bennani, Alexandre Donz \'e , Georgios Fainekos, Goran Frehse, Logan Mathesen, Claudio Menghi, Giulia Pedrielli, Marc Pouzet, Shakiba Yaghoubi, Yoriyuki Yamagata, and Zhenya Zhang. 2020. ARCH-COMP 2020 category report: Falsification. In 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (...

work page 2020

Show all 42 references

[9]

Gidon Ernst, Paolo Arcaini, Georgios Fainekos, Federico Formica, Jun Inoue, Tanmay Khandait, Mohammad Mahdi Mahboob, Claudio Menghi, Giulia Pedrielli, Masaki Waga, Yoriyuki Yamagata, and Zhenya Zhang. 2022. https://doi.org/10.29007/fhnk ARCH-COMP 2022 category report: Falsific...

2022 doi
[10]

Shalini Ghosh, Daniel Elenius, Wenchao Li, Patrick Lincoln, Natarajan Shankar, and Wilfried Steiner. 2016. Arsenal: automatic requirements specification extraction from natural language. In NFM 2016, pages 41--46. Springer

2016
[11]

John A Hartigan, Manchek A Wong, et al. 1979. A k-means clustering algorithm. Applied statistics, 28(1):100--108

1979
[12]

Jie He, Ezio Bartocci, Dejan Nickovic, Haris Isakovic, and Radu Grosu. 2022. Deepstl - from english requirements to signal temporal logic. In ICSE 2022 , pages 610--622. ACM

2022
[13]

Diederik P Kingma. 2014. Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980

2014 arXiv
[14]

Abdullatif K \"o ksal, Timo Schick, Anna Korhonen, and Hinrich Schuetze. 2024. Longform: Effective instruction tuning with reverse instructions. In ICLR 2024 Workshop on Navigating and Addressing Data Problems for Foundation Models

2024
[15]

o pf, Yannic Kilcher, Dimitri von R \

Andreas K \"o pf, Yannic Kilcher, Dimitri von R \"u tte, Sotiris Anagnostidis, Zhi Rui Tam, Keith Stevens, Abdullah Barhoum, Duc Nguyen, Oliver Stanley, Rich \'a rd Nagyfi, et al. 2024. Openassistant conversations-democratizing large language model alignment. Advances in Neura...

2024
[16]

Dhanashree Kulkarni, Andrew N Fisher, and Chris J Myers. 2013. A new assertion property language for analog/mixed-signal circuits. In Proceedings of the 2013 Forum on specification and Design Languages (FDL), pages 1--8. IEEE

2013
[17]

Marcus, and Hadas Kress - Gazit

Constantine Lignos, Vasumathi Raman, Cameron Finucane, Mitchell P. Marcus, and Hadas Kress - Gazit. 2015. Provably correct reactive control from natural language. Auton. Robots, 38(1):89--105

2015
[18]

Chin-Yew Lin. 2004. Rouge: A package for automatic evaluation of summaries. In Text summarization branches out, pages 74--81

2004
[19]

Aixin Liu, Bei Feng, Bing Xue, Bingxuan Wang, Bochao Wu, Chengda Lu, Chenggang Zhao, Chengqi Deng, Chenyu Zhang, Chong Ruan, et al. 2024. Deepseek-v3 technical report. arXiv preprint arXiv:2412.19437

2024 arXiv
[20]

Aman Madaan, Niket Tandon, Prakhar Gupta, Skyler Hallinan, Luyu Gao, Sarah Wiegreffe, Uri Alon, Nouha Dziri, Shrimai Prabhumoye, Yiming Yang, et al. 2024. Self-refine: Iterative refinement with self-feedback. Advances in Neural Information Processing Systems, 36

2024
[21]

DeLateur, Ron Weiss, Douglas Densmore, and Calin Belta

Curtis Madsen, Prashant Vaidyanathan, Sadra Sadraddini, Cristian Ioan Vasile, Nicholas A. DeLateur, Ron Weiss, Douglas Densmore, and Calin Belta. 2018. Metrics for signal temporal logic formulae. In 57th IEEE Conference on Decision and Control, CDC 2018, Miami, FL, USA, Decemb...

2018
[22]

Sebastian Maierhofer, Anna-Katharina Rettinger, Eva Charlotte Mayer, and Matthias Althoff. 2020. Formalization of interstate traffic rules in temporal logic. In 2020 IEEE Intelligent Vehicles Symposium (IV), pages 752--759. IEEE

2020
[23]

Oded Maler and Dejan Ni c kovi \'c . 2004. https://doi.org/10.1007/978-3-540-30206-3\_12 Monitoring temporal properties of continuous signals . In FORMATS/FTRTFT 2004 , volume 3253 of LNCS, pages 152--166. Springer

2004 doi
[24]

Yuchen Mao, Tianci Zhang, Xu Cao, Zhongyao Chen, Xinkai Liang, Bochen Xu, and Hao Fang. 2024. Nl2stl: Transformation from logic natural language to signal temporal logics using llama2. In 2024 IEEE International Conference on Cybernetics and Intelligent Systems (CIS) and IEEE ...

2024
[25]

Sara Mohammadinejad, Sheryl Paul, Yuan Xia, Vidisha Kudalkar, Jesse Thomason, and Jyotirmoy V Deshmukh. 2024. Systematic translation from natural language robot task descriptions to stl. In International Conference on Bridging the Gap between AI and Reality, pages 259--276. Springer

2024
[26]

Kishore Papineni, Salim Roukos, Todd Ward, and Wei-Jing Zhu. 2002. Bleu: a method for automatic evaluation of machine translation. In ACL 2002, pages 311--318

2002
[27]

Amir Pnueli. 1977. https://doi.org/10.1109/SFCS.1977.32 The temporal logic of programs . In FOCS 1977 , pages 46--57. IEEE

1977 doi
[28]

Nils Reimers and Iryna Gurevych. 2019. https://arxiv.org/abs/1908.10084 Sentence-bert: Sentence embeddings using siamese bert-networks . In Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing. Association for Computational Linguistics

2019 arXiv
[29]

Tain \ a Santos, Gustavo Carvalho, and Augusto Sampaio. 2018. Formal modelling of environment restrictions from natural-language requirements. In SBMF 2018, pages 252--270. Springer

2018
[30]

Aarohi Srivastava, Abhinav Rastogi, Abhishek Rao, Abu Awal Md Shoeb, Abubakar Abid, Adam Fisch, Adam R Brown, Adam Santoro, Aditya Gupta, Adri \`a Garriga-Alonso, et al. 2023. Beyond the imitation game: Quantifying and extrapolating the capabilities of language models. Transac...

2023
[31]

Zhiqing Sun, Yikang Shen, Qinhong Zhou, Hongxin Zhang, Zhenfang Chen, David Cox, Yiming Yang, and Chuang Gan. 2024. Principle-driven self-alignment of language models from scratch with minimal human supervision. Advances in Neural Information Processing Systems, 36

2024
[32]

Rohan Taori, Ishaan Gulrajani, Tianyi Zhang, Yann Dubois, Xuechen Li, Carlos Guestrin, Percy Liang, and Tatsunori B Hashimoto. 2023. Stanford alpaca: An instruction-following llama model

2023
[33]

Stefanie Tellex, Nakul Gopalan, Hadas Kress-Gazit, and Cynthia Matuszek. 2020. Robots that use language. Annual Review of Control, Robotics, and Autonomous Systems, 3(1):25--55

2020
[34]

Yizhong Wang, Yeganeh Kordi, Swaroop Mishra, Alisa Liu, Noah A Smith, Daniel Khashabi, and Hannaneh Hajishirzi. 2023. Self-instruct: Aligning language models with self-generated instructions. In ACL 2023

2023
[35]

Zifeng Wang, Chun-Liang Li, Vincent Perot, Long Le, Jin Miao, Zizhao Zhang, Chen-Yu Lee, and Tomas Pfister. 2024. Codeclm: Aligning language models with tailored synthetic data. In Findings of the Association for Computational Linguistics: NAACL 2024, pages 3712--3729

2024
[36]

Can Xu, Qingfeng Sun, Kai Zheng, Xiubo Geng, Pu Zhao, Jiazhan Feng, Chongyang Tao, and Daxin Jiang. 2023. Wizardlm: Empowering large language models to follow complex instructions. arXiv preprint arXiv:2304.12244

2023 arXiv
[37]

Wenting Zhao, Xiang Ren, Jack Hessel, Claire Cardie, Yejin Choi, and Yuntian Deng. 2024. Wildchat: 1m chatgpt interaction logs in the wild. In ICLR 2024

2024
[38]

Lianmin Zheng, Wei-Lin Chiang, Ying Sheng, Tianle Li, Siyuan Zhuang, Zhanghao Wu, Yonghao Zhuang, Zhuohan Li, Zi Lin, Eric Xing, et al. 2023. Lmsys-chat-1m: A large-scale real-world llm conversation dataset. In ICLR 2023

2023
[39]

Chunting Zhou, Pengfei Liu, Puxin Xu, Srinivasan Iyer, Jiao Sun, Yuning Mao, Xuezhe Ma, Avia Efrat, Ping Yu, Lili Yu, et al. 2024. Lima: Less is more for alignment. Advances in Neural Information Processing Systems, 36

2024
[40]

Luk \'a s Z ilka. 2010. Temporal logic for man. Ph.D. thesis, Master’s thesis, Brno University of Technology

2010
[41]

online" 'onlinestring :=

ENTRY address archivePrefix author booktitle chapter edition editor eid eprint eprinttype howpublished institution journal key month note number organization pages publisher school series title type volume year doi pubmed url lastchecked label extra.label sort.label short.list...
[42]

write newline

" write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 gl...

Pith tools

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

[1] [1]

Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. 2023. Gpt-4 technical report. arXiv preprint arXiv:2303.08774

arXiv 2023

[2] [2]

Chaima Boufaied, Maris Jukss, Domenico Bianculli, Lionel Claude Briand, and Yago Isasi Parache. 2021. Signal-based properties of cyber-physical systems: Taxonomy and logic-based characterization. J. Syst. Softw., 174:110881

work page 2021

[3] [3]

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

work page 2023

[4] [4]

Mike Conover, Matt Hayes, Ankit Mathur, Xiangrui Meng, Jianwei Xie, Jun Wan, Ali Ghodsi, Patrick Wendell, and Matei Zaharia. 2023. Hello dolly: Democratizing the magic of chatgpt with open models. Databricks blog. March, 24

work page 2023

[5] [5]

Matthias Cosler, Christopher Hahn, Daniel Mendoza, Frederik Schmitt, and Caroline Trippel. 2023. nl2spec: Interactively translating unstructured natural language to temporal logics with large language models. In CAV 2023 , volume 13965 of LNCS, pages 383--396. Springer

work page 2023

[6] [6]

Matthew B Dwyer, George S Avrunin, and James C Corbett. 1999. Patterns in property specifications for finite-state verification. In ICSE 1999, pages 411--420

work page 1999

[7] [7]

Gidon Ernst, Paolo Arcaini, Ismail Bennani, Aniruddh Chandratre, Alexandre Donz \'e , Georgios Fainekos, Goran Frehse, Khouloud Gaaloul, Jun Inoue, Tanmay Khandait, Logan Mathesen, Claudio Menghi, Giulia Pedrielli, Marc Pouzet, Masaki Waga, Shakiba Yaghoubi, Yoriyuki Yamagata, and Zhenya Zhang. 2021. https://doi.org/10.29007/xwl1 ARCH-COMP 2021 category r...

doi:10.29007/xwl1 2021

[8] [8]

Gidon Ernst, Paolo Arcaini, Ismail Bennani, Alexandre Donz \'e , Georgios Fainekos, Goran Frehse, Logan Mathesen, Claudio Menghi, Giulia Pedrielli, Marc Pouzet, Shakiba Yaghoubi, Yoriyuki Yamagata, and Zhenya Zhang. 2020. ARCH-COMP 2020 category report: Falsification. In 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (...

work page 2020