  We investigate an approach for extracting knowledge from trained neural
networks based on Angluin's exact learning model with membership and
equivalence queries to an oracle. In this approach, the oracle is a trained
neural network. We consider Angluin's classical algorithm for learning Horn
theories and study the necessary changes to make it applicable to learn from
neural networks. In particular, we have to consider that trained neural
networks may not behave as Horn oracles, meaning that their underlying target
theory may not be Horn. We propose a new algorithm that aims at extracting the
"tightest Horn approximation" of the target theory and that is guaranteed to
terminate in exponential time (in the worst case) and in polynomial time if the
target has polynomially many non-Horn examples. To showcase the applicability
of the approach, we perform experiments on pre-trained language models and
extract rules that expose occupation-based gender biases.
