In automated learning problems, the task is to find a model that maps given inputs to their corresponding outputs as accurately as possible. Over the past 30 years, machine learning and deep learning have achieved tremendous success in solving this type of problem. However, while the resulting models can be used to make predictions, they offer limited interpretability, i.e. they provide little insight into *how* they solve the problem. For instance, if we train a recurrent neural network to predict whether a sequence of events will lead to a crash, the model cannot describe the sequences of events that lead to crashes and provide solutions to remediate the issue. Program synthesis is a framework for solving learning problems with models that are programs in a domain-specific language, which allows creating interpretable models in the domain of the problem.
In this talk, I will present our recent work on enumeration algorithms for program synthesis. I will begin with an introduction to program synthesis, using examples from program de-obfuscation and anomaly explanation. In the second part, I will present the main techniques used in our algorithms: observational equivalence and domination, pruning techniques used to reduce the search space, and massively parallel approaches. Finally, I will discuss the engineering choices we made when implementing this algorithm for learning Linear Temporal Logic (LTL) formulas in Bolt, our open-source tool, available at https://github.com/SynthesisLab/Bolt.
This talk is based on joint work with Nathanaël Fijalkow, Théo Matricon, Baptiste Mouillon and Pierre Vandenhove.
