When: Friday, November 17, 2023, 9:30 (GMT).

Where: In person and Zoom online.

Topic: Neuro-Symbolic Methods for Reactive Synthesis, Repair, and Natural Language Formalization.

Speaker: Matthias Cosler.

Abstract

Neuro-symbolic methods bridge the gap between symbolic and neural approaches by combining symbolic knowledge with data-driven deep-learning techniques. In this talk, I will present our work on neuro-symbolic methods for reactive synthesis, automatic circuit repair, and natural language formalization.

Reactive synthesis is a challenging problem in computer science that dates back to Church in the 1950s as the automatic construction of a system that satisfies formal temporal requirements. We developed several transformer-based approaches that address the reactive synthesis problem and show remarkable out-of-distribution capabilities. Automatic circuit repair is the problem of repairing a faulty sequential circuit to a circuit that satisfies temporal requirements. We developed an approach to correct the defective circuit and analyzed the fault’s influence on the model’s training and evaluation. Applied iteratively to the reactive synthesis problem, our approach improves over previous work on all benchmarks. Further, we focus on the formalization of unstructured natural language requirements to Linear Temporal Logic (LTL) specifications. Manually formalizing requirements for verification or reactive synthesis is a tedious and error-prone task. Using large language models, we present a framework that aids with translating natural language expressions into formal logic and enables the use of these requirements for verification, planning, and system design. With these directions, we advance on important issues in the applicability of temporal reasoning with the help of deep learning.

Short Bio

Matthias Cosler is a Ph.D. student with Bernd Finkbeiner at CISPA Helmholtz Center for Information Security and Saarland University. He obtained his Bachelor’s and Master’s degrees at Saarland University. During his studies, he spent an exchange semester at Trinity College Dublin. His research interests are in the neuro-symbolic intersection of formal methods and deep learning, with a current focus on the application of transformers and large language models to temporal logic, and reactive synthesis.

Material