saracandu/stlenc

STL Encoder (Neural Backbone)

This repository contains the neural encoder architecture for the STLEnc project. The model is designed to map Signal Temporal Logic (STL) formulae into a 1024-dimensional latent embedding space.

Model Description

This model is a neural approximation of the kernel-based framework introduced by Gallo et al. in "A Kernel-Based Approach to Signal Temporal Logic" (2020).

In the original framework, STL formulae are embedded into a Reproducing Kernel Hilbert Space (RKHS) using a recursive kernel that accounts for the syntax and temporal intervals of the logic. Our approach replaces the traditional kernel-based projection with a Transformer-based encoder.

By using a fixed anchor set of formulae (as suggested in kernel approximation methods), the Transformer is trained to learn a mapping that mimics the kernel's distance properties. This allows for:

• Scalability: Faster computation compared to recursive kernel evaluations.

• Continuity: A smooth latent space suitable for optimization and deep learning tasks.

• Architecture: Custom Transformer Encoder (12 layers, 16 attention heads).

• Tokenizer: Custom longest-match tokenizer optimized for STL symbols, temporal intervals, and numeric predicates.

• Output: 1024-dimensional embeddings via [CLS] token pooling.

Training Data

The model is designed to be trained on the saracandu/stl_formulae dataset, which contains a large-scale collection of STL expressions and their corresponding kernel-derived embeddings.

Usage

from transformers import AutoModel, AutoTokenizer
import torch

repo_id = "saracandu/stlenc"

# Load Tokenizer & Model
tokenizer = AutoTokenizer.from_pretrained(repo_id, trust_remote_code=True)
model = AutoModel.from_pretrained(repo_id, trust_remote_code=True)

# Example: Encode an STL formula
formula = "always[0, 10] (x > 0) and eventually[5, 20] (y < -1)"
inputs = tokenizer(formula, return_tensors="pt")

with torch.no_grad():
    embedding = model(**inputs)

print(embedding.shape)  # [1, 1024]