Abstract:
Machine teaching is an algorithmic framework for teaching a target hypothesis via a sequence of examples or demonstrations. We investigate machine teaching for temporal logic formulas—a novel and expressive hypothesis class amenable to time-related task specifications. In the context of teaching temporal logic formulas, an exhaustive search even for a myopic solution takes exponential time (with respect to the time span of the task). We propose an efficient approach for teaching parametric linear temporal logic formulas. Concretely, we derive a necessary condition for the minimal time length of a demonstration to eliminate a set of hypotheses. Utilizing this condition, we propose an efficient myopic teaching algorithm by solving a sequence of integer programming problems. We further show that, under two notions of teaching complexity, the proposed algorithm has near-optimal performance. We evaluate our algorithm extensively under different classes of learners (i.e., learners with different preferences over hypotheses) and interaction protocols (e.g., non-adaptive and adaptive). Our results demonstrate the effectiveness of the proposed algorithm in teaching temporal logic formulas; in particular, we show that there are significant gains of teaching efficacy when the teacher adapts to feedback of the learner, or adapts to a (non-myopic) oracle.
