### [这家公司想用数学证明来管住AI的幻觉，2700万美元押一条没人走的路](https://www.willai.cc/article/2008)

**Published:** 2026-06-17T15:21:29

**Author:** hiyoho

**Excerpt:** 企业想把AI用到实处，最难的不是让模型”说出话”，而是让说出来的话靠谱。税务、法律、药物研发——这些领域错一个字就是真金白银甚至人命，AI幻觉在这儿比别处更致命。一家刚冒头的新公司觉得，解决这个问题靠的不是把模型做得更大，而是把规则写得更死

企业想把AI用到实处，最难的不是让模型”说出话”，而是让说出来的话靠谱。税务、法律、药物研发——这些领域错一个字就是真金白银甚至人命，AI幻觉在这儿比别处更致命。一家刚冒头的新公司觉得，解决这个问题靠的不是把模型做得更大，而是把规则写得更死。

### 给AI套上数学的缰绳

Pramaana Labs本周冒了出来，拿了Kholla Ventures领投的2700万美元种子轮，Accel、Boldcap、Nexus Venture Partners、Premji Invest和Unbound跟投。这家公司的主意说起来不复杂：用计算机科学里最”死板”的工具——数学形式化验证——来管住AI最”飘”的那部分幻觉和乱编。

![AI形式化验证概念图](https://admin.hiyoho.com/wp-content/uploads/2026/06/ai-formal-verification.png)

形式化验证让AI的推理过程变得可验证 | 配图来源：WorkBuddy AI生成

CEO Ranjan Rajagopalan的说法是：税务法规本质上就是一套规则，跟数学差不多。一旦把规则用代码形式化，推理过程就能变成确定性的——换句话说，AI可以天马行空地理解自然语言，但最后得出来的结论必须过一道”数学检查”，否则不让出门。

> “世界上最难的问题不是无解，而是没有被形式化。每个’出错就要命’的领域——健康、金钱、自由——都有规则，只是这些规则还没被写成代码。”  
> ——Ranjan Rajagopalan，Pramaana Labs联合创始人兼CEO

### LEAN语言来了

Pramaana的做法是在常规LLM上面加一层确定性验证，这套验证用的是开源LEAN编程语言的工具——本来这东西是用来验证数学证明的，现在被他们拿来验证AI的输出。有法国民俗，法国的CATALA项目已经把本国税法和福利系统的一大块形式化成了可执行代码，算是这条路上有分量的先驱。

每个使用场景，Pramaana会搭一套自己的类LEAN形式化验证系统，并且有领域专家盯着。税务方向的前IRS局长Danny Werfel在公司顾问名单上；网络安全与药物研发系统则由IIT Delhi、IIT Madras和UC Berkeley的教授们把关。

### 为什么是现在

AI可靠性这事儿，搁两年前大家还在实验室里吵，现在企业已经被迫要认真对待了。幻觉在闲聊里是个笑话，在报税软件里就是一个灾难。Pramaana挑的这几个垂直领域——法律、药物研发、税务——恰恰是容错率最低的几个地方，也是愿意为”可靠性”付钱的地方。

这条路能不能走通，取决于一件事：把现实世界的复杂规则完整、准确地形式化，这件事本身难度就不比做AI小。但Rajagopalan的判断是，那些规则本来就在那儿，只是没人把它们变成代码而已。

* * *

📎 原文来源：[Pramaana Labs raises $27M seed round from Khosla Ventures to bring formal verification to AI — TechCrunch](https://techcrunch.com/2026/06/17/pramaana-labs-raises-27-million-seed-round-from-khosla-ventures-to-bring-formal-verification-to-ai/)

**Tags:** AI, AI创业, AI安全, AI技术

**Categories:** AI资讯

---