The intersection of deep learning and formal methods is a young research area that integrates deep neural networks with rigorous formal reasoning. Applications of deep learning to symbolic domains, such as programming languages, are already adopted but often lack the integration of formal reasoning and logics that are required for analyzing formal correctness.

In our research, we use deep learning methods to facilitate the formalization, formal verification and synthesis of software and hardware systems. The goals of this research can be described along the following lines (1) Developing methods with both neural and algorithmic components that increase the applicability and reduce the manual effort of formal methods. Practical instances of verification and synthesis problems often follow a particular structure, and similar problems are solved over and over again. Deep neural networks, with their ability to learn rich patterns and to improve from experience, can be utilized in such cases and largely increase efficiency. (2) Bridging formal methods with domains that are inherently difficult to formalize. Formal specifications are the cornerstone of formal methods, but it is often easier and more common to express specifications in natural language. The auto-formalization of specifications with language models emerged as a new paradigm to translate between those domains. (3) Developing a more principled understanding of the relationship between neural and symbolic reasoning mechanisms. To this end, formal reasoning problems provide a testbed rooted in computability, complexity, and comprehensive results on the relationship of problems to study training, generalization abilities, and expressive power of modern deep neural networks.