# SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning

arXiv: https://arxiv.org/abs/2501.17496 · HTML: https://mlsanity.com/paper/2501.17496/

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 11 of its 44 references that are in the map.
- First posted on arXiv 29 Jan 2025.

## Builds on (most cited first, 11 of 11)

- [Neural Circuit Synthesis from Specification Patterns](https://mlsanity.com/paper/2107.11864/) (2021)
- [Iterative Circuit Repair Against Formal Specifications](https://mlsanity.com/paper/2303.01158/) (2023)
- [Boolean Abstractions for Realizability Modulo Theories (Extended version)](https://mlsanity.com/paper/2310.17292/) (2023)
- [BoSy: An Experimentation Framework for Bounded Synthesis](https://mlsanity.com/paper/1803.09566/) (2018)
- [The Reactive Synthesis Competition (SYNTCOMP): 2018-2021](https://mlsanity.com/paper/2206.00251/) (2022)
- [Semantic Labelling and Learning for Parity Game Solving in LTL Synthesis](https://mlsanity.com/paper/1907.12157/) (2019)
- [A High-Level LTL Synthesis Format: TLSF v1.1](https://mlsanity.com/paper/1604.02284/) (2016)
- [Guessing Winning Policies in LTL Synthesis by Semantic Learning](https://mlsanity.com/paper/2305.15109/) (2023)
- [Playing Games with your PET: Extending the Partial Exploration Tool to Stochastic Games](https://mlsanity.com/paper/2405.03885/) (2024)
- [NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis](https://mlsanity.com/paper/2401.12131/) (2024)
- [Acacia-Bonsai: A Modern Implementation of Downset-Based LTL Realizability](https://mlsanity.com/paper/2204.06079/) (2022)

## Built on by (most cited first, 6 of 6)

- [Semantically Labelled Automata for Multi-Task Reinforcement Learning with LTL Instructions](https://mlsanity.com/paper/2602.06746/) (2026)
- [SemML 2.0: Synthesizing Controllers for LTL](https://mlsanity.com/paper/2604.24102/) (2026)
- [Learning Representations Through Contrastive Neural Model Checking](https://mlsanity.com/paper/2510.01853/) (2025)
- [Live LTL Progress Tracking: Towards Task-Based Exploration](https://mlsanity.com/paper/2604.17106/) (2026)
- [Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models](https://mlsanity.com/paper/2605.15131/) (2026)
- [Infinite Trace Objectives with Finite Trace Techniques: Translating LTL to LTLf+](https://mlsanity.com/paper/2608.02454/) (2026)

## Abstract (arXiv)

Synthesizing a reactive system from specifications given in linear temporal logic (LTL) is a classical problem, finding its applications in safety-critical systems design. We present our tool SemML, which won this year's LTL realizability tracks of SYNTCOMP, after years of domination by Strix. While both tools are based on the automata-theoretic approach, ours relies heavily on (i) Semantic labelling, additional information of logical nature, coming from recent LTL-to-automata translations and decorating the resulting parity game, and (ii) Machine Learning approaches turning this information into a guidance oracle for on-the-fly exploration of the parity game (whence the name SemML). Our tool fills the missing gaps of previous suggestions to use such an oracle and provides an efficeint implementation with additional algorithmic improvements. We evaluate SemML both on the entire set of SYNTCOMP as well as a synthetic data set, compare it to Strix, and analyze the advantages and limitations. As SemML solves more instances on SYNTCOMP and does so significantly faster on larger instances, this demonstrates for the first time that machine-learning-aided approaches can out-perform state-of-the-art tools in real LTL synthesis.