用形式化验证压制幻觉
devanshmehta · x · 2026-07-11
有人介绍了 **PramaanaLabs**：这家公司在尝试用**形式化验证**来减少 AI 幻觉。 ### 核心思路 - 现在大模型的价值之一，是先给出答案，再由人来验证。 - PramaanaLabs 想进一步去掉“人工核验”这一步，把用户需求转成一种名为 **lean** 的编程语言。 - 这种语言由编译器自动拒绝不满足数学规格的输出，从机制上防止错误答案通过。 ### 关注场景 作者提到他们当前重点面向： - 税务申报 - 法律案件 - 医疗健康 这些场景里，哪怕一次幻觉都可能造成严重后果。作者还猜测，这家公司未来可能会转向“把旧代码迁移成可形式化验证语言”的方向。