SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning

• URL: http://arxiv.org/abs/2501.17496v1
• Date: Wed, 29 Jan 2025 09:06:19 GMT
• Title: SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning
• Authors: Jan Kretinsky, Tobias Meggendorfer, Maximilian Prokop, Ashkan Zarkhah,
• Abstract summary: SemML won this year's realizability tracks of SYNTCOMP. We present our tool SemML, which won this year's realizability tracks of SYNTCOMP.
• Score: 3.468621550644668
• License:
• 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. 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.

Related papers

• Matchmaker: Self-Improving Large Language Model Programs for Schema Matching [60.23571456538149]
  We propose a compositional language model program for schema matching, comprised of candidate generation, refinement and confidence scoring. Matchmaker self-improves in a zero-shot manner without the need for labeled demonstrations. Empirically, we demonstrate on real-world medical schema matching benchmarks that Matchmaker outperforms previous ML-based approaches.
  arXiv  Detail & Related papers  (2024-10-31T16:34:03Z)
• LLM-based Optimization of Compound AI Systems: A Survey [64.39860384538338]
  In a compound AI system, components such as an LLM call, a retriever, a code interpreter, or tools are interconnected. Recent advancements enable end-to-end optimization of these parameters using an LLM. This paper presents a survey of the principles and emerging trends in LLM-based optimization of compound AI systems.
  arXiv  Detail & Related papers  (2024-10-21T18:06:25Z)
• Genetic Instruct: Scaling up Synthetic Generation of Coding Instructions for Large Language Models [54.51932175059004]
  We introduce a scalable method for generating synthetic instructions to enhance the code generation capability of Large Language Models. The proposed algorithm, Genetic-Instruct, mimics evolutionary processes, utilizing self-instruction to create numerous synthetic samples from a limited number of seeds.
  arXiv  Detail & Related papers  (2024-07-29T20:42:59Z)
• SynthesizRR: Generating Diverse Datasets with Retrieval Augmentation [55.2480439325792]
  We study the synthesis of six datasets, covering topic classification, sentiment analysis, tone detection, and humor. We find that SynthesizRR greatly improves lexical and semantic diversity, similarity to human-written text, and distillation performance.
  arXiv  Detail & Related papers  (2024-05-16T12:22:41Z)
• CodecLM: Aligning Language Models with Tailored Synthetic Data [51.59223474427153]
  We introduce CodecLM, a framework for adaptively generating high-quality synthetic data for instruction-following abilities. We first encode seed instructions into metadata, which are concise keywords generated on-the-fly to capture the target instruction distribution. We also introduce Self-Rubrics and Contrastive Filtering during decoding to tailor data-efficient samples.
  arXiv  Detail & Related papers  (2024-04-08T21:15:36Z)
• Guiding Enumerative Program Synthesis with Large Language Models [15.500250058226474]
  In this paper, we evaluate the abilities of Large Language Models to solve formal synthesis benchmarks. When one-shot synthesis fails, we propose a novel enumerative synthesis algorithm. We find that GPT-3.5 as a stand-alone tool for formal synthesis is easily outperformed by state-of-the-art formal synthesis algorithms.
  arXiv  Detail & Related papers  (2024-03-06T19:13:53Z)
• ALMOST: Adversarial Learning to Mitigate Oracle-less ML Attacks via Synthesis Tuning [18.758747687330384]
  Oracle-less machine learning (ML) attacks have broken various logic locking schemes. We propose ALMOST, a framework for adversarial learning to mitigate oracle-less ML attacks via synthesis tuning.
  arXiv  Detail & Related papers  (2023-03-06T18:55:58Z)
• 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)
• Towards Neural-Guided Program Synthesis for Linear Temporal Logic Specifications [26.547133495699093]
  We use a neural network to learn a Q-function that is then used to guide search, and to construct programs that are subsequently verified for correctness. Our method is unique in combining search with deep learning to realize synthesis.
  arXiv  Detail & Related papers  (2019-12-31T17:09:49Z)

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.