随着企业努力将AI试点项目转化为实际业务功能，可靠性已成为核心关注点。一家新创公司希望通过运用数学形式化工具来解决这一问题，将计算机科学中最可靠的系统之一与最不可预测的系统之一结合起来。
本周三，Pramaana Labs宣布获得由Khosla Ventures领投的2700万美元种子轮融资，Accel、BoldCap、Nexus Venture Partners、Premji Invest和Unbound也参与了此次投资。
Pramaana将专注于法律、药物发现和税务准备等高度敏感领域——在这些领域中，错误可能带来高昂代价，可靠性至关重要。在这些系统中部署AI将需要比现有技术更强的防幻觉和防错能力。但Pramaana联合创始人兼CEO Ranjan Rajagopalan认为，这些领域也特别适合形式化验证。
Rajagopalan向TechCrunch解释税法规则时表示："这类似于数学，你需要遵守很多规则。一旦你有了规范化的版本，基于它的推理就会开始变得确定性。"
Pramaana的系统仍然基于传统大型语言模型(LLM)运行，这使其能够灵活地回答自然语言问题并解决传统计算机无法处理的复杂问题。但在该LLM之上还有一个确定性验证层，确保LLM的工作结果经过验证。
将LLM引擎与确定性验证相结合是一种流行的架构；Pramaana的独特方法是使用形式化验证工具——借鉴用于验证数学证明的开源LEAN编程语言。这项工作有实际先例；Rajagopalan提到了法国的CATALA项目，该项目将该国大部分税务和福利系统形式化为可执行代码。
针对每个应用场景，Pramaana将构建自己的LEAN风格形式化验证系统，并由领域专家监督。在税法领域，该公司与前美国国税局局长Danny Werfel合作；而在网络安全和药物发现系统方面，则由印度理工学院德里分校(IIT Delhi)、印度理工学院马德拉斯分校(IIT Madras)和加州大学伯克利分校(UC Berkeley)的教授们负责监督。
Rajagopalan表示："世界上最难的问题并非无法解决，而是尚未形式化。在每个错误可能导致人们失去健康、金钱或自由的领域，都存在规则。"
现在，这些规则只需要被形式化编码即可。
【全文结束】