Large Language Models

Towards Combining the Cognitive Abilities of Large Language Models with the Rigor of Deductive Progam Verification
We evaluate the potential of Large Language Models (specifically GPT 3.5 and GPT 4o) for the generation of code annotations in the Java Modelling Language using a prototypical integration of the Java verification tools KeY and JJBMC with OpenAI’s API.
Bernhard Beckert, Jonas Klamroth, Wolfram Pfeifer, Patrick Röper, Samuel Teuber
Cite