可证明推理

可证明推理试图为模型输出提供形式化保证，而不仅是经验上的准确性。

当前可证明推理工作多走「局部形式化」路线：只对解码约束、输出格式、概率边界等可离散化或可解析的部分给出保证。

短期内，多数团队不会直接使用形式化证明工具，但相关思想会渗透到工程实践：更严格的输出校验、基于约束的解码、可审计的推理日志。