Pramaana Labs获2700万美元融资，将形式化验证引入AI

AI

在企业努力将AI试点项目转化为实际业务的过程中，可靠性问题已成为核心挑战。一家新兴创业公司希望借助数学形式化工具来解决这一难题，将计算机科学中最可靠的系统与最不可预测的系统相结合。

近日，Pramaana Labs宣布完成2700万美元种子轮融资，由Khosla Ventures领投，Accel、Boldcap、Nexus Venture Partners、Premji Invest和Unbound跟投。

Pramaana将重点布局法律、药物研发和税务申报等高敏感性垂直领域——这些领域对错误零容忍，可靠性要求极高。在这类系统中部署AI，需要比现有方案更强大的幻觉与错误防护机制。而在Pramaana联合创始人兼CEO Ranjan Rajagopalan看来，这些领域也天然适合形式化处理。

"从某种程度上说，这就像数学——你必须遵守大量规则，"Rajagopalan在描述税法规则时表示，"一旦将其编码化，在此基础上进行推理就会变得可预测。"

Pramaana的系统仍以传统大语言模型为核心引擎，保留了回答自然语言问题、处理传统计算机难以应对的复杂问题的能力。但在大语言模型之上，还叠加了一个确定性验证层，用于校验大语言模型的输出结果。

将大语言模型与确定性验证相结合是一种主流思路，而Pramaana的独特之处在于采用了形式化验证工具——借助用于验证数学证明的开源LEAN编程语言。这一方向已有现实先例可循：Rajagopalan提到了法国的CATALA项目，该项目将法国大量税收和福利制度规则编译为可执行代码。

针对每个具体应用场景，Pramaana都会构建专属的LEAN式形式化验证系统，并由各领域专家负责监督。在税法领域，公司与前美国国税局局长Danny Werfel展开合作；网络安全和药物研发系统则由来自IIT德里、IIT马德拉斯和加州大学伯克利分校的教授团队提供学术支持。

"世界上最难的问题并非无解，而是缺乏形式化表达，"Rajagopalan说，"每一个'出错就意味着损害健康、财产或自由'的领域，都有其规则存在。"

而现在，这些规则只需要被系统地编码化。

Q&A

Q1：Pramaana Labs的AI系统是如何保障准确性的？

A：Pramaana的系统以传统大语言模型为核心引擎，同时在其上叠加了一个确定性验证层。这个验证层基于开源LEAN编程语言构建，借鉴了数学证明领域的形式化验证方法，能够对大语言模型的输出结果进行校验，从而有效减少幻觉和错误，提升系统在高敏感场景下的可靠性。

Q2：Pramaana Labs主要针对哪些行业？

A：Pramaana重点布局法律、药物研发和税务申报等高敏感性垂直领域。这些行业对错误零容忍，可靠性要求极高，一旦出错可能危及用户的健康、财产或法律权益。公司在税法领域与前美国国税局局长合作，在网络安全和药物研发领域则引入了多所顶尖高校教授团队提供专业监督。

Q3：形式化验证技术在AI领域有没有现实先例？

A：有。Pramaana Labs的CEO Ranjan Rajagopalan提到了法国的CATALA项目作为参考先例。该项目将法国大量税收和社会福利制度的规则编译为可执行代码，实现了对复杂法规的形式化处理，证明了将规则体系编码化并用于AI推理的可行性。