Pramaana Labs 获得 2700 万美元融资，旨在通过形式化验证解决 AI 可靠性问题

随着企业在将 AI 从实验性试点项目转向关键业务运营的过程中面临重重困难，整个行业正面临着一个巨大的障碍：可靠性。Pramaana Labs 旨在通过将形式化验证（formal verification）的数学严谨性应用于大语言模型（LLMs）不可预测的特性，来填补这一空白。

弥合概率性 AI 与确定性 AI 之间的鸿沟

现代 AI 的根本矛盾在于概率性推理与确定性真理之间的差异。虽然 LLMs 在处理自然语言和处理复杂的非结构化数据方面表现出色，但它们容易产生幻觉和逻辑错误。对于那些一旦出错就可能导致法律或财务灾难的行业来说，这些错误是无法接受的。

Pramaana Labs 正通过构建一种混合架构来解决这一问题。其系统利用传统的 LLM 引擎来保持自然语言交互所需的灵活性，但同时叠加了一个确定性验证层。该层确保 LLM 生成的输出遵循严格的、代码化的规则，有效地充当了防止错误的数学护栏。

利用 LEAN 实现高风险行业应用

与标准的软件测试不同，Pramaana Labs 正在利用形式化验证工具，特别是从开源编程语言 LEAN 中汲取灵感。LEAN 通常用于验证复杂的数学证明，而 Pramaana 计划调整这项技术，以将特定专业领域的“规则”代码化。

该公司瞄准了准确性不容置疑的高敏感垂直领域：

• 法律与税务准备： 使用复杂税法的代码化版本，以确保推理保持确定性。
• 药物研发： 对生物和化学数据应用严格的验证，以确保安全性和有效性。
• 网络安全： 实施形式化数学检查，以保障数字基础设施的安全。

为了确保这些系统立足于现实，Pramaana 正与顶尖领域专家展开合作。这包括为税务相关应用提供支持的前美国国税局（IRS）局长 Danny Werfel，以及来自德里理工学院（IIT Delhi）、马德拉斯理工学院（IIT Madras）和加州大学伯克利分校（UC Berkeley）的教授，负责监督网络安全和药物研发协议。

为什么这对 AI 生态系统至关重要

这笔由 Khosla Ventures 领投，Accel、Boldcap、Nexus Venture Partners、Premji Invest 和 Unbound 参投的 2700 万美元种子轮融资，标志着 AI 投资领域的巨大转变。生成式 AI “快速行动，打破常规”的时代正面临企业界“验证与校验”的需求。

通过将非形式化知识转化为可执行、可验证的代码（类似于法国的 CATALA 项目），Pramaana Labs 为 AI 如何在受监管行业中部署提供了蓝图。如果成功，这种方法将允许 AI 安全地管理人类健康、法律权利和庞大的金融系统，从而释放数万亿美元的价值。

核心要点

• 混合架构： Pramaana Labs 将 LLM 的灵活性与由 LEAN 式形式化验证驱动的确定性层相结合，以消除幻觉。
• 聚焦高风险领域： 该初创公司正优先考虑错误会导致严重后果的行业，包括法律、税务、药物研发和网络安全。
• 强大的机构支持： 由 Khosla Ventures 领投的 2700 万美元种子轮融资，凸显了市场对可验证且可靠的 AI 系统日益增长的需求。