一句话定义：可证明推理（Provable AI 词典：Inference">Inference）指模型在给出结论的同时，附上一份能被独立的小程序机械校验的凭证，比如证明、证书或反例；只有校验通过，结论才算成立。
原理：生成很贵，校验很便宜
打个比方，数学考试有三种判分方式。第一种只对答案；第二种老师翻草稿纸，看步骤写得像不像；第三种要求交卷时附一份能被验算器逐行核对的证明。验算器不懂数学直觉，但每一步都能查，查完盖章通过。可证明推理要的是第三种。
它的技术支点是一个不对称：找出证明很难，验证证明很容易。所以系统通常分两个角色。大模型负责“猜”，比如猜定理证明、猜满足约束的可行解、猜一段带前置条件的代码；校验器负责“判”，比如证明助手的内核（如 Lean、Coq）、SAT/SMT 求解器的证明检查器、类型检查器，或者几十行断言脚本。猜错就重来，猜对就留下凭证。工程上这条路有先例：proof-carrying code（携带证明的代码）让程序出厂时自带安全证明，使用方只需运行一个很小的检查器。
它不是什么
下面几个概念经常被混为一谈，差别其实很大：
| 概念 | 检查对象 | 判断者 | 保证粒度 | 典型失效方式 |
|---|---|---|---|---|
| 事后评测 | 一批输出的统计正确率 | 测试集与指标 | 平均层面，不保单条 | 分布漂移、指标被“刷” |
| 推理链审计 | 模型写出的推理文本 | 人或模型评审 | 单条，但靠主观判断 | 推理链不忠实，写得像对的 |
| 形式化验证 | 系统本身的性质 | 证明助手内核 | 对该性质全局成立 | 规约写错，建模与实现不符 |
| 可证明推理 | 某一次推理的结论 | 小型校验器 | 单条结论，逐例 | 命题无法形式化、证明生成失败 |
一句话记：推理链是草稿纸，不是证书；形式化验证审的是“系统”，可证明推理审的是“这一次的答案”。
三道坎，别高估
一是规约（specification）。校验器只认形式化命题。“这段代码不会数组越界”能验，“这段文案是否得体”不能验。把真实需求翻译成形式规约往往比找证明还难，也最容易出错。规约写歪了，证明再漂亮也等于白验。
二是覆盖面。数学证明、约束求解、带规格的代码、可核对的查询与计划，这些天生有校验器；开放写作、战略判断、审美取舍，目前没有。
三是信任基。凭证的可信上限等于校验器本身：内核有 bug、公理用错，整条链就失效了。所以校验器必须小而透明。
对你的实际意义
做系统的人，把“能不能验”提前当成设计约束：凡是可以写出检查器的任务，就值得做成“生成—校验—重试”的闭环，而不是事后抽检。对外表述也要分清：“模型说它自己检查过”是自证，“另一个程序独立验过”才是他证。
普通职场人可以用一句话筛方案：这份输出，除了模型自己，还有别的东西能判对错吗？答不上来的，那还是评测，不是证明。