随着企业努力将人工智能试点项目转变为其业务的功能性部分，可靠性已成为中心议题。一家初创公司希望通过借助数学形式化的工具来解决这个问题，将计算机科学最可靠的系统与其最混乱的系统结合起来。周三，Pramaana Labs宣布获得由Khosla Ventures牵头的2700万美元种子融资，Accel、Boldcap、Nexus Venture Partners、Premji Invest和Unbound也参与了投资。Pramaana将专注于法律、药物发现和税务准备等高度敏感的垂直领域——在这些领域，错误可能代价高昂，可靠性至关重要。在这些系统中部署人工智能需要比我们目前拥有的更强的防护措施以防止幻觉和错误。但正如Pramaana的联合创始人兼首席执行官Ranjan Rajagopalan所见，他们也特别适合形式化。“就像数学一样，你需要遵循许多规则，”Rajagopalan在向TechCrunch描述税法的规则时表示。“一旦你有了一个编码版本，基于它的推理就会变得确定性。”Pramaana的系统仍然依赖传统的LLM，这使其能够灵活回答自然语言问题并解决传统计算机无法处理的复杂问题。但在这个LLM之上有一个确定性层，确保LLM的工作得到验证。这种LLM引擎与确定性验证的结合是一种流行的设置；Pramaana独特的方法是使用形式验证的工具——借助用于验证数学证明的开源LEAN编程语言。有很多此类工作的真实先例；Rajagopalan提到法国的CATALA项目，该项目将该国的税收和福利系统形式化为可执行代码。对于每个用例，Pramaana将建立自己的LEAN风格的形式验证系统，由领域专家监督。对于税法，该公司正在与前国税局局长Danny Werfel合作，而来自德里理工学院、马德拉斯理工学院和加州大学伯克利分校的教授则负责网络安全和药物发现系统。“世界上最难的问题不是不可解决的，而是没有形式化的，”Rajagopalan说。“在每个错误可能使人失去健康、金钱或自由的领域，都有规则。”现在，这些规则只需要被编码。当你通过我们文章中的链接购买时，我们可能会赚取少量佣金。这不会影响我们的编辑独立性。Russell Brandom自2012年以来一直在关注科技行业，重点关注平台政策和新兴技术。他曾在The Verge和Rest of World工作，并为Wired、The Awl和MIT的Technology Review撰稿。他可以通过邮箱russell.brandom@techcrunch.com或在Signal上拨打412-401-5489联系。查看个人资料