Research map / Architectures and efficiency / RNNs and normalization
End-to-End Learning of LTLf Formulae by Faithful LTLf Encoding
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes TLTLf, an end-to-end neural method that learns LTLf formulae via a faithful LTLf encoding of a parameterized network, from which the formula is interpreted directly.
Problem
Learning tree-structured LTLf formulae from positive and negative finite traces, including imperfect (mislabeled) data, where the search space is huge and the neural model may not faithfully match the extracted formula.
Approach
Parameterizes a neural network with an LTLf encoding (parameters in [0,1] encoding syntax tree nodes and right-child links) whose faithful subclass has a one-to-one correspondence with prefix-form LTLf formulae, so the learned network is interpreted into a formula with beam-search decoding and regularization enforces faithfulness.
Key results
- TLTLf reaches 98.0% accuracy at kf=3 and 90.4% at kf=15 on successful cases, outperforming GLTLf (94.3% and 83.0%) and BayesLTL.
- On imperfect data, TLTLf averages 88.47% accuracy at a 30% imperfect rate, while MaxSAT-DT and C.&M. fail on all such datasets.
- The interpreted formula agrees with the network on over 95% of test traces, with a smaller network-to-formula performance gap than GLTLf.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use faithful LTLf encoding in place of GLTLf's encoding | TLTLf · LTLf datasets | accuracy: up to 7% | Helped |
| Train on data with imperfect labels at rate δ=0.3 | TLTLf · Imperfect LTLf datasets | accuracy: 88.47% | Hurt |
| Interpret the formula from the trained network using faithful LTLf encoding | TLTLf · Test traces | consistency: over 95% | Helped |
| Increase encoding size L (ablation) | TLTLf · kf=9 | accuracy | Helped |
| Increase beam width ω (ablation) | TLTLf formula interpretation · kf=9 | accuracy | Helped |
Surprising findings
- MaxSAT-DT and C.&M. achieve the highest accuracy on solved cases but run out of time on many larger instances.
Limitations
- Only the fundamental operators (not/and/X/U) are considered; other LTLf operators are not handled.
- Faithfulness of the trained network is approximate because constraints are enforced by regularization rather than exactly.
- Accuracy drops as kf grows and performance is evaluated only on synthetic datasets.
Experimental setup
Datasets: LTLf learning datasets from Luo et al. 2022 (GLTLf)
Benchmarks: Luo et al. 2022 LTLf datasets (kf in 3,6,9,12,15)
Metrics: accuracy F1 number of solved cases consistency
Baselines: C.&M. BayesLTL MaxSAT-DT GLTLf
Builds on: GLTLf BayesLTL MaxSAT-DT
Closest papers by meaning
- Neuro-Symbolic Temporal Point Processes (ICML 2024 · similarity 0.86)
- Efficient Test-Time Scaling via Hierarchical Search and Self-Verification for Discrete Diffusion Language Models (ICML 2026 · similarity 0.86)
- Entropy-Gated Latent Recursion (NeurIPS 2026 · similarity 0.85)
- DeepLTL: Learning to Efficiently Satisfy Complex LTL Specifications for Multi-Task RL (ICLR 2025 · similarity 0.85)
- xLSTM 7B: A Recurrent LLM for Fast and Efficient Inference (ICML 2025 · similarity 0.84)
- Zero-Shot Instruction Following in RL via Structured LTL Representations (NeurIPS 2026 · similarity 0.84)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.