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.

通过给大型语言模型提供关于控制和数据分离的指导，我们探讨了在反应式程序合成中为LLM提供指导对于规范生成的影响，发现这种关注点的分离改进了规范生成，并提供了一个基准测试集用于验证未来的LLM生成时态逻辑规范的工作。

使用明确的数据和控制分离引导LLM时态逻辑生成