Guta, Gábor, Kusper, Gábor (2025) LLM-based framework to support the construction of valid formal models In: Proceedings of the International Conference on Formal Methods and Foundations of Artificial Intelligence. Eger, Eszterházy Károly Catholic University. pp. 78-89.
![[thumbnail of fmfai2025_pp078-089.pdf]](http://publikacio.uni-eszterhazy.hu/style/images/fileicons/text.png) |
pdf
fmfai2025_pp078-089.pdf Download (609kB) [error in script] |
Absztrakt (kivonat)
The use of large language models (LLMs) in software development is becoming increasingly widespread, despite well-known concerns regarding their reliability. A significant risk arises from relying on poorly understood approximate solutions that may subtly introduce errors into the final system. A key barrier to the adoption of formal modeling – beyond the steep learning curve of formal specification languages – is the additional abstraction layer, which can be as difficult to maintain as the source code itself. This complexity persists even when the formal specification can generate code directly. Another challenge is that, while tools for verifying properties of formal models are well-established, the initial translation of a mental model into a formal one often results in invalid or imprecise representations. We propose a tool which facilitates the validation of formal models generated by LLMs from natural language specifications. The validation process involves two steps: first, the formal model is translated back into natural language using a deterministic, easily verifiable rule-based method; second, the author of the original specification validates this reformulated version. This human-in-the-loop method mitigates the risks associated with LLM black-box generation by enabling explicit semantic verification of the model.
| Mű típusa: | Könyvrészlet - Book section |
|---|---|
| Szerző: | Szerző neve Email MTMT azonosító ORCID azonosító Közreműködés Guta, Gábor gabor.guta@axonmatics.com NEM RÉSZLETEZETT NEM RÉSZLETEZETT Szerző Kusper, Gábor gkusper@aries.ektf.hu NEM RÉSZLETEZETT NEM RÉSZLETEZETT Szerző |
| Kapcsolódó URL-ek: | |
| Kulcsszavak: | LLM, formal specification, human-in-the-loop |
| Nyelv: | angol |
| DOI azonosító: | 10.17048/fmfai.2025.78 |
| Felhasználó: | Tibor Gál |
| Dátum: | 28 Okt 2025 10:08 |
| Utolsó módosítás: | 28 Okt 2025 10:08 |
| URI: | http://publikacio.uni-eszterhazy.hu/id/eprint/8804 |
 |
Tétel nézet |
