随着企业努力将人工智能试点项目转化为业务的实际组成部分，可靠性问题日益成为关注焦点。一家新兴初创公司希望通过借助数学形式化工具，结合计算机科学中最可靠的系统与最复杂的技术，来解决这一难题。

周三，Pramaana Labs宣布完成2700万美元的种子轮融资，领投方为Khosla Ventures，Accel、BoldCap、Nexus Venture Partners、Premji Invest和Unbound等机构也参与了本轮融资。

Pramaana Labs将重点关注法律、药物研发和税务筹划等高度敏感的领域——这些领域中错误代价高昂，对可靠性的要求极高。在这些系统中部署人工智能，需要比现有技术更强的防止幻觉和错误的保护措施。正如Pramaana联合创始人兼CEO Ranjan Rajagopalan所说，这些领域也非常适合形式化验证。

Rajagopalan向TechCrunch解释道：“这就像数学一样，你必须遵守许多规则。”他以税法为例，“一旦规则被编码，基于这些规则的推理就会变得确定无疑。”

Pramaana的系统仍然基于传统的大型语言模型（LLM），这赋予它回答自然语言问题和解决传统计算机难以处理的复杂问题的灵活性。但在LLM之上，增加了一层确定性验证，确保LLM的输出结果准确无误。

这种将LLM引擎与确定性验证相结合的方案已较为流行；而Pramaana的独特之处在于采用形式化验证工具，借助开源的LEAN编程语言来验证数学证明。Rajagopalan提到，这方面已有成熟的先例，例如法国的CATALA项目，该项目将国家税收和福利系统形式化为可执行代码。

针对每个应用场景，Pramaana都会构建自己的LEAN风格形式化验证系统，并由领域专家监督。在税法领域，公司与前美国国税局局长Danny Werfel合作；而在网络安全和药物研发领域，则由印度理工学院德里分校、印度理工学院马德拉斯分校和加州大学伯克利分校的教授们负责监督。

Rajagopalan表示：“世界上最难的问题并非无解，而是尚未被形式化。任何一个错误可能危及健康、财产或自由的领域，都有其明确的规则。”

现在，这些规则只需被编码实现即可。