Functional Synthesis via Formal Methods and Machine Learning
Abstract:
Functional synthesis, a fundamental task in computer science, involves automatically generating functions that meet specific user requirements. Its practical applications span a wide range, from automatically repairing programs to cryptanalysis. While theoretical investigations have shown that certain instances of functional synthesis can be exceptionally time-consuming, the need for practical usability has spurred the development of algorithms that showcase remarkable scalability. Despite these significant strides, practical challenges persist, and there are still real-world situations where current methods encounter limitations.
In my thesis, we delve into the topic of functional synthesis, examining it through the lens of recent advancements in machine learning and formal methods. We present a novel approach called Manthan, which treats functional synthesis as a classification problem. Manthan leverages innovative techniques for data generation and employs formal methods to guide repair and verification processes. Notably, Manthan demonstrates remarkable scalability, outperforming previous state-of-the-art methods by handling 40% more instances to synthesize functions. Moreover, the impressive scalability achieved by Manthan prompts us to consider its applications in various domains. We propose a reduction of program synthesis to functional synthesis. This reduction transforms Manthan into a cutting-edge solution for synthesizing programs based on bit-vector theory.
Taking a progressive stride, and acknowledging the demand for a versatile framework that can adapt to a range of real-world scenarios, encompassing situations requiring adherence to hard constraints as well as accommodating more adaptable (soft) constraints, we introduce a synthesis framework. The framework ensures compliance with strict constraints and strives to achieve predefined goodness measures for soft constraints.