Pramaana 融资 2700 万美元做可验证 AI
TechCrunch AI··作者 Russell Brandom
关键信息
Pramaana 的系统底层仍使用常规 LLM 来处理自然语言和复杂推理，但其上层会加一个确定性验证层来检查结果是否成立。该公司表示，它借鉴了用于数学证明验证的 LEAN 编程语言，并计划在领域专家监督下，为不同场景分别构建验证系统，例如税务领域由前美国国税局局长 Danny Werfel 参与，网络安全和药物发现则有来自 IIT Delhi、IIT Madras 和 UC Berkeley 的学者把关。
资讯摘要
Pramaana Labs 在周三宣布完成 2700 万美元种子轮融资，由 Khosla Ventures 领投。此次融资还吸引了 Accel、BoldCap、Nexus Venture Partners、Premji Invest 和 Unbound 参与。该公司瞄准的是企业落地 AI 时最棘手的问题之一：试点阶段看起来有用，但一旦进入核心业务流程就不够可靠。Pramaana 的首批重点行业包括法律、药物发现和税务申报，因为这些领域一旦出错，代价可能非常高，甚至会造成伤害。联合创始人兼 CEO Ranjan Rajagopalan 认为，这些领域特别适合做形式化处理，因为它们本身就由大量规则组成。以税法为例，他把它类比为数学：只要规则被编码并写清楚，后续推理就可以变得更确定。
Pramaana 的技术路线是把常规 LLM 与一个确定性验证层结合起来，由后者检查前者的输出是否成立。公司并不是只依赖 LLM 自己回答，而是想借助形式化验证方法，这些方法受到用于数学证明验证的开源 LEAN 语言启发。Rajagopalan 还提到法国的 CATALA 项目，认为该项目把税收和福利制度形式化为可执行代码，说明这条路已有先例。Pramaana 表示，它会针对不同应用场景分别构建 LEAN 风格的验证系统，并由领域专家监督。税法方向由前美国国税局局长 Danny Werfel 参与，而网络安全和药物发现系统则由来自 IIT Delhi、IIT Madras 和 UC Berkeley 的教授负责监督。Rajagopalan 认为，世界上许多最难的问题并不是无法解决，而是尚未被形式化。
资讯正文
随着企业努力将 AI 试点项目转化为其业务中可正常运转的组成部分，可靠性已成为焦点。一家新的初创公司希望借助数学形式化工具来解决这一问题，把计算机科学中最可靠的系统之一与最混乱的系统之一结合起来。
周三，Pramaana Labs 宣布获得 2700 万美元种子轮融资，由 Khosla Ventures 领投，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 说。“每一个出错可能让某人付出健康、金钱或自由代价的领域，都有规则可循。”
而现在，这些规则只需要被编码出来。
来源与参考
收录于 2026-06-18