LLM-Powered Automatic Theorem Proving and Synthesis for Hybrid Systems and Game
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866908858614546432 |
|---|---|
| author | Kabra, Aditi Laurent, Jonathan Martins, Ruben Mitsch, Stefan Platzer, André |
| author_facet | Kabra, Aditi Laurent, Jonathan Martins, Ruben Mitsch, Stefan Platzer, André |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_00737 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | LLM-Powered Automatic Theorem Proving and Synthesis for Hybrid Systems and Game Kabra, Aditi Laurent, Jonathan Martins, Ruben Mitsch, Stefan Platzer, André Logic in Computer Science 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. |
| title | LLM-Powered Automatic Theorem Proving and Synthesis for Hybrid Systems and Game |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2603.00737 |