Guiding LLM Temporal Logic Generation with Explicit Separation of Data and Control
CoRR(2024)
摘要
Temporal logics are powerful tools that are widely used for the synthesis and
verification of reactive systems. The recent progress on Large Language Models
(LLMs) has the potential to make the process of writing such specifications
more accessible. However, writing specifications in temporal logics remains
challenging for all but the most expert users. A key question in using LLMs for
temporal logic specification engineering is to understand what kind of guidance
is most helpful to the LLM and the users to easily produce specifications.
Looking specifically at the problem of reactive program synthesis, we explore
the impact of providing an LLM with guidance on the separation of control and
data–making explicit for the LLM what functionality is relevant for the
specification, and treating the remaining functionality as an implementation
detail for a series of pre-defined functions and predicates. We present a
benchmark set and find that this separation of concerns improves specification
generation. Our benchmark provides a test set against which to verify future
work in LLM generation of temporal logic specifications.
更多查看译文
AI 理解论文
溯源树
样例
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要