LLM-based framework to support the construction of valid formal models

Guta, Gábor and 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. Eszterházy Károly Katolikus Egyetem Líceum Kiadó, Eger, pp. 78-89. ISBN 9789634963035

Preview

Text fmfai2025_pp078-089.pdf - Published Version Download (609kB) | Preview

Abstract

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.

Actions (login required)

Edit Item