# SMT-Based Active Learning of Weighted Automata

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 6 of its 37 references that are in the map.
- First posted on arXiv 8 May 2026.

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

- [Prognosis: Closed-Box Analysis of Network Protocol Implementations](https://mlsanity.com/paper/2201.02577/) (2021)
- [Weighted Programming](https://mlsanity.com/paper/2202.07577/) (2022)
- [Feasability of Learning Weighted Automata on a Semiring](https://mlsanity.com/paper/2309.07806/) (2023)
- [On Learning Polynomial Recursive Programs](https://mlsanity.com/paper/2310.14725/) (2023)
- [An L^* Algorithm for Deterministic Weighted Regular Languages](https://mlsanity.com/paper/2411.06228/) (2024)
- [Weighted NetKAT: A Programming Language For Quantitative Network Verification](https://mlsanity.com/paper/2604.13987/) (2026)

## Abstract (arXiv)

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.