Formalizing Requirements using Large Language Models (LLMs)
| Typ | Bachelorarbeit | |
|---|---|---|
| Aushang | ReqForm.pdf | |
| Betreuer | Wenden Sie sich bei Interesse oder Fragen bitte an: Tobias Hey (E-Mail: hey@kit.edu, Telefon: +49-721-608-44765) |
Motivation
Software requirements are often written in natural language to facilitate communication among stakeholders, but their ambiguity and lack of formal structure make them difficult to use directly in formal verification. Converting these informal requirements into precise formal specifications is a crucial yet labor-intensive task that demands specialized expertise. Recent advancements in Large Language Models (LLMs) offer an opportunity to automate this translation by understanding and formalizing natural language descriptions. By leveraging LLMs to generate formal specifications, such as those expressed in temporal logics like Computation Tree Logic (CTL), this research aims to reduce human effort, minimize errors, and strengthen the connection between requirements engineering and formal verification, ultimately improving software reliability.
Task Description
This thesis aims to develop and evaluate a novel approach for using Large Language Models (LLMs) to automatically formalize natural language requirements into precise specifications, such as those expressed in Computation Tree Logic (CTL). The research will focus on designing methods that enable LLMs to interpret and transform stakeholder requirements into logically sound formal representations. The approach will be trained, tested, and validated using existing benchmark datasets to assess its accuracy and effectiveness. Ultimately, the work seeks to improve automation in requirements engineering and strengthen the integration between requirements specification and formal verification.