神经抽象是复杂的非线性动力模型的形式近似，通过神经 ODE 和抽象神经网络与具体动力模型之间的误差的保证上界来表示。本文通过形式归纳合成过程生成动力学模型，并讨论复杂神经 ODE 的抽象以提高可达性分析的效率。

Jul, 2023

抽象是一种关键的验证技术，可提高可伸缩性。然而，神经网络领域对抽象的使用迄今极其有限。本研究提供了一个更灵活的框架，可以通过其他神经元的线性组合替换神经元，从而改善减少。我们在句法和语义抽象上应用这种方法，并进行实证实现和评估。此外，我们引入了一种改进方法用于我们的抽象，以在减少和精确性之间找到更好的平衡。

Jul, 2023

我们通过调整表示分布的熵，训练神经模型生成一系列离散表示，并在微调实验中展示了将表示调整到任务适当复杂度水平支持最高微调性能，并通过离散表示的可视化帮助用户在下游任务中识别适当的复杂度水平，这为利用人类洞察力快速微调模型指明了一个有希望的方向。

Oct, 2023

本文提出一种新的方法，通过共享基于低维学习的环境编码来明确地连接无模型和有模型的强化学习方法，该方法能够捕捉到总结性抽象，同时具有模块化的特点，因此具有良好的泛化能力和计算效率，并在较小的潜在状态空间中进行计划。此外，此方法还能恢复足够低维的环境表示，从而为可解释的人工智能、探索和迁移学习开辟了新的策略。

Sep, 2018

本文提出了一种用于验证神经网络鲁棒性的新算法 Charon，并通过实验评估其在数百个基准测试中显著优于 AI^2，Reluplex 和 Reluval 等三种最先进的工具。

Apr, 2019

我们对简单强化学习基准问题中控制器的鲁棒性提出了关注。我们关注神经网络控制器及其低神经元和符号抽象。即使典型控制器达到较高的平均回报值，它仍会产生大量持续低回报的解，这是一种高度不受欢迎的特性，容易被对手利用。我们发现简单控制器容易产生更多持续的坏解。我们提供了一种系统鲁棒性研究算法，并使用计算辅助证明方法证明了持续解的存在以及在某些情况下的周期轨道。

Jul, 2023

本研究提出了一种通过使用过度逼近来减小神经网络规模，以提高神经网络验证技术的框架，并使用反例引导调整逼近，以验证大型神经网络。实验证明，该方法对验证大型神经网络具有很大的潜力。

Oct, 2019

该论文针对多智能体控制问题提出了分层方法，其中包括三个阶段：计算系统的高级计划、通过 SMT 公式处理组合问题，以及使用强化学习获得神经网络控制策略，由于其正确性具有构建性，但缺乏实时执行功能，因此使用 SWA-SMT 解决方案作为最后阶段的初始训练数据集

Jul, 2023

自动化合成控制器，基于概率时间逻辑规范的随机动态模型，通过状态验证技术构建的 iMDP（带概率区间的马尔科夫决策过程），解决安全关键场景中面临的挑战。

Nov, 2023

本文提出了基于信号时间逻辑和控制障碍函数的神经网络控制器综合算法，以优化指定性能目标并满足硬性约束条件，在飞行器和单轮车等测试系统上进行了验证。

Oct, 2022