REVIEW 5 cited by
Guiding LLM Temporal Logic Generation with Explicit Separation of Data and Control
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Guiding LLM Temporal Logic Generation with Explicit Separation of Data and Control
read the original abstract
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.
Forward citations
Cited by 5 Pith papers
-
Incentivizing Vision Language Models to Search for Long Video Question Answering
RL post-training of a VLM agent with neuro-symbolic temporal-logic rewards for evidence retrieval raises Pass@1 by up to 8% and Pass@4 by 15% on long-video QA.
-
Truth or Sophistry? LoFa: A Benchmark for LLM Robustness Against Logical Fallacies
LoFa is a new benchmark and LFR@k metric for measuring LLM resistance to sustained logical fallacy attacks via generated question-argument pairs and debate simulations.
-
Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models
A neuro-symbolic system using large reasoning models and model checkers outperforms dedicated reactive synthesis tools on benchmarks and handles parameterized systems.
-
As You Wish: Mission Planning with Formal Verification using LLMs in Precision Agriculture
Authors add multiple LTL-based verification feedback loops using two different LLMs to an existing natural-language mission planner for agricultural robots to ensure plans satisfy user specifications.
-
Syntax Is Easy, Semantics Is Hard: Evaluating LLMs for LTL Translation
LLMs handle LTL syntax better than semantics, improve with detailed prompts, and perform substantially better when the task is reframed as Python code completion.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.