Class-Conditional Conformal Prediction for Signal Temporal Logic Inference with Many Classes
Authors: Yixuan Wang, Danyang Li, Matthew Cleaveland, Roberto Tron, Mingyu Cai
Organizations: Mechanical Engineering, University of California, Riverside, CA 92521, USA · Mechanical Engineering, Boston University · MIT Lincoln Laboratory, Lexington, MA 02421, USA
Signal Temporal Logic (STL) inference provides interpretable formulas for time series classification. For multiclass classification, however, accurate predictions do not necessarily ensure that the inferred formulas are satisfied consistently with the true class. We introduce the positive satisfaction rate and codeword satisfaction rate to quantify satisfaction of required formulas and consistency with the complete class codeword, respectively. We develop a two-stage procedure that first learns discriminative formulas using a margin-based objective and then refines predicate thresholds toward a small positive robustness target while fixing the formula structure and temporal intervals. Satisfaction and ranking penalties discourage violations of required formulas and loss of class separation. The decoding loss is used as a nonconformity score and calibrated separately for each class, providing finite-sample class-conditional coverage under intra-class exchangeability. Experiments on naval, synthetic, and robot manipulation trajectories demonstrate discrepancies between classification accuracy and formula satisfaction. The results further reveal a data-dependent tradeoff between robustness tightness and satisfaction, while class-conditional calibration mitigates undercoverage that can be hidden by pooled calibration.
Figures & tables
Fig. 1 : Overview of the proposed framework combining discriminative STL learning, tightness refinement, and class conditional conformal prediction.
Fig. 2 : Conformal prediction with the refined models, standard against class conditional calibration. Rows: naval, synthetic, and CALVIN datasets. Columns: classwise coverage at α=0.10 , coverage gap, and inefficiency across miscoverage levels. Coverage gap is the average absolute difference between the classwise coverage and 1−α , and inefficiency is the average prediction set size.
Dataset
Model
Acc val
Acc test
PSR test
CSR test
Rˉpos
Naval
Discriminative
0.977
0.980
0.924
0.872
0.24
Refined
0.960
0.960
0.873
0.797
0.13
w/o margin
0.997
1.000
0.984
0.885
0.26
Synthetic
Discriminative
0.997
0.996
0.966
0.722
0.34
Refined
0.995
0.995
0.944
0.695
0.33
w/o margin
1.000
0.998
0.998
0.565
0.36
TABLE I : Accuracy, satisfaction rates, and mean positive robustness Rˉpos on the test split. Refinement reduces Rˉpos toward zero. The w/o margin rows remove the margin term of Eq. ( 9 ), reducing the codewise losses to sign losses.
Fig. 3 : Trajectory examples in the naval surveillance scenario. Vessels of class 0 arrive at the harbor without approaching the island, vessels of class 1 pass the island region on the way to the harbor, and vessels of class 2 turn back to the open sea. The formulas of Table II correspond to the regions and time windows that separate the three behaviors.
Class
Formula
0
F[29,31](x<38.7)∧F[1,2](y<44.3)
∧F[1,2](y>34.7)∧F[9,26](y>29.2)
1
G[5,6](x<55.1)∧G[43,45](y>26.6)
2
G[41,48](y<38.8)∧G[41,56](x>37.1)
TABLE II : Learned STL formulas on the naval dataset after refinement, in the original coordinate frame. Vacuous and redundant atoms are pruned using the training and validation splits, on which the pruned formulas agree with the full model by construction; on the test split they agree on all but one sample.
Fig. 4 : Trajectory examples in Synthetic Dataset.
Class
Formula
0
F[33,35](y<−2.0)∧G[13,63](x<3.1)
1
G[17,19](x>3.5)
2
F[69,70](y<−1.1)
3
F[25,26](−3.6<x<2.6)∧G[75,76](x>0.9)
4
F[32,36](x<1.6)∧G[62,63](y<0.1)
5
F[22,26](x>−4.1)∧G[38,39](x<0.0)
TABLE III : Learned STL formulas on the synthetic dataset after refinement, in the generator coordinate frame. Same pruning convention as Table II .
Fig. 5 : One trajectory per task of CALVIN Dataset.
Class
Formula
0
F[62,63](y<−35.1)
1
G[31,36](y<−34.0)
2
F[38,42](x>−11.3∧y>−2.6∧g>1.9)
∧F[20,27](g>4.7)∧G[7,51](x<23.6∧y<3.5)
3
F[60,63](x>−16.9)∧G[33,39](x<−5.0∧y>−6.1)
∧G[5,38](g>−0.1)
TABLE IV : Learned STL formulas on the CALVIN dataset after refinement. Same pruning convention as Table II . Here x , y , z are the end effector position and g the gripper width, in centimeters.
Dataset
Acc network
Acc exact
Sign disagreement
Naval
0.960
0.980
0/753
Synthetic
0.995
0.964
0/15337
CALVIN
0.895
0.871
0/5472
TABLE V : Network and exact STL semantics on the test split for the selected refined models. Robustness signs agree on every code entry, so PSR and CSR coincide under both semantics; accuracies differ because decoding compares loss magnitudes.
Configuration
ηtight
ηsign
γ
Acc
PSR
CSR
Rˉpos
Baseline
1.0
5
0.01
0.976
0.757
0.729
0.105
ηtight×0.5
0.5
5
0.01
0.976
0.705
0.661
0.097
ηsign×2
1.0
10
0.01
0.960
0.853
0.793
0.124
ηsign×4
1.0
20
0.01
0.960
0.873
0.797
0.128
γ×2
1.0
5
0.02
0.976
0.809
0.777
0.116
TABLE VI : Stage 2 sweep on the naval dataset, all metrics on the test split. The baseline row is the configuration used on the synthetic and CALVIN datasets, and the ηsign×4 row is the reported operating point.
Signal Temporal Logic (STL) inference learns interpretable logical rules for temporal behaviors in dynamical systems. To ensure the correctness of learned STL formulas, recent approaches have incorporated conformal prediction as a statistical tool for uncertainty quantification. However, most existing methods rely on the assumption that calibration and testing data are identically distributed and exchangeable, an assumption that is frequently violated in real-world settings. This paper proposes a conformalized STL inference framework that explicitly addresses covariate shift between training and deployment trajectories dataset. From a technical standpoint, the approach first employs a template-free, differentiable STL inference method to learn an initial model, and subsequently refines it using a limited deployment side dataset to promote distribution alignment. To provide validity guarantees under distribution shift, the framework estimates the likelihood ratio between training and deployment distributions and integrates it into an STL-robustness-based weighted conformal prediction scheme. Experimental results on trajectory datasets demonstrate that the proposed framework preserves the interpretability of STL formulas while significantly improving symbolic learning reliability at deployment time.
Yixuan Wang, Danyang Li, Matthew Cleaveland +2
Mingyu Cai and Yixuan Wang are with Mechanical Engineering, University of California, Riverside, CA, 92521, USA. · Danyang Li and Roberto Tron are with Mechanical Engineering, Boston University. · Matthew Cleaveland is with MIT Lincoln Laboratory, Lexington, MA, 02421, USA
We introduce a framework for learning continuous neural representations of formal specifications by distilling the geometry of their semantics into a latent space. Existing approaches rely either on symbolic kernels -- which preserve behavioural semantics but are computationally prohibitive, anchor-dependent, and non-invertible -- or on syntax-based neural embeddings that fail to capture underlying structures. Our method bridges this gap: using a teacher-student setup, we distill a symbolic robustness kernel into a Transformer encoder. Unlike standard contrastive methods, we supervise the model with a continuous, kernel-weighted geometric alignment objective that penalizes errors in proportion to their semantic discrepancies. Once trained, the encoder produces embeddings in a single forward pass, effectively mimicking the kernel's logic at a fraction of its computational cost. We apply our framework to Signal Temporal Logic (STL), demonstrating that the resulting neural representations faithfully preserve the semantic similarity of STL formulae, accurately predict robustness and constraint satisfaction, and remain intrinsically invertible. Our proposed approach enables highly efficient, scalable neuro-symbolic reasoning and formula reconstruction without repeated kernel computation at runtime.
Sara Candussio, Gabriele Sarti, Gaia Saveri +1
AILab, MIGe, University of Trieste, IT · Khoury College of Computing Sciences, Northeastern University, Boston, MA, USA
Signal Temporal Logic (STL) is an expressive formal language for specifying spatio-temporal requirements over real-valued, real-time signals. It has been widely used for the verification and synthesis of autonomous systems and cyber-physical systems. In practice, however, users often express their requirements in natural language rather than in structured STL formulas, making natural-language-to-STL translation a critical yet challenging task. Manual specification requires temporal-logic expertise and cannot scale, while prompting commercial LLM APIs incurs substantial token costs and may expose sensitive system requirements to third-party services, raising privacy concerns for industrial deployment. To address these challenges, we present ReasonSTL, a tool-augmented framework that adapts local open-source language models for natural-language-to-STL generation. ReasonSTL decomposes the translation process into explicit reasoning, deterministic tool calls, and structured formula construction. We further introduce process-rewarded training to supervise both tool-use trajectories and final formulas, together with STL-Bench, a bilingual, computation-aware benchmark grounded in real-world signals. Experiments show that a 4B model trained with ReasonSTL achieves state-of-the-art performance in both automatic metrics and human evaluations, demonstrating that ReasonSTL provides a transparent, low-cost, and privacy-preserving alternative for formal specification drafting.
Bowen Ye, Zhijian Li, Junyue Huang +2
Shanghai Jiao Tong University · Alibaba Group, Hangzhou, China