Machine Learning with Guarantees using Descriptive Complexity and SMT Solvers

TL;DR

This paper introduces a logical framework for machine learning that leverages descriptive complexity and SMT solvers to achieve strong theoretical guarantees while maintaining efficiency.

Contribution

It presents a novel logical approach to machine learning using formulas and structures, bridging the gap between efficiency and theoretical soundness.

Findings

Framework evaluated with SAT and SMT solvers

Proves strong theoretical guarantees using descriptive complexity

Demonstrates learning complexity reductions for board games

Abstract

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.