Abstract
\([Context\,and\,Motivation]\) Large Language Models (LLMs) have made remarkable advancements in emulating human linguistic capabilities, showing potential in executing various traditional software engineering tasks, including code generation. [Question/Problem] Despite their generally good performance, utilizing LLM-generated code raises legitimate concerns regarding its correctness and the assurances it can provide. [Principal Idea/Results] To address these concerns, we propose turning to formal requirements engineering—a practice currently predominantly used in developing complex systems where adherence to standards and accountability are required. [Contribution] In this vision paper, we discuss the integration of automatic formal requirements engineering techniques as a complement to LLM code generation. Additionally, we explore how LLMs can facilitate the broader acceptance of formal requirements, thus making the vision proposed in this paper realizable.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Note that to improve the LLM performance the model can be fine-tuned through a training phase using a set of examples. Fine-tuned models typically perform better than just prompting [23].
References
Bibel, W.: Automated Theorem Proving. Springer, Wiesbaden (2013). https://doi.org/10.1007/978-3-322-90102-6
Brun, Y., Meliou, A.: Software fairness. In: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 754–759 (2018)
Brunello, A., Montanari, A., Reynolds, M.: Synthesis of LTL formulas from natural language texts: state of the art and research directions. In: 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2019)
Chen, M., et al.: Evaluating large language models trained on code. arXiv preprint arXiv:2107.03374 (2021)
Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. Formal Methods Syst. Des. 43, 61–92 (2013)
Chen, Y., Gandhi, R., Zhang, Y., Fan, C.: NL2TL: transforming natural languages to temporal logics using large language models. arXiv preprint arXiv:2305.07766 (2023)
Cherukuri, H., Ferrari, A., Spoletini, P.: Towards explainable formal methods: from LTL to natural language with neural machine translation. In: Gervasi, V., Vogelsang, A. (eds.) REFSQ 2022. LNCS, vol. 13216, pp. 79–86. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-98464-9_7
Chong, N., et al.: Code-level model checking in the software development workflow. In: Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering: Software Engineering in Practice (2020)
Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R., et al.: Handbook of Model Checking, vol. 10. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-10575-8
Czepa, C., Zdun, U.: On the understandability of temporal properties formalized in linear temporal logic, property specification patterns and event processing language. IEEE Trans. Softw. Eng. 46(1), 100–112 (2018)
De Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24
Dietsch, D., Langenfeld, V., Westphal, B.: Formal requirements in an informal world. In: 2020 IEEE Workshop on Formal Requirements (FORMREQ), pp. 14–20. IEEE (2020)
D’silva, V., Kroening, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. IEEE Trans. Comput. Aided Des. Integr. Circ. Syst. 27(7), 1165–1178 (2008)
Fan, A., et al.: Large language models for software engineering: survey and open problems. arXiv preprint arXiv:2310.03533 (2023)
Gopalan, N., Arumugam, D., Wong, L.L., Tellex, S.: Sequence-to-sequence language grounding of non-Markovian task specifications. In: Robotics: Science and Systems, vol. 2018 (2018)
Greenspan, S., Mylopoulos, J., Borgida, A.: On formal requirements modeling languages: RML revisited. In: Proceedings of 16th International Conference on Software Engineering, pp. 135–147. IEEE (1994)
Hou, X., et al.: Large language models for software engineering: a systematic literature review. arXiv preprint arXiv:2308.10620 (2023)
Huang, D., Bu, Q., Zhang, J., Xie, X., Chen, J., Cui, H.: Bias testing and mitigation in LLM-based code generation (2024)
Katoen, J.P.: The probabilistic model checking landscape. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (2016)
Knobelsdorf, M., Frede, C., Böhne, S., Kreitz, C.: Theorem provers as a learning tool in theory of computation. In: Proceedings of the 2017 ACM Conference on International Computing Education Research, pp. 83–92 (2017)
Liu, J.X., et al.: Lang2LTL: translating natural language commands to temporal robot task specification. arXiv preprint arXiv:2302.11649 (2023)
Liu, T., Nagel, M., Taghdiri, M.: Bounded program verification using an SMT solver: a case study. In: 2012 IEEE Fifth International Conference on Software Testing, Verification and Validation, pp. 101–110. IEEE (2012)
Min, B., et al.: Recent advances in natural language processing via large pre-trained language models: a survey. ACM Comput. Surv. 56(2), 1–40 (2023)
Patel, R., Pavlick, E., Tellex, S.: Grounding language to non-Markovian tasks with no supervision of task specifications. In: Robotics: Science and Systems (2020)
Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), pp. 46–57. IEEE (1977)
Shah, D., Osiński, B., Levine, S., et al.: LM-NAV: robotic navigation with large pre-trained models of language, vision, and action. In: Conference on Robot Learning, pp. 492–504. PMLR (2023)
Coq Development Team: he Coq proof assistant (1989–2023). http://coq.inria.fr
Wang, R.E., Durmus, E., Goodman, N., Hashimoto, T.: Language modeling via stochastic processes. arXiv preprint arXiv:2203.11370 (2022)
Ye, H., Liu, T., Zhang, A., Hua, W., Jia, W.: Cognitive mirage: a review of hallucinations in large language models. arXiv preprint arXiv:2309.06794 (2023)
Zan, D., et al.: Large language models meet NL2Code: a survey. In: Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp. 7443–7464 (2023)
Zhao, W.X., et al.: A survey of large language models. arXiv preprint arXiv:2303.18223 (2023)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Spoletini, P., Ferrari, A. (2024). The Return of Formal Requirements Engineering in the Era of Large Language Models. In: Mendez, D., Moreira, A. (eds) Requirements Engineering: Foundation for Software Quality. REFSQ 2024. Lecture Notes in Computer Science, vol 14588. Springer, Cham. https://doi.org/10.1007/978-3-031-57327-9_22
Download citation
DOI: https://doi.org/10.1007/978-3-031-57327-9_22
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-57326-2
Online ISBN: 978-3-031-57327-9
eBook Packages: Computer ScienceComputer Science (R0)