# Guiding LLM Temporal Logic Generation with Explicit Separation of Data and Control

arXiv: https://arxiv.org/abs/2406.07400 · HTML: https://mlsanity.com/paper/2406.07400/

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Builds on 5 of its 13 references that are in the map.
- First posted on arXiv 11 Jun 2024.

## Builds on (most cited first, 5 of 5)

- [SWE-bench: Can Language Models Resolve Real-World GitHub Issues?](https://mlsanity.com/paper/2310.06770/) (2023)
- [nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models](https://mlsanity.com/paper/2303.04864/) (2023)
- [Procedural Adherence and Interpretability Through Neuro-Symbolic Generative Agents](https://mlsanity.com/paper/2402.16905/) (2024)
- [Parameterized Synthesis Case Study: AMBA AHB (extended version)](https://mlsanity.com/paper/1406.7608/) (2014)
- [Syntroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications](https://mlsanity.com/paper/2101.07232/) (2021)

## Built on by (most cited first, 8 of 8)

- [LLMs as Planning Formalizers: A Survey for Leveraging Large Language Models to Construct Automated Planning Models](https://mlsanity.com/paper/2503.18971/) (2025)
- [The Fusion of Large Language Models and Formal Methods for Trustworthy AI Agents: A Roadmap](https://mlsanity.com/paper/2412.06512/) (2024)
- [Towards a Common Framework for Autoformalization](https://mlsanity.com/paper/2509.09810/) (2025)
- [Incentivizing Vision Language Models to Search for Long Video Question Answering](https://mlsanity.com/paper/2607.02959/) (2026)
- [LTLf Learning Meets Boolean Set Cover](https://mlsanity.com/paper/2509.24616/) (2025)
- [Syntax Is Easy, Semantics Is Hard: Evaluating LLMs for LTL Translation](https://mlsanity.com/paper/2604.07321/) (2026)
- [Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models](https://mlsanity.com/paper/2605.15131/) (2026)
- [As You Wish: Mission Planning with Formal Verification using LLMs in Precision Agriculture](https://mlsanity.com/paper/2606.18519/) (2026)

## Abstract (arXiv)

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.