Machine Learning with Guarantees using Descriptive Complexity and SMT Solvers
This work addresses the problem of providing strong theoretical guarantees for machine learning methods, which is incremental as it builds on existing logical and complexity theory.
The paper tackles the gap between efficiency and theoretical guarantees in machine learning by introducing a logical framework using descriptive complexity and SMT solvers, with experimental results including learning reduction rules for board games.
Machine learning is a thriving part of computer science. There are many efficient approaches to machine learning that do not provide strong theoretical guarantees, and a beautiful general learning theory. Unfortunately, machine learning approaches that give strong theoretical guarantees have not been efficient enough to be applicable. In this paper we introduce a logical approach to machine learning. Models are represented by tuples of logical formulas and inputs and outputs are logical structures. We present our framework together with several applications where we evaluate it using SAT and SMT solvers. We argue that this approach to machine learning is particularly suited to bridge the gap between efficiency and theoretical soundness. We exploit results from descriptive complexity theory to prove strong theoretical guarantees for our approach. To show its applicability, we present experimental results including learning complexity-theoretic reductions rules for board games. We also explain how neural networks fit into our framework, although the current implementation does not scale to provide guarantees for real-world neural networks.