SearcharxivSearch

arXiv subjects

Sam Nicholas Kouteili

Publications and source records attributed to Sam Nicholas Kouteili.

3 recordsLinked to original sources

Learning GR(1) Specifications from Traces

Constrained specification mining enables the automatic discovery of desired properties from system traces. Generalized Reactivity of Rank 1, or GR(1), is a fragment of LTL with polynomial-time synthesis that natively encodes assume-guarantee properties present in most hardware and robotics domains. In this paper, we present GR1MINE, a SAT-based tool for efficiently learning GR(1) formulas from examples. We exploit the GR(1) temporal skeleton to incrementally enumerate formula candidates, leveraging learnt clauses to avoid recomputation. On the Boolean GR(1) Syntech suite, GR1MINE learns a realizable formula for all 60 benchmarks over 30X faster than generic and constrained LTL mining tools. On non-GR(1) specifications from SYNTCOMP, GR1MINE is still able to recover >2X more realizable specifications than baselines within the timeout.

cs.LO

Warm Starting State-Space Models with Automata Learning

We prove that Moore machines can be exactly realized as state-space models (SSMs), establishing a formal correspondence between symbolic automata and these continuous machine learning architectures. These Moore-SSMs preserve both the complete symbolic structure and input-output behavior of the original Moore machine, but operate in Euclidean space. With this correspondence, we compare the training of SSMs with both passive and active automata learning. In recovering automata from the SYNTCOMP benchmark, we show that SSMs require orders of magnitude more data than symbolic methods and fail to learn state structure. This suggests that symbolic structure provides a strong inductive bias for learning these systems. We leverage this insight to combine the strengths of both automata learning and SSMs in order to learn complex systems efficiently. We learn an adaptive arbitration policy on a suite of arbiters from SYNTCOMP and show that initializing SSMs with symbolically-learned approximations learn both faster and better. We see 2-5 times faster convergence compared to randomly initialized models and better overall model accuracies on test data. Our work lifts automata learning out of purely discrete spaces, enabling principled exploitation of symbolic structure in continuous domains for efficiently learning in complex settings.

cs.LG

Mining Beyond the Bools: Learning Data Transformations and Temporal Specifications

Mining specifications from execution traces presents an automated way of capturing characteristic system behaviors. However, existing approaches are largely restricted to Boolean abstractions of events, limiting their ability to express data-aware properties. In this paper, we extend mining procedures to operate over richer datatypes. We first establish candidate functions in our domain that cover the set of traces by leveraging Syntax Guided Synthesis (SyGuS) techniques. To capture these function applications temporally, we formalize the semantics of TSL$_f$, a finite-prefix interpretation of Temporal Stream Logic (TSL) that extends LTL$_f$ with support for first-order predicates and functional updates. This allows us to unify a corresponding procedure for learning the data transformations and temporal specifications of a system. We demonstrate our approach synthesizing reactive programs from mined specifications on the OpenAI-Gymnasium ToyText environments, finding that our method is more robust and orders of magnitude more sample-efficient than passive learning baselines on generalized problem instances.

cs.LO