时态逻辑分类器在环系统的鲁棒推理与验证
Robust Inference and Verification of Temporal Logic Classifier-in-the-loop Systems
摘要：
嵌入了机器学习模块的自治系统通常依赖于深度神经网络来对环境中的不同感兴趣对象进行分类，或者对系统采取不同的操作或策略。由于深度神经网络的非线性和高维性，自治系统的可解释性受到损害。此外，自治系统中的机器学习方法大多是数据密集型的，缺乏人类自然的常识知识和推理。在本文中，我们提出了时态逻辑分类器在循环系统的框架。时间逻辑分类器可以基于环境输出自治系统要采取的不同动作，使得自治系统的行为可以满足给定的时间逻辑规范。我们的方法是鲁棒的和可证明正确的，因为我们可以证明，自治系统的行为可以满足给定的时序逻辑规范（有界）干扰的存在。
英文摘要：
Autonomous systems embedded with machine learning modules often rely on deep neural networks for classifying different objects of interest in the environment or different actions or strategies to take for the system. Due to the non-linearity and high-dimensionality of deep neural networks, the interpretability of the autonomous systems is compromised. Besides, the machine learning methods in autonomous systems are mostly data-intensive and lack commonsense knowledge and reasoning that are natural to humans. In this paper, we propose the framework of temporal logic classifier-in-the-loop systems. The temporal logic classifiers can output different actions to take for an autonomous system based on the environment, such that the behavior of the autonomous system can satisfy a given temporal logic specification. Our approach is robust and provably-correct, as we can prove that the behavior of the autonomous system can satisfy a given temporal logic specification in the presence of (bounded) disturbances.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
