Learning Quantitative Automata Modulo Theories

TL;DR

This paper introduces QUINTIC, an active learning algorithm for deterministic quantitative automata that infers models from constraints rather than explicit examples, enabling efficient learning in preference-based scenarios.

Contribution

The paper proposes QUINTIC, a novel deductive reasoning-based active learning algorithm for quantitative automata from constraints, guaranteeing minimality and correct termination.

Findings

Effective learning of summation automata using theory of rationals

Successful inference of discounted summation and product automata

QUINTIC outperforms existing methods in constraint-based learning scenarios

Abstract

Quantitative automata are useful representations for numerous applications, including modeling probability distributions over sequences to Markov chains and reward machines. Actively learning such automata typically occurs using explicitly gathered input-output examples under adaptations of the L-star algorithm. However, obtaining explicit input-output pairs can be expensive, and there exist scenarios, including preference-based learning or learning from rankings, where providing constraints is a less exerting and a more natural way to concisely describe desired properties. Consequently, we propose the problem of learning deterministic quantitative automata from sets of constraints over the valuations of input sequences. We present QUINTIC, an active learning algorithm, wherein the learner infers a valid automaton through deductive reasoning, by applying a theory to a set of currently available constraints and an assumed preference model and quantitative automaton class. QUINTIC performs a complete search over the space of automata, and is guaranteed to be minimal and correctly terminate. Our evaluations utilize theory of rationals in order to learn summation, discounted summation, product, and classification quantitative automata, and indicate QUINTIC is effective at learning these types of automata.