两位教授授予AI种子赠款，以推进代数证明系统

人工智能是否可以允许计算机确保安全的自主系统并提高优化？两位普林斯顿教授认为这可以，他们今年早些时候获得了一项研究赠款，以探索用于确保复杂技术安全和效率的数学证明系统的AI增强。

运营研究与金融工程教授Amir Ali Ahmadi和计算机科学教授Pravesh Kothari于2月获得了普林斯顿AI实验室种子赠款，其研究项目与工程应用程序有关。

这项协作努力的目的是利用特定于应用程序的数据以及AI工具来扩展基于半程编程的代数证明系统。半决赛编程是一种强大的方法，用于解决复杂的优化问题 - 尤其是那些涉及不确定性或安全性的方法，对于常规算法而言通常太复杂了。这些证明系统有助于严格确认某些数学条件是否成立，这对于无法选择失败的工程应用至关重要。

他们的工作将重点放在关键应用程序上，包括对机器人系统的安全验证，在几何形状中证明的自动化定理以及算法鲁棒统计。安全验证涉及证明，像无人机或自动驾驶汽车这样的系统始终在任何条件下都可以安全地行为。自动定理证明使用计算机在逻辑上证明了数学语句，并且稳健的统计信息涉及以一种被异常值或错误误导的方式分析数据。

艾哈迈迪告诉《每日普林斯顿学》，这项合作已经有一段时间了。我们正在从理论计算机科学方面和我的优化和控制方面进行正方形优化的总和[kothari]。

正方形（SOS）优化的总和是一种尖端的数学技术，它允许研究人员验证由多项式方程所控制的系统的行为。从本质上讲，它有助于证明某些结果是不可能的还是保证的，这在机器人技术和控制理论之类的领域尤其重要，必须在数学上确保安全性。例如，为了确保自动驾驶汽车避免障碍，可以使用SOS来证明车辆路径永远不会与其环境中的任何物体相交。

尽管具有理论上的力量，SOS经常遇到计算限制，因为它依赖于半决赛编程，这在较大的尺度上往往变得棘手。在这种情况下，棘手意味着计算变得如此大而复杂，以至于甚至强大的计算机在合理的时间内也要努力或无法完成它们。这是机器学习进入方程式的地方：艾哈迈迪（Ahmadi）和科萨里（Kothari）正在使用经过过去数据训练的AI工具，以帮助指导和加快找到这些数学证明的过程。

`如果我已经有一个不可行的多项式系统及其代数证明的数据集，那么我可以用它来捷达下一个证明吗？”艾哈迈迪问。换句话说，如果该系统以前遇到的问题被证明没有解决方案，那么AI可以从这些示例中学习以更快地识别或排除将来类似问题的问题吗？这是我们指导未来计算的愿景。

尽管赠款资金相对谦虚，但艾哈迈迪指出，它仍然刺激了该项目。工程和应用科学创新基金的额外支持将使团队能够参与更多的学生并为该项目奠定基础。

该团队应对的第一个项目涉及解释SOS算法以查找图形的着色数。简而言之，他们想找到为网络的节点（或点）上色所需的最小颜色数量，以使连接的节点不共享相同的颜色。

艾哈迈迪解释说，这个问题有很多应用。例如，如果图表的节点代表普林斯顿的课程，而边缘代表这些课程中的冲突（它们同时相遇），则着色编号正是举办所有课程所需的无需冲突所需的教室数量。”

艾哈迈迪继续使用第二，更轻松的应用。•如果相同的节点代表您的婚礼上的客人，而边缘代表人际冲突（可以互相站立的客人），那么着色编号对应于确保无戏剧婚礼所需的最少餐桌数量！

就像许多基于神经网络的AI工具一样，它是效果很好的黑匣子的系统，但很容易揭示它们如何到达特定答案 - SOS算法很强大，但也可能是神秘的。” 

``对于机器学习社区而言，人们越来越感兴趣地用更可解释的模型代替它们。我们的目标是了解这些算法如何解决困难的组合问题，目前没有其他更可解释的算法。

从长远来看，艾哈迈迪（Ahmadi）和科萨里（Kothari）希望他们的工作将为人工智能中最雄心勃勃的边界之一做出贡献：自动化数学推理。

艾哈迈迪说，该项目的重大目标之一是自动化的。”艾哈迈迪说。机器实际上可以自行证明深度，不平凡的定理吗？这是一个巨大的挑战，广场优化的总和为我们提供了一条结构化的道路。

他补充说，这是一项深刻的跨学科努力。而且它才刚刚开始。

亚当·穆萨（Adam Moussa）是王子的贡献者。

请将任何更正发送给校正[at DailyPrincetonian.com。