SemML 2.0: Synthesizing Controllers for LTL

• URL: http://arxiv.org/abs/2604.24102v1
• Date: Mon, 27 Apr 2026 06:50:14 GMT
• Title: SemML 2.0: Synthesizing Controllers for LTL
• Abstract summary: We present the second version of SemML, which outperforms all state-of-the-art tools for finding either solution.<n>We evaluate our tool against the existing state-of-the-art tools (in particular Strix, LtlSynt, and the previous version of SemML) on the dataset of the synthesis competition SYNTCOMP.
• Score: 4.1483423188102755
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Synthesizing a reactive system from specifications given in linear temporal logic (LTL) is a classical problem, finding its applications in safety-critical systems design. These systems are typically represented using either Mealy machines or AIGER circuits. We present the second version of SemML, which outperforms all state-of-the-art tools for finding either solution. Aside from implementing the classical automata-theoretic approach, our tool utilizes partial exploration and machine-learning guidance for obtaining solutions efficiently, and numerous heuristics and improvements of classic algorithms for extracting small representations of these solutions. We evaluate our tool against the existing state-of-the-art tools (in particular Strix, LtlSynt, and the previous version of SemML) on the dataset of the synthesis competition SYNTCOMP. We show that we solve significantly more instances and do so much faster than other tools, while maintaining state-of-the-art solution quality.

Related papers

• SynAct: A Reasoning-Acting Large Language Model Agent for Adaptive Synthesis Optimization [32.192326654149966]
  We present SynAct, an adaptive closed-loop LLM reasoning--acting agent that iteratively diagnoses live synthesis reports and reasons over the current circuit state.<n>Experiments on a commercial synthesis tool across 14 designs show that SynAct reduces average WNS to 27% of that from synthesis.
  arXiv  Detail & Related papers  (2026-08-13T03:02:25Z)
• SOCRATES: Simulation Optimization with Correlated Replicas and Adaptive Trajectory Evaluations [25.18297372152296]
  SOCRATES is a novel two-stage procedure that automates the design of tailored SO algorithms.<n>An ensemble of digital replicas of the real system is used as a testbed to evaluate a set of baseline SO algorithms.<n>An LLM acts as a meta-optimizer, analyzing the performance trajectories of these algorithms to iteratively revise and compose a final, hybrid optimization schedule.
  arXiv  Detail & Related papers  (2025-11-01T19:57:38Z)
• VerlTool: Towards Holistic Agentic Reinforcement Learning with Tool Use [78.29315418819074]
  We introduce VerlTool, a unified and modular framework that addresses limitations through systematic design principles.<n>Our framework formalizes ARLT as multi-turn trajectories with multi-modal observation tokens (text/image/video), extending beyond single-turn RLVR paradigms.<n>The modular plugin architecture enables rapid tool integration requiring only lightweight Python definitions.
  arXiv  Detail & Related papers  (2025-09-01T01:45:18Z)
• Tool-Star: Empowering LLM-Brained Multi-Tool Reasoner via Reinforcement Learning [63.31585771716123]
  Large language models (LLMs) have shown remarkable reasoning capabilities via large-scale reinforcement learning (RL)<n>We introduce Tool-Star, an RL-based framework designed to empower LLMs to autonomously invoke multiple external tools during stepwise reasoning.<n>Tool-Star integrates six types of tools and incorporates systematic designs in both data synthesis and training.
  arXiv  Detail & Related papers  (2025-05-22T09:00:19Z)
• SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning [3.468621550644668]
  SemML won this year's realizability tracks of SYNTCOMP.<n>We present our tool SemML, which won this year's realizability tracks of SYNTCOMP.
  arXiv  Detail & Related papers  (2025-01-29T09:06:19Z)
• Scaffolded Language Models with Language Supervision for Mixed-Autonomy: A Survey [52.00674453604779]
  This survey organizes the literature on the design and optimization of emerging structures around post-trained LMs.<n>We refer to this overarching structure as scaffolded LMs and focus on LMs that are integrated into multi-step processes with tools.
  arXiv  Detail & Related papers  (2024-10-21T18:06:25Z)
• Planning, Creation, Usage: Benchmarking LLMs for Comprehensive Tool Utilization in Real-World Complex Scenarios [93.68764280953624]
  UltraTool is a novel benchmark designed to improve and evaluate Large Language Models' ability in tool utilization. It emphasizes real-world complexities, demanding accurate, multi-step planning for effective problem-solving. A key feature of UltraTool is its independent evaluation of planning with natural language, which happens before tool usage.
  arXiv  Detail & Related papers  (2024-01-30T16:52:56Z)
• Machine Learning Insides OptVerse AI Solver: Design Principles and Applications [74.67495900436728]
  We present a comprehensive study on the integration of machine learning (ML) techniques into Huawei Cloud's OptVerse AI solver. We showcase our methods for generating complex SAT and MILP instances utilizing generative models that mirror multifaceted structures of real-world problem. We detail the incorporation of state-of-the-art parameter tuning algorithms which markedly elevate solver performance.
  arXiv  Detail & Related papers  (2024-01-11T15:02:15Z)
• INVICTUS: Optimizing Boolean Logic Circuit Synthesis via Synergistic Learning and Search [18.558280701880136]
  State-of-the-art logic synthesis algorithms have a large number of logic minimizations. INVICTUS generates a sequence of logic minimizations based on a training dataset of previously seen designs.
  arXiv  Detail & Related papers  (2023-05-22T15:50:42Z)
• OMLT: Optimization & Machine Learning Toolkit [54.58348769621782]
  The optimization and machine learning toolkit (OMLT) is an open-source software package incorporating neural network and gradient-boosted tree surrogate models. We discuss the advances in optimization technology that made OMLT possible and show how OMLT seamlessly integrates with the algebraic modeling language Pyomo.
  arXiv  Detail & Related papers  (2022-02-04T22:23:45Z)
• LTLf Synthesis on Probabilistic Systems [0.0]
  synthesis is used to find a policy that maximizes the probability of achieving this behavior. No tools exist to solve policy synthesis for behaviors given finite-trace properties. We present two algorithms for solving this problem: the first via reduction of Markov Processes and the second native tools for automatonf.
  arXiv  Detail & Related papers  (2020-09-23T01:26:47Z)
• Revisiting LSTM Networks for Semi-Supervised Text Classification via Mixed Objective Function [106.69643619725652]
  We develop a training strategy that allows even a simple BiLSTM model, when trained with cross-entropy loss, to achieve competitive results. We report state-of-the-art results for text classification task on several benchmark datasets.
  arXiv  Detail & Related papers  (2020-09-08T21:55:22Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.