Machine Learning with Guarantees using Descriptive Complexity and SMT Solvers
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.
Code (0)
등록된 구현이 없습니다.
Tasks
BIG-bench Machine LearningBoard GamesDescriptiveLearning TheorySimilar Papers 제목 키워드 기반
Structural Analysis of Branch-and-Cut and the Learnability of Gomory Mixed Integer Cuts
The incorporation of cutting planes within the branch-and-bound algorithm, known as branch-and-cut, forms the backbone of modern integer programming solvers. These solvers are the foremost method for solving discrete opt…
BIG-bench Machine LearningLinear Bandit Algorithms with Sublinear Time Complexity
We propose two linear bandits algorithms with per-step complexity sublinear in the number of arms $K$. The algorithms are designed for applications where the arm set is extremely large and slowly changing. Our key realiz…
Movie RecommendationImproved Sample Complexity Bounds for Branch-and-Cut
Branch-and-cut is the most widely used algorithm for solving integer programs, employed by commercial solvers like CPLEX and Gurobi. Branch-and-cut has a wide variety of tunable parameters that have a huge impact on the …
Efficient Alternating Minimization Solvers for Wyner Multi-View Unsupervised Learning
In this work, we adopt Wyner common information framework for unsupervised multi-view representation learning. Within this framework, we propose two novel formulations that enable the development of computational efficie…
Computational EfficiencyRepresentation LearningVariational InferenceTensor Gaussian Processes: Efficient Solvers for Nonlinear PDEs
Machine learning solvers for partial differential equations (PDEs) have attracted growing interest. However, most existing approaches, such as neural network solvers, rely on stochastic training, which is inefficient and…
Gaussian Processes