Building a Frontier AI Verification Lab 深度访谈

节目开头以若干关键问题预告 Pramaana Labs 的核心主张，包括为何称其为前沿实验室、LLM 与其技术路线的差异，以及税务、法律、医疗等只有专家能判断的领域为何需要新型 AI。嘉宾用一句话概括使命：将所有人类知识形式化。随后主持人介绍三位创始人 Ranjan、Krishnan 和 Sanjay，并说明 BoldCap 从早期就参与支持该公司，访谈将围绕 Pramaana 正在建设的机会与技术展开。

主持人询问 Pramaana 为何被称为 Frontier Lab，以及它与一般创业公司的区别。嘉宾认为，实验室与普通创业公司的核心差异在于出发点：实验室更强调使命、终局状态和实现路径，而不是先从收入模型开始。他们把 Pramaana 的目标定义为把数学严谨性引入关键任务领域的 AI 输出，因为目前 AI 在这些场景中难以落地，主要原因是用户无法完全信任其答案，模型在被追问时也可能轻易改变立场。

嘉宾讨论 Pramaana 如何衡量自身进展。由于面向真实世界关键领域的基准并不充分，公司一方面与领域专家合作研究新基准，另一方面也使用数学、自动形式化和 Lean 证明等内部基准测试其证明能力。在税务等具体领域，他们关注 TaxCalc 类任务，即能否理解税法推理并产出税表或税务建议。Ranjan 进一步解释，Pramaana 先追求 precision，即只要回答就必须 100% 正确；recall 则是持续扩大可回答问题范围，最终目标是每个问题都能以 100% 准确率回答。

主持人要求比较 Pramaana 与 OpenAI、Anthropic 等前沿模型公司的技术栈差异。Sanjay 解释，主流 LLM 的训练方式是基于大规模文本、语音、图像或视频等符号数据，学习在上下文中预测下一个 token。它们本质上是概率模型，擅长通过统计分布压缩大量知识并生成最可能的续写。问题在于，这类模型受限于训练数据和统计分布，本身没有内建的正确与错误概念，也没有明确的规则或结构，因此在需要严格正确性的任务中存在局限。

嘉宾进一步说明 Pramaana 与 Harmonic、Axiom 等形式化验证公司不同：后者多从数学、软件、硬件和芯片验证开始，而 Pramaana 更关注数学尚未充分进入的领域，如税务、法律和医疗。他们用 Jim Simons 将交易从直觉游戏转化为数学问题的例子，说明数学能够显著提升信任水平。嘉宾认为，医疗诊断、法律判断和税务政策并非纯直觉活动，而是依赖知识库、测试、假设、反事实分析和符号推理；在人类不能犯错的关键领域，人类本就发明了结构化推理来获得严谨性。

主持人要求用简单语言解释形式化验证。Ranjan 将其类比为高中数学证明：过去人们写出推导后交给另一个人检查逻辑是否一致，而形式化验证则是把证明交给编译器，由机器检查正确性。它最早广泛用于芯片设计，因为芯片错误可能造成巨大经济损失。Lean 等系统则把数学知识编码为机器可检查的形式，使证明一旦通过编译，就不再需要另一个人来重新确认其正确性。

Krishnan 用软件工程中的单元测试解释形式化验证的价值。单元测试只能验证特定输入样例，而无法穷尽无限多的输入；形式化验证则可以证明代码对所有可能输入都满足某种属性，例如排序算法对任何输入都会输出有序结果。随后主持人提出批评意见：形式化验证不易扩展、耗时、昂贵、证明很长。嘉宾承认历史上确实如此，甚至十行函数的证明可能长达数百行，这也是软件行业长期依赖单元测试的原因。但 LLM 正在降低写规范和生成证明的成本，使形式化验证变得更现实。

嘉宾补充说，过去人们信任软件或证明，主要是因为它们由人类编写并承担判断责任；而当 AI 生成代码、证明或专业建议时，责任边界变得不清晰。因此，他认为形式化验证将成为信任 LLM 输出的必要条件。代码至少还有编译和单元测试，其他领域几乎没有类似保障。随着 AI 在各行业采用度快速提升，它可能足够聪明，以至于让最聪明的人也相信错误答案是正确的。要防止这种情况，嘉宾认为只能依赖形式化验证，尤其是在安全、法律、税务和航空等关键场景。