SMT-Based Active Learning of Weighted Automata

TL;DR

This paper introduces an SMT-based active learning algorithm for weighted automata that guarantees minimality, outperforms naive baselines, and is competitive with state-of-the-art methods.

Contribution

It presents a novel SMT-based approach for learning minimal weighted automata with proven partial correctness and termination guarantees.

Findings

Capable of learning minimal WFAs over finite and infinite semirings.

Vastly outperforms naive baseline methods.

Produces smaller automata with less interaction compared to existing algorithms.

Abstract

We present an SMT-based active learning algorithm for nondeterministic weighted automata (WFAs) as a practical and robust alternative to Hankel/L*-style methods. Our algorithm is parametric in a given semiring and, if it terminates, guaranteed to produce minimal WFAs. We prove partial correctness and provide a sufficient termination condition, which in particular implies termination for all finite semirings. Our extensive experimental evaluation shows that our algorithm is capable of learning numerous minimal WFAs over both finite and infinite semirings, vastly outperforms a naive baseline, and is competitive with a state-of-the-art algorithm while producing significantly smaller automata and requiring less interaction with the teacher.