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 时态逻辑生成

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

Deep neural networks (DNNs) are increasingly being used as controllers in
reactive systems. However, DNNs are highly opaque, which renders it difficult
to explain and justify their actions. To mitigate this issue, there has been a
surge of interest in explainable AI (XAI) techniques, capable of pinpointing
the input features that caused the DNN to act as it did.
Existing XAI techniques typically face two limitations: (i) they are
heuristic, and do not provide formal guarantees that the explanations are
correct; and (ii) they often apply to ``one-shot'' systems (where the DNN is
invoked independently of past invocations), as opposed to reactive systems.
Here, we begin bridging this gap, and propose a formal DNN-verification-based
XAI technique for reasoning about multi-step, reactive systems. We suggest
methods for efficiently calculating succinct explanations, by exploiting the
system's transition constraints in order to curtail the search space explored
by the underlying verifier. We evaluate our approach on two popular benchmarks
from the domain of automated navigation; and observe that our methods allow the
efficient computation of minimal and minimum explanations, while significantly
outperforming the state of the art. We also demonstrate that our method
produces formal explanations that are more reliable than competing,
non-verification-based XAI techniques.

深度神经网络在反应式系统中作为控制器的应用越来越多。为了解释和证明其行为，可解释的人工智能（XAI）技术引起了人们的广泛兴趣。本文提出了一种形式化的 DNN 验证型 XAI 技术，用于推理多步骤的反应式系统，并通过利用系统的过渡约束来计算简洁的解释。在自动导航领域的两个广泛应用的基准测试中，我们的方法在计算最小和最小解释时表现出了高效的性能，同时比现有技术更可靠。

在反应系统内正式解释神经网络

Formally Explaining Neural Networks within Reactive Systems

Multi-Agent Reinforcement Learning (MARL) discovers policies that maximize
reward but do not have safety guarantees during the learning and deployment
phases. Although shielding with Linear Temporal Logic (LTL) is a promising
formal method to ensure safety in single-agent Reinforcement Learning (RL), it
results in conservative behaviors when scaling to multi-agent scenarios.
Additionally, it poses computational challenges for synthesizing shields in
complex multi-agent environments. This work introduces Model-based Dynamic
Shielding (MBDS) to support MARL algorithm design. Our algorithm synthesizes
distributive shields, which are reactive systems running in parallel with each
MARL agent, to monitor and rectify unsafe behaviors. The shields can
dynamically split, merge, and recompute based on agents' states. This design
enables efficient synthesis of shields to monitor agents in complex
environments without coordination overheads. We also propose an algorithm to
synthesize shields without prior knowledge of the dynamics model. The proposed
algorithm obtains an approximate world model by interacting with the
environment during the early stage of exploration, making our MBDS enjoy formal
safety guarantees with high probability. We demonstrate in simulations that our
framework can surpass existing baselines in terms of safety guarantees and
learning performance.

该论文提出了一种基于模型的动态屏蔽（MBDS）方法来支持多智能体强化学习算法设计，同时在强化学习和部署阶段实现形式化安全性保证。该算法合成分布式屏蔽，可以在与每个 MARL 代理并行运行的情况下监视和纠正不安全行为，从而实现对多智能体复杂环境的有效监控，并具有强有力的安全性保证。