Machine Learning Meets Program Reasoning: Opportunities and Challenges
Program reasoning is the central challenge in programming languages and formal methods research. The field has been largely driven by manually designed frameworks, heavily engineered symbolic solvers, and endless heuristics inspired by various domain expertise. Automatically adapting existing frameworks, solvers, heuristics to new programs with minimum or no human involvement is highly desirable. In recent years, machine learning achieved remarkable successes in visual object recognition, natural language understanding, and various decision making tasks. This motivates exciting research opportunities in both formal methods and machine learning — progress in machine learning sheds new light on automating formal reasoning with either small or big data; program reasoning can serve as the new grand challenge for machine learning, especially deep learning, a field rapidly driven by tackling grand challenges; furthermore, machine learning models can be viewed as a special kind of program, posing interesting new challenges for formal methods.
In this talk, I will share several paradigms of applying machine learning for program analysis and verification, with concrete examples in static analysis, loop invariant inference, and symbolic constraint solving. I will also discuss some unique challenges and opportunities in analyzing and verifying machine learning models.