一句话：提出工具 Prophecy，通过神经元激活状态自动推断神经网络的形式化性质，支持解释、验证与监控。
神经网络内部逻辑难以形式化刻画，导致其验证、解释与运行时监控缺乏可用的形式化性质。本文提出工具 Prophecy，其核心观察是网络内部大量逻辑体现在内层神经元的激活状态中。Prophecy 从神经元的激活值或开/关状态提取规则，作为蕴含期望输出性质（如预测为某类别）的前置条件。文中介绍该工具的架构与特性，并在不同模型和输出性质上演示其用法，概述其在推断与证明形式化解释、组合验证、运行时监控和修复等方面的应用，还展示了在大型视觉语言模型上的新结果，表明该方法具有潜力。
We present Prophecy, a tool for automatically inferring formal properties of neural networks. Prophecy is based on the observation that a significant part of the logic of neural networks is captured in the activation status of the neurons at inner layers. Prophecy works by extracting rules based on neuron activations (values or on/off statuses) as preconditions that imply certain desirable output property, e.g., the prediction being a certain class. We present the architecture of the tool, highlight its features and demonstrate its usage on different types of models and output properties. We also present an overview of its applications, such as inferring and proving formal explanations of neural networks, compositional verification, run-time monitoring, repair, and others. We also show novel results highlighting its potential in the era of large vision-language models. Demo: https://youtu.be/Xrd3v2JRW7E