Career: Correct-by-Learning Methods for Reliable Autonomy

具有高度自主能力的人参与的计算系统需要提供严格的安全保证。在这样的系统上，可以使用形式化方法来提供数学证明，以确保正确的行为。然而，机器学习和数据驱动方法现在是自主系统设计中不可或缺的一部分，它们对高度非线性连续函数和概率推理的依赖在很大程度上与形式化方法中的逻辑和符号分析框架不一致。因此，缺乏正式保证已成为阻碍自主系统更广泛部署和采用的关键瓶颈。该项目通过开发基于学习和数据驱动的自主系统控制和规划方法的正式综合和验证技术来应对这一公开挑战。该项目开发了理论基础以及实用技术和工具，以提高自动驾驶汽车和无人驾驶飞行器等现实自主系统的基本可靠性。这项工作建立在研究者之前对连续和混合领域的形式方法的工作基础上，以实现实际工程中符号和数值方法的统一。通过学习纠正的方法可以确保通用的基于学习的决策算法在所有人工智能应用领域的安全性和可信度的形式化属性。教育和推广活动是项目的关键部分，因为所开发的方法只有在广泛的工程领域中被新一代自主系统开发人员采用时才有用。教育工作直接有助于在实际工程中提高形式化方法的自动化和可用性。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Computing systems that engage people physically with high degrees of autonomy need to provide rigorous guarantees of safety. Formal methods can been used on such systems to provide mathematical proofs to ensure correct behavior. However, machine learning and data-driven approaches are now an indispensable part of autonomous-systems design, and their reliance on highly nonlinear continuous functions and probabilistic reasoning has largely been at odds with the logical and symbolic-analysis frameworks in formal methods. As a result, the lack of formal assurance has become the key bottleneck that impedes the wider deployment and adoption of autonomous systems. This project targets this open challenge by developing formal synthesis and verification techniques for learning-based and data-driven control and planning methods for autonomous systems. The project develops the theoretical foundations as well as practical techniques and tools for improving the fundamental reliability of realistic autonomous systems such as autonomous cars and unmanned aerial vehicles. The work builds on the investigator's prior work on formal methods over continuous and hybrid domains towards the unification of symbolic and numerical methods in practical engineering. The correct-by-learning methods can ensure formal properties of general learning-based decision-making algorithms towards safety and trustworthiness in all areas of AI applications. The education and outreach activities are a crucial part of the project, as the methods developed are only useful if they are adopted by the new generations of developers of autonomous systems in a broad range of engineering domains. The education efforts contribute directly to improving automation and usability of formal methods in practical engineering.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.