近日，美国AI初创公司Theorem宣布，已完成600万美元种子轮融资，用于开发验证人工智能生成软件正确性的自动化工具。
GitHub 、亚马逊和谷歌等公司的AI编码助手每年生成数十亿行代码，企业采用速度正在加快。
然而，验证AI编写的软件是否真正按预期运行的能力却未能跟上步伐，这造成了日益扩大的“监管缺口”，威胁着从金融系统到电网等关键基础设施。
Theorem 是一款面向关键任务软件的AI编码集成开发环境 (IDE)。以往，程序验证工作非常耗费人力，需要博士级别的工程师花费数年时间进行研究。
创始人格罗斯在创立Theorem之前，他曾在麻省理工学院攻读博士学位，研究经过验证的密码学代码，这些代码如今为 HTTPS 安全协议提供支持，每天保护着数万亿个互联网连接。Theorem 的核心技术结合了形式化验证（一种证明软件行为完全符合规范的数学技术）和经过训练可自动生成和检查证明的 AI 模型。该方法将以往需要数年博士级工程技术才能完成的流程，缩短至该公司声称可在数周甚至数天内完成。
在最近名为SFBench的技术演示中，Theorem 利用人工智能将1276个问题从 Rocq（一种形式化证明辅助工具）翻译成 Lean（另一种验证语言），然后自动证明每个翻译版本与原始版本等效。该公司估计，如果由人工团队完成同样的工作，大约需要2.7人年。
这家初创公司已经开始与人工智能研究实验室、电子设计自动化和GPU加速计算领域的客户开展合作。
一个案例研究说明了这项技术的实际价值。一位客户带着一份长达1500页的 PDF规格说明和一套饱受内存泄漏、崩溃和其他难以发现的bug困扰的旧软件实现找到了Theorem。他们最迫切的问题是：在不引入额外错误的前提下，将性能从每秒 10 兆比特提升到每秒 1 吉比特——提升 100 倍。
Theorem的系统生成了16000行生产代码，客户在未进行任何人工审查的情况下就部署了这些代码。这种信心源于一个简洁的可执行规范——仅几百行代码就概括了庞大的PDF文档——以及一个等效性检查工具，该工具验证了新实现与预期行为的一致性。
这家初创公司的出现预示着企业技术领导者评估人工智能编码工具的方式可能需要发生转变。第一波人工智能辅助开发浪潮承诺提高生产力——编写更多代码，速度更快。而Theroem公司则押注下一波浪潮将提出不同的要求：需要用数学证明速度的提升不会以牺牲安全性为代价。
如果觉得不错，随手点个赞、在看、转发三连吧
>作者：沙龙AI
>投稿、爆料邮箱：120208558@qq.com
