企业想把AI用到实处，最难的不是让模型”说出话”，而是让说出来的话靠谱。税务、法律、药物研发——这些领域错一个字就是真金白银甚至人命，AI幻觉在这儿比别处更致命。一家刚冒头的新公司觉得，解决这个问题靠的不是把模型做得更大，而是把规则写得更死。
给AI套上数学的缰绳
Pramaana Labs本周冒了出来，拿了Kholla Ventures领投的2700万美元种子轮，Accel、Boldcap、Nexus Venture Partners、Premji Invest和Unbound跟投。这家公司的主意说起来不复杂：用计算机科学里最”死板”的工具——数学形式化验证——来管住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的判断是，那些规则本来就在那儿，只是没人把它们变成代码而已。