We present a method and an interactive tool named LLMon that utilizes an LLM for synthesizing RV monitors from temporal or natural language (NL) specifications. Our focus is on allowing the flexibility of defining further temporal constructs on top of the standard ones; it helps to better customize the temporal formalism for expressing requirements originally given in NL. Our method allows the user to define new temporal operators through interaction with the tool. The LLM reframes the given descriptions of new operators, provided by the user in natural language, and synthesizes code for each alternative description. It performs analysis that compares the alternative generated codes, based on searching for traces with distinguishing verdicts. It then generates verbal descriptions that help the user to select the correct semantic interpretation. The tool can be used to synthesize monitors either directly from specifications in the extended temporal logic, or from NL descriptions.

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

The Power of Reframing: Using LLMs in Synthesizing RV Monitors

  • Itay Cohen,
  • Klaus Havelund,
  • Doron Peled,
  • Yoav Goldberg

摘要

We present a method and an interactive tool named LLMon that utilizes an LLM for synthesizing RV monitors from temporal or natural language (NL) specifications. Our focus is on allowing the flexibility of defining further temporal constructs on top of the standard ones; it helps to better customize the temporal formalism for expressing requirements originally given in NL. Our method allows the user to define new temporal operators through interaction with the tool. The LLM reframes the given descriptions of new operators, provided by the user in natural language, and synthesizes code for each alternative description. It performs analysis that compares the alternative generated codes, based on searching for traces with distinguishing verdicts. It then generates verbal descriptions that help the user to select the correct semantic interpretation. The tool can be used to synthesize monitors either directly from specifications in the extended temporal logic, or from NL descriptions.