We demonstrate how LLMs can be harnessed to synthesize runtime verification monitors from natural language specifications. We instruct the LLM through prompts to assemble the monitors through a sequence of stages. To start with, we employ the learned insights LLMs possess regarding linear temporal logic for translating natural language specifications into propositional past time LTL formulas. Next, we utilize a sequence of prompts to synthesize from the LTL specification a runtime verification monitor for the given formula. Part of these prompts enable the LLM to validate its own outputs, thereby significantly improving the probability of obtaining a correct monitor.

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

End-to-End AI Generated Runtime Verification from Natural Language Specification

  • Itay Cohen,
  • Doron Peled

摘要

We demonstrate how LLMs can be harnessed to synthesize runtime verification monitors from natural language specifications. We instruct the LLM through prompts to assemble the monitors through a sequence of stages. To start with, we employ the learned insights LLMs possess regarding linear temporal logic for translating natural language specifications into propositional past time LTL formulas. Next, we utilize a sequence of prompts to synthesize from the LTL specification a runtime verification monitor for the given formula. Part of these prompts enable the LLM to validate its own outputs, thereby significantly improving the probability of obtaining a correct monitor.