As developers increasingly rely on Large Language Models (LLMs) to generate code, the pace of software development is accelerating beyond the capabilities of traditional design-time verification and testing methods. We predict a paradigm shift towards continuous monitoring to complement and eventually supersede upfront verification. By embracing a “correct-ish by design” philosophy, we acknowledge the inevitability of imperfections in LLM-generated code. We anticipate an adaptive approach where real-time monitoring and feedback mechanisms are employed to detect, diagnose, and rectify issues as they emerge in the field. This continuous monitoring strategy not only ensures sustained software reliability and performance, but also provides valuable insights into LLM behavior, facilitating iterative improvements. Specifically, we use an LLM to generate Python code from a formal specification written in the VDM specification language, accessible as a PDF document. The VDM specification formalizes aspects of NASA’s SAFER rescue system, which uses small thrusters on a backpack to let astronauts maneuver and return safely to the spacecraft during spacewalks in case they become untethered. We experiment with property-based testing, and by using two Python programs, both generated from the specification by the LLM in two different developments, to monitor each other during runtime.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Correct-ish by Design: From Upfront Verification to Continuous Monitoring of LLM Generated Code

  • Bernhard K. Aichernig,
  • Klaus Havelund

摘要

As developers increasingly rely on Large Language Models (LLMs) to generate code, the pace of software development is accelerating beyond the capabilities of traditional design-time verification and testing methods. We predict a paradigm shift towards continuous monitoring to complement and eventually supersede upfront verification. By embracing a “correct-ish by design” philosophy, we acknowledge the inevitability of imperfections in LLM-generated code. We anticipate an adaptive approach where real-time monitoring and feedback mechanisms are employed to detect, diagnose, and rectify issues as they emerge in the field. This continuous monitoring strategy not only ensures sustained software reliability and performance, but also provides valuable insights into LLM behavior, facilitating iterative improvements. Specifically, we use an LLM to generate Python code from a formal specification written in the VDM specification language, accessible as a PDF document. The VDM specification formalizes aspects of NASA’s SAFER rescue system, which uses small thrusters on a backpack to let astronauts maneuver and return safely to the spacecraft during spacewalks in case they become untethered. We experiment with property-based testing, and by using two Python programs, both generated from the specification by the LLM in two different developments, to monitor each other during runtime.