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

TL;DR

This paper presents a formal framework in Agda for analyzing the run-time complexity of active learning algorithms by modeling them as coalgebras, enabling rigorous proofs of bounds without knowing the hidden automaton.

Contribution

It introduces a coalgebraic formalization of learning algorithms in Agda, allowing for automated proofs of query complexity bounds in active learning.

Findings

Proved upper and lower bounds of (\u221a n) for number guessing game in Agda.

Demonstrated the framework's ability to formalize run-time analysis of learning algorithms.

Showed how to model learners and teachers as coalgebras for complexity proofs.

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 is, 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 both the lower and upper bound on number of guesses by the learner is $\mathcal{O}(\log n)$, where $n$ is the teacher's secret number.