Pramaana Labs 从 Khosla Ventures 获得 2700 万美元种子轮融资，将形式化验证引入 AI

# Pramaana Labs 获 Khosla Ventures 领投 2700 万美元种子轮融资，将形式验证引入 AI | TechCrunch 来源：https://techcrunch.com/2026/06/17/pramaana-labs-raises-27-million-seed-round-from-khosla-ventures-to-bring-formal-verification-to-ai/ 随着企业努力将 AI 试点项目转化为业务中可正常运作的部分，可靠性已成为核心焦点。一家新初创公司希望通过借助数学形式化的工具来解决这个问题，将计算机科学中最可靠的系统之一与最混乱的系统之一结合起来。 周三，Pramaana Labs (https://pramaanalabs.ai/) 宣布获得 2700 万美元的种子轮融资，由 Khosla Ventures 领投，Accel、Boldcap、Nexus Venture Partners、Premji Invest 和 Unbound 参投。 Pramaana 将聚焦于法律、药物发现和税务准备等高度敏感的垂直领域——在这些领域，错误代价高昂，可靠性尤为珍贵。在这些系统中部署 AI，需要比当前更强大的防幻觉和防错误保护。但在 Pramaana 联合创始人兼 CEO Ranjan Rajagopalan 看来，这些领域也特别适合形式化。 “从某种意义上说，这就像数学：你需要遵守很多规则，”Rajagopalan 在描述税法规则时告诉 TechCrunch。“一旦你有了一个编码化的版本，基于它的推理就会开始变得确定。” Pramaana 的系统仍然运行在传统的 LLM 上，从而保留了回答自然语言问题和处理传统计算机无法解决的复杂问题的灵活性。但在 LLM 之上增加了一个确定性层，确保 LLM 的输出是经过验证的。 这种 LLM 引擎与确定性验证相结合的方式是一种流行的配置 (https://techcrunch.com/2026/06/16/probably-raises-9m-to-build-a-more-reliable-kind-of-ai/)；Pramaana 的独特之处在于使用形式验证的工具——借鉴用于验证数学证明的开源 LEAN 编程语言。这项工作有不少真实先例；Rajagopalan 提到了法国的 CATALA 项目 (https://www.inria.fr/en/catala-software-dgfip-cnaf)，该项目将法国大部分税收和福利系统形式化为可执行代码。 针对每个用例，Pramaana 将构建自己基于 LEAN 风格的形式验证系统，并由领域专家监督。在税法领域，公司正与前任 IRS 专员 Danny Werfel 合作，而网络安全和药物发现系统则由来自印度理工学院德里分校、马德拉斯分校以及加州大学伯克利分校的教授们监督。 “世界上最难的问题并非无解，而是未被形式化，”Rajagopalan 表示。“每个因犯错而可能让患者付出健康、金钱或自由代价的领域，都有其规则。” 现在，这些规则只需要被编码化。 *当您通过我们文章中的链接购买商品时，我们可能会获得少量佣金 (https://techcrunch.com/techcrunch-affiliate-monetization-standards/)。这不会影响我们的编辑独立性。* Russell Brandom 自 2012 年起一直报道科技行业，重点关注平台政策和新兴技术。他此前任职于 The Verge 和 Rest of World，并为 Wired、The Awl 和 MIT Technology Review 撰稿。可通过 [email protected] 或 Signal (412-401-5489) 联系他。 查看简历 (https://techcrunch.com/author/russell-brandom/)