6.8
深览指数
科技TechCrunch·Russell Brandom··AI 生成
Pramaana Labs 获 Khosla Ventures 2700 万美元种子轮融资,将形式化验证引入 AI
AI 可靠性成为企业落地的核心挑战,Pramaana Labs 获 Khosla Ventures 领投的 2700 万美元种子轮融资,试图用形式化验证解决 LLM 幻觉问题。其独特方案是在常规 LLM 之上叠加一层基于开源 LEAN 语言的确定性验证引擎,优先应用于税务、法律、药物发现等高错误成本领域。公司已聘请前 IRS 专员 Danny Werfel 主导税法方向。文章的关键判断是:世界最棘手的问题并非不可解,而是尚未形式化。原文 ↗
核心观点
- ▍AI 可靠性问题的核心解决方案是将涉及严格规则的领域(税法、法律、药物发现)进行形式化编码,使 LLM 推理过程可被确定性验证。
- ▍世界最难的问题并非不可解,而是未被形式化——每个可能损害健康、金钱或自由的领域都存在一套可被编码的规则。
- 01Pramaana Labs 获得 2700 万美元种子轮融资,由 Khosla Ventures 领投,Accel、BoldCap、Nexus Venture Partners、Premji Invest 和 Unbound 参投。
- 02Pramaana 采用常规 LLM 引擎 + 确定性验证层的架构,使用开源 LEAN 编程语言(最初用于验证数学证明)来实现形式化验证。
- 03公司参考了法国 CATALA 项目,该项目已将法国大部分税收和福利系统形式化为可执行代码。
- 04Pramaana 为每个用例构建专属的 LEAN 风格形式化验证系统,由领域专家监督——前 IRS 专员 Danny Werfel 负责税法方向,来自 IIT Delhi、IIT Madras 和 UC Berkeley 的教授负责网络安全和药物发现方向。
- 05CEO Ranjan Rajagopalan 将税法描述为「像数学,有大量需遵守的规则;一旦实现编码化,基于其上的推理就变得确定。」
反方 / 局限
- — 形式化验证系统需要为每个垂直领域重新构建 LEAN 风格的验证框架,意味着 Pramaana 的扩展能力将严重受限于领域专家的可获取性和成本。
- — 文章未讨论形式化验证本身可能存在的局限性——即使是验证过的系统,其「确定性」也取决于底层规则编码是否正确,而税法、法律等领域的规则本身可能模糊或存在解释空间。
- — LLM + 确定性验证的组合方案在行业中已有多家初创公司尝试,差异化挑战较大;Pramaana 是否在领域知识壁垒上足够深、足够快,尚未充分论证。
Pramaana LabsKhosla VenturesAccelBoldCapNexus Venture PartnersPremji InvestUnboundLEAN (形式化验证语言)CATALA 项目Danny WerfelRanjan RajagopalanRussell Brandom
7 分钟 · 2 卡片 · 4 资料
读原文 →