2018年7月16日亚马逊杰出科学家拜伦·库克在牛津大学联合逻辑会议上发表主题演讲这是一个自1996年以来每四年举办一次的计算机逻辑聚会。在演讲中库克描述了他的团队如何使用名为cvc合作有效性检查器的开源软件工具来识别代码中的逻辑问题并修复它们。坐在台下的斯坦福大学教授克拉克·巴雷特已经在cvc项目上工作了近20年。Cvc被开发用于分析编码为可满足性模理论问题的验证问题。SMT是形式化方法的支柱即使用自动推理来证明程序或系统将按预期运行。通过大规模应用SMTcvc可以检测代码和系统中的逻辑错误比如用于身份验证和访问管理的系统。我有点震惊真的很兴奋巴雷特说。这真正开始于一个令人兴奋的时刻意识到嘿我们的工作正在被亚马逊使用。库克和巴雷特的邂逅最终促成了一项持续多年的研究合作最终巴雷特在2023年成为亚马逊学者。最初亚马逊通过亚马逊研究奖项目向巴雷特在斯坦福工程学院的实验室提供小额资助随着研究的进展这些资助逐步增长为更大的资金承诺。这项资助支持的基础研究加上两个团队之间的深度技术合作使得cvc5的开发成为可能这是该开源软件的最新版本。Cvc5为亚马逊客户和更广泛的行业都提供了重大价值同时推进了学术研究。举例来说cvc5被用于自动推理检查这是亚马逊Bedrock的一个新功能用于根据组织政策验证自然语言内容。它为访问策略分析工具提供动力包括身份和访问管理访问分析器这是一项帮助客户安全管理AWS资源访问的服务。最近亚马逊开始在Kiro中部署cvc5进行规范分析和测试生成Kiro是一个新的智能体开发环境。在这些应用中cvc5现在每天处理约10亿次求解器调用为AWS客户增强了安全性、可靠性和持久性。与巴雷特共同参与该项目的是AWS的高级首席应用科学家罗伯特·琼斯他们两人在斯坦福大学读博士时师从同一位导师。多年来还有许多渴望测试自己技能的学生和博士后参与了该项目。其中不少人后来加入了亚马逊开发新的实现和应用延续了他们作为学生研究者时开始的工作。真正有趣的是比如刚完成博士学位的人经常为长期存在的研究挑战带来新的见解因为他们以不同的方式思考这些问题琼斯说。我发现协作最好的部分是不同的人倾向于为同一个问题构建不同的心理模型。当这些模型结合在一起时你经常对如何思考问题或如何将其映射到你已经知道如何解决的不同问题有新的见解。学术研究和商业资助的成功结合可以产生巨大影响但正如巴雷特指出的需要专注于可实现的目标。巴雷特说很容易陷入一个有趣的项目想法但最终导致实际的死胡同。如果你在象牙塔里构建你的工具而你无法接触到真正的问题很容易构建错误的工具。我实际上犯过这个错误他说。你造了一把锤子然后四处寻找钉子但找不到任何合适的东西。你对某种特定方法感到兴奋但没有考虑这种方法可能适用于什么。所以我现在更喜欢相反的方式我去找一个真正的问题然后退一步说我们实际上可以使用什么方法来解决这个问题当你改变代码时他说80%的时间它会做得更好20%的时间它会做得更差。在某些情况下这实际上不是那么好。他补充说将精华与糟粕分开对于产生强大和可扩展的代码至关重要需要大规模测试来发现和修复在代码更改时可能无意中引入的问题。琼斯说在这个级别分析交互需要多个头脑人越多越好。古话人多力量大在混合公共研究和实际应用时特别有用。我真的喜欢处理需要多人解决的难题。我享受科学中涉及的协作他说。我一直发现多个头脑一起解决同一个问题比一个人更好。巴雷特和琼斯都同意使这项工作成功的是愿意从学术和商业两个角度来看待问题。有时纯研究目标可能有非常有益的结果有时则不然但将这两种方法融合在一起来解决严重问题可以带来巨大的好处。两人都同意沟通是关键。学术界的难题之一是知道哪些问题最重要以及这些问题如何影响行业中遇到的现实问题琼斯说。能够更开放地讨论我们正在努力解决的问题类型以及克拉克告诉我们他的研究议程这对我们双方都有帮助。它使亚马逊能够指出感兴趣的领域并帮助克拉克理解我们在实践中尝试应用这些工具和技术时每天遇到的具体问题。QAQ1cvc5是什么软件它在亚马逊有什么用途Acvc5是一个开源软件工具用于识别和修复代码中的逻辑问题。在亚马逊它被用于自动推理检查、身份和访问管理分析器以及智能体开发环境Kiro中每天处理约10亿次求解器调用为AWS客户提供安全性、可靠性和持久性保障。Q2学术界和工业界合作研发软件有什么好处A学术界和工业界合作可以结合理论研究和实际应用需求。学术界提供新颖的理论见解和研究方法而工业界提供真实的问题场景和大规模测试环境。这种合作避免了纯学术研究可能脱离实际的问题确保研发的工具能够解决真正的业务需求。Q3为什么说沟通在学术产业合作中很重要A沟通帮助学术界了解哪些问题在工业界最重要以及研究成果如何影响现实应用。同时工业界可以向学术界说明他们面临的具体技术挑战学术界则可以分享研究议程。这种双向沟通使合作更加有效确保研究方向与实际需求对接。