TLS4AI: Temporal Logic Sketching for Artificial Intelligence

• Applicant: Professor Dr. Daniel Neider
• Subject Area: Theoretical Computer Science
• Term: since 2020
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 434592664

Formal Methods encompass a range of mathematically rigorous techniques used for the specification, design, and verification of software, hardware, and cyber-physical systems. With a proven track record spanning decades, these techniques have consistently ensured the safety and reliability of complex computing systems across a broad range of sectors, including the software industry, critical infrastructure projects, and the automotive and aerospace sectors. Despite this success, there exists a crucial and often neglected obstacle with formal methods: virtually all techniques rely on the assumption that the specifications required for the design or verification of a system are available in a suitable format, are functionally correct, and precisely capture the properties the engineers had in mind. However, these assumptions are often unrealistic. Formalizing system requirements is notoriously difficult and error-prone, and the training effort required to reach proficiency with specification languages can be disproportionate to the expected benefits. To alleviate this severe limitation, the predecessor project introduced the novel concept of Temporal Logic Sketching (TLS). This innovative, computer-aided framework enables engineers to create formal specifications by expressing their high-level knowledge of a system as an incomplete specification, named sketch, where parts that are difficult to formalize can be left out. Furthermore, an engineer can provide examples of a system’s desired and undesired behavior. Based on these inputs, a so-called sketching algorithm completes the sketch by filling in the unspecified parts, resulting in a complete formal specification that is consistent with the provided examples and faithfully captures the engineer’s original design goals. The increasing demand for trustworthy AI has highlighted the vast potential of formal methods, and TLS in particular, to ensure the safety and reliability of AI systems, as emphasized by numerous researchers in the field. However, TLS was designed with formal verification and synthesis in mind, making the current framework challenging (if not impractical) for AI applications. Therefore, the goal of this follow-up project is to extend and enhance TLS to better meet the needs of the AI community. In particular, we will (i) adapt TLS to accommodate multi-agent systems and interpretable machine learning, (ii) improve the integration of domain knowledge, (iii) investigate the theoretical foundations of TLS to enhance its performance and inform example selection, (iv) improve its scalability to meet the demand of real-world AI applications, and (v) develop a software tool and web-based demonstrator to empirically evaluate our algorithms and ensure broad dissemination of our research. By doing so, we seek to significantly simplify the process of applying formal methods in AI, empowering researchers and practitioners to build more robust, safe, and explainable AI systems.

• DFG Programme: Research Grants