Our research interests broadly lie in the intersection of machine learning and formal methods. We am especially interested in combining inductive techniques from the area of machine learning and symbolic techniques from the area of logic. The group's overall goal is to build automated tools for the design, the construction, and the analysis of intelligent systems.

The group works on a number of topics, including:

• Verification of learning systems: automatically proving correctness properties (e.g., robustness) of learning systems.
• Explanability of artificial intelligence: generating provably correct explanations for the decision making of intelligent systems.
• Intelligent formal methods: tools that learn correctness and termination proofs for a wide range of systems, including hardware, software, and cyber-physical systems.
• Learning-based synthesis: automatically generating reactive systems and program code from logical specifications and examples.
• Specification learning/recommendation: learning-based methods that assist humans in writing formal specifications.
• Incorporating automata learning and symbolic reasoning in reinforcement learning, inverse reinforcement learning, and transfer learning.
• Learning theory: developing principled ways to combine learning and symbolic reasoning.

Our projects often extend into theoretical computer science, specifically to automata theory, game theory, and logic.