Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

LLM-Powered Automatic Theorem Proving and Synthesis for Hybrid Systems and Game

Aditi Kabra, Jonathan Laurent, Ruben Martins, Stefan Mitsch, André Platzer

TL;DR

This work uses Large Language Models (LLMs) to scale formal verification and synthesis for hybrid systems and games for a high-level hybrid games symbolic logic, differential game logic (dGL).

Abstract

Hybrid games model cyber-physical systems (CPS), like cars, trains, and airplanes, where discrete control decisions interact with continuous physical dynamics. We use Large Language Models (LLMs) to scale formal verification and synthesis for hybrid systems and games for a high-level hybrid games symbolic logic, differential game logic (dGL). This combination of a logic with the right expressivity and automation of the interactive theorem proving process using LLMs brings within reach a challenging class of CPS verification/synthesis problems, that were previously well out of range of automatic theorem proving. We demonstrate it on five challenging case studies, all beyond the reach of existing automatic techniques. Verification succeeds for all five, and the synthesis of control solutions succeeds for four of the five.

LLM-Powered Automatic Theorem Proving and Synthesis for Hybrid Systems and Game

TL;DR

This work uses Large Language Models (LLMs) to scale formal verification and synthesis for hybrid systems and games for a high-level hybrid games symbolic logic, differential game logic (dGL).

Abstract

Hybrid games model cyber-physical systems (CPS), like cars, trains, and airplanes, where discrete control decisions interact with continuous physical dynamics. We use Large Language Models (LLMs) to scale formal verification and synthesis for hybrid systems and games for a high-level hybrid games symbolic logic, differential game logic (dGL). This combination of a logic with the right expressivity and automation of the interactive theorem proving process using LLMs brings within reach a challenging class of CPS verification/synthesis problems, that were previously well out of range of automatic theorem proving. We demonstrate it on five challenging case studies, all beyond the reach of existing automatic techniques. Verification succeeds for all five, and the synthesis of control solutions succeeds for four of the five.
Paper Structure (28 sections, 15 equations, 12 figures, 6 tables)

This paper contains 28 sections, 15 equations, 12 figures, 6 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. Automated Theorem Proving
  4. Background.
  5. Pipeline Description
  6. Case Studies
  7. Outcomes
  8. Verification Impact by Example
  9. Case Study: Lotka-Volterra.
  10. model:lotka-volterra Explanation.
  11. Synthesis
  12. Subvalue Maps
  13. Pipeline Description
  14. Outcomes
  15. Details of Verification Experiments
  16. ...and 13 more sections

Figures (12)

  • Figure 1: Schematic representation of tradeoffs in formal methods applied to Hybrid Systems.
  • Figure 2: Automated Theorem Proving Pipeline. app:verification-prompts shows prompts.
  • Figure 3: Lotka-Volterra Population Control. Gray text is part of the verification problem but is excluded during synthesis, where it is synthesized automatically.
  • Figure 4: A subvalue map for the running example.
  • Figure 5: Synthesis Pipeline. app:synthesis-prompts shows prompts.
  • ...and 7 more figures

Theorems & Definitions (2)

  • definition 1: semantics
  • definition 2: Semantics of hybrid games