Introduction
Generative AI and in particular Large Language Models have been proved to be an interesting technology in understanding and analysing both text and source code.
Spazio IT has been experimenting with this technology since beginning of 2023 and some of the results of this research have been presented at the 28th Ada-Europe International Conference on Reliable Software Technologies in June 2024.
Software Verification
Software Verification entails reading and analysing big if not huge documents sets and code bases. Both the documents and the sources can be described as list of «things», list of «objects», e.g.:
- A System Specification (RS) is a list of System Requirements
- a Software Specification is a list of Software Requirements
- a DDF is a list of Architectural Component
- a code base is a list of compilation units
- each compilation units is a list of classes, procedures and functions (of course the actual names of these «things» depend on the programming language).
All «things» in a list are identified by some kind of «ID». The lists are usually at different levels of abstraction, e.g. a list of specifications implements a list of requirements. Traceability information binds together, establishes a relationship between «things» usually belonging to lists at different level of abstraction, e.g.:
requirements –> design –> code
Automatic traceability checks have been working (up to now) only at «ID» level.
Generative AI opens new opportunities for a semantic match.
Local/Isolated Language Models
When users utilize generative AI systems like OpenAI’s ChatGPT, Google’s Gemini, or others provided by major tech companies for free, there’s no assurance that the data they input, i.e. the Content, specifically the information within the prompts, remains confidential.
It is always feasible to set up commercial registrations or contractual agreements that prohibit the service provider from retaining and exploiting user content, but these are merely business assurances. The sole method for users to ensure their content isn’t misused is by exclusively utilizing open-source models (with a thorough understanding of their functions) and operating these models on a private and local computing platform, completely isolated and protected.
Large language models demand huge computational resource. To be able to run these models on local and affordable computing platforms a technique, called “quantization” is used. Quantization refers to the process of reducing the precision of model parameters, typically by converting floating-point numbers (which have decimal precision) into integers with a smaller bit-width representation. While quantization introduces some loss of information, dithering, that is adding small amounts of random noise to the data before quantization, can help mitigate this loss by spreading the quantization error.
In addition to streamlining or “downsizing” the model, another method of conserving resources is to utilize efficient software platforms or frameworks, such as “ggml“.
Retrieval-Augmented Generation and future work
Attempting to apply Generative AI to Software Verification requires solving two major problems:
- How to make the model «digest» huge documents sets and code bases?
- How to build the correct prompts?
Spazio IT is tackling the first issue by leveraging the Retrieval-Augmented Generation (RAG) technology – i.e. “the process of optimizing the output of a large language model, so it references an authoritative knowledge base outside of its training data sources before generating a response”.
Spazio IT is also working on the generation of relevant prompts, starting from its static analysis tools.
Generative AI currently cannot replace a human reader when analyzing text or source code. However, the tools created by Spazio IT, which utilize Local Models and RAG technologies, are already capable of providing valuable feedback and helpful suggestions. Of course, these recommendations should undergo prior verification by human experts.
The following presentation describes how Generative AI can help Software Verification.