Formalized Run-Time Analysis of Active Learning -- Coalgebraically in Agda

Abstract

The objective of automata learning is to reconstruct the implementation of a hidden automaton, to which only a teacher has access. The learner can ask certain kinds of queries to the teacher to gain more knowledge about the hidden automaton. The run-time of such a learning algorithm is then measured in the number of queries it takes until the hidden automaton is successfully reconstructed, which is usually parametric in the number of states of that hidden automaton. How can we prove such a run-time complexity of learning algorithms in a proof assistant if we do not have the hidden automaton and the number of states available? In the present paper, we solve this by considering learning algorithms themselves as generalized automata, more specifically as coalgebras. We introduce formal and yet compact definitions of what a learner and a teacher are, which make it easy to prove upper and lower bounds of different kinds of learning games in the proof assistant Agda. As a running example, we discuss the common number guessing game where a teacher thinks of a natural number and answers guesses by the learner with `correct', `too high', or `too low'. To demonstrate our framework, we formally prove in Agda that binary search finds the teacher's secret number $n$ within $\mathcal{O}(\log n)$ guesses and that no learning strategy can guarantee fewer than $\log_2(n)$ guesses. We apply our framework to automata learning to prove the following complexity bounds in Agda: (1) If the teacher does not provide counterexamples, then there is no learning algorithm that uses only polynomially many queries. (2) The $L^{\#}$-learning algorithm takes $\mathcal{O}(k\cdot n^2 + n\cdot \log(m))$ queries to learn a Mealy machine with $k$ input symbols, $n$ states, where $m$ is the maximum length of the teacher's counterexamples.