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

TL;DR

This paper leverages Large Language Models to enhance formal verification and synthesis in hybrid systems and games, enabling automation for complex cyber-physical systems previously out of reach.

Contribution

It introduces a novel approach combining LLMs with differential game logic for scalable verification and synthesis of hybrid systems and games.

Findings

Verification succeeded in all five case studies.

Control synthesis succeeded in four case studies.

Demonstrated scalability beyond existing automatic techniques.

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.