立直麻将听牌集合最优编码的形式化验证

1. 问题背景：听牌集合为什么值得编码

立直麻将使用 34 种牌，每种牌在实体牌堆中有 4 张。牌的种类包括万子、筒子、索子三种花色，每种花色各有 1 到 9 共九个数牌，再加上 7 种字牌。若一副 13 张手牌 H 再加某一张牌 t 后，能够形成合法的 14 张和牌，则称 H 处于听牌状态，t 就是 H 的一张听牌。

听牌集合 W(H) 的定义可以写为：

W(H) = { t ∈ T : c_H(t) < 4 且 H ⊎ {t} ∈ G }

其中 c_H(t) 表示手牌 H 中牌 t 的张数，G 表示全部合法的 14 张和牌多重集合。这里要求 c_H(t) < 4，是为了避免加入第 5 张同类牌，从而超出实体牌数量限制。

和牌结构主要有三类：

1. 标准型：四个面子加一个雀头。面子可以是三张同种牌组成的刻子，也可以是同一花色内连续三张数牌组成的顺子；雀头是一对完全相同的牌。
2. 七对子：七种互不相同的对子。
3. 国士无双：由特定种类的幺九牌与字牌组成的特殊和牌型。

听牌集合的规模通常不大，但在组合上具有高度不规则性。对于牌效率分析、局面判断与某些自动化决策场景，人们希望用尽量少的比特数表示任意合法手牌的听牌集合。这就引出一个自然的问题：在所有可能的手牌上，听牌集合的最优编码长度到底是多少。

单纯依赖人工枚举或常规程序穷举，可以得到经验结果，但无法提供严格的数学保证。形式化验证的价值在于，它不仅能给出一个编码长度上界，还能证明“任何合法手牌的听牌集合都能被该编码覆盖”，并且这种保证不依赖某个具体程序的运行结果。

2. 核心思路：把不可信的编码方案变成可验证的证书

本文讨论的方案并不把编码算法本身直接嵌入证明系统中执行，而是把它当作一个不被信任的证书。也就是说，编码方案可以由外部工具生成，证明系统只负责验证这个证书是否确实覆盖了所有合法手牌。

这种“生成器不可信、验证器可信”的思路在形式化验证中非常常见。生成器可以使用高性能语言、复杂启发式算法甚至人工构造，只要最终产出的编码方案能够被形式化系统完整检查，那么证明结论就成立。

验证过程的核心是把“每一副合法听牌手牌都被覆盖”这一全称命题，归结为若干有限检查。也就是说，我们不需要对手牌空间做无限遍历，而是按照牌型结构与数量约束，把问题拆分为有限多个需要逐一核对的情况。每一种情况对应一个可判定的检查项，检查项本身可以在证明系统中描述为一个命题。

3. 检查项的形式化与内核求值

这些检查项的含义本身在形式化语言中给出严格定义，并由证明系统证明“只要全部检查项通过，则原命题成立”。这一步称为归约定理，是整个验证中最关键的部分之一。

之后，系统需要对全部 1075 项检查逐一求值。这里特别强调“由内核完成全部检查，不使用任何原生代码求值”。这意味着求值过程运行在证明系统的可信内核中，而不是调用外部语言编写的快速函数。这样做的目的是避免外部求值器引入未经验证的逻辑跳步。

在具体实现中，检查项可以表示为布尔表达式或可判定的计算任务。例如：

check_hand(h) : Bool :=
  match classify(h) with
  | standard => check_standard(h)
  | seven_pairs => check_seven_pairs(h)
  | thirteen_orphans => check_thirteen_orphans(h)
  | _ => false
  end

这只是示意性写法，实际形式化定义需要严格遵循证明系统的语法与可判定性要求。每个检查函数都必须被证明为可终止，并且其结果可以被内核求值。

通过这种方式，最终得到的不再是“某个程序跑了一遍没有报错”的结论，而是“在形式系统中，归约定理成立，且 1075 个检查项全部通过”的证明对象。

4. 可信度边界：只依赖三条基础公理

任何形式化证明最终都会依赖若干基础公理。公理越多，证明系统的可信基面就越大；公理越少，结论越容易被审计。

本文所述构建过程将最终定理的可信边界压缩到只依赖三条标准公理。也就是说，除这三条公理外，不依赖其他自定义公理或未经形式化的假设。

这一性质并不是由某些声明保证的，而是由构建时的“失败即报错”验收门槛强制保证的。具体来说，整个形式化项目的构建过程被配置为：如果任何证明引用了超出允许公理集合之外的假设，构建直接失败。这样一来，每次成功构建都意味着当前代码满足公理使用约束。

这种设计将可信度从一个抽象口号转变成一个可操作的工程约束。任何构建产物都可以被第三方重新构建，并通过相同门槛验证其是否符合公理限制。

5. 构建与持续集成

为了确保结论可复现，项目构建与源码的 SHA-256 清单绑定。也就是说，构建入口记录当前源码与依赖的哈希值，保证构建结果与特定源码版本一一对应。

在 16 线程工作站上，从零开始的完整构建用时 21 分 38 秒。所谓“从零开始”，意味着不依赖任何预编译缓存，编译器与证明检查器需要重新处理全部定义、定理与检查项。

在持续集成环境中，每当源码发生改动，系统都会在标准 Linux 运行器上重新执行完整检查。该运行器配置为 4 个 CPU、16 GB 内存，从零构建用时 31 分 37 秒。虽然耗时明显长于工作站环境，但更重要的是它保证了每次修改都不会悄悄破坏既有结论。

持续集成的作用不仅是发现编译错误，更是验证项目的可复现性。如果某个第三方无法在干净环境中重建证明，那么所谓的形式化验证就缺乏实践意义。通过将构建时间、资源规格与验收门槛全部纳入版本控制，项目可以持续提供可审计的证据链。

6. 为什么这种验证方式值得借鉴

传统上，很多组合问题的“验证”等价于运行一个搜索程序。程序跑完没有异常，人们就认为结论成立。但这种方式依赖程序的正确性，而程序本身可能包含隐藏缺陷。

本文所展示的方法改变了验证责任的分配方式：

• 生成编码方案的程序不需要被信任；
• 编码方案作为证书进入形式化系统；
• 归约定理保证“检查项全部通过”等价于“原始命题成立”；
• 检查项的求值由证明内核完成；
• 构建门槛保证最终结论只依赖极少基础公理。

这样做的好处是，即使外部生成器存在错误，也不会造成错误结论。最多只会生成一个无法通过检查的证书，导致验证失败。失败本身不构成定理，也不会污染证明库。

对于开发者来说，这种“生成与验证分离”的思路不仅适用于麻将听牌集合编码，也可以推广到其他需要强保证的优化问题中，例如调度方案、排班表、路由表或资源分配方案。只要能够把“方案可行”表达为有限项检查，并把检查项在形式化系统中定义清楚，就存在构造类似可信验证流程的可能。

7. 组合细节：为什么检查项是 1075 项

1075 这个数字并非随意设定，而是由听牌集合的结构分类决定。立法麻将的和牌结构包含标准型、七对子与国士无双三类。国士无双的牌型相对固定，检查项较少；七对子要求七种互不相同的对子，数量约束较强，也可以归约为有限组合；标准型则需要处理面子与雀头的各种组合。

在编码方案中，听牌集合可以按“哪些牌可能成为和牌完成牌”进行分类。分类的粒度决定检查项数量。粒度太粗，单个检查项难以判断；粒度太细，检查项数量激增，内核求值时间变长。1075 项是在表达力与验证成本之间的一个平衡点。

形式化归约需要证明分类是完备的：任何合法手牌一定落入某一个检查项所覆盖的情况。这一步通常通过结构性归纳完成。例如，先根据和牌类型对手牌分类，再根据完成牌的候选集合进一步细分，最后对每个细分情况验证编码方案给出的表示是否正确覆盖了听牌集合。

8. 编码长度与检查结果的关系

编码方案的最优性体现在它声称能够用固定数量的比特表示任意合法听牌集合。验证并不直接证明“不存在更短编码”，而是证明“当前方案对于全部合法手牌成立”。如果要证明最优下界，还需要额外论证：存在某一副手牌，其听牌集合的信息量恰好达到该长度，因此任何更短编码都不可能是单射的。

从技术写作角度看，验证可以拆成两个方向：

• 上界方向：给出一个编码，证明所有合法手牌都能被编码；
• 下界方向：构造至少一个具体手牌，证明其听牌集合需要的比特数达到目标值。

本文重点描述上界方向的可信验证。下界方向通常可以通过构造显式反例或计算熵下界来完成，相对容易审计。

9. 工程实践中的注意事项

如果想要复现或设计类似的形式化验证项目，以下几点值得特别关注：

1. 区分生成器与验证器。生成器可以用任意语言实现，但验证器必须完全运行在形式化系统内。
2. 最小化公理依赖。显式声明允许使用的公理列表，并通过构建脚本强制检查。
3. 把求值留在内核中。不要让外部求值结果未经证明就进入证明对象。
4. 记录构建哈希与资源规格。可复现性是可信验证的重要组成部分。
5. 为持续集成配置干净环境。避免依赖开发者本地的预编译状态。

这些实践并不绑定特定证明系统，任何具备足够表达能力与可判定求值能力的形式化工具都可以作为基础。

10. 结语

立直麻将听牌集合的最优编码长度问题，表面上是一个组合游戏问题，实际上涉及可信计算、形式化验证与组合优化的交叉。通过把外部编码方案视为证书，将覆盖性命题归约为 1075 项有限检查，并让证明内核完成全部求值，最终可以得到一个仅依赖三条基础公理的形式化定理。

这种方法的真正价值不在于麻将本身，而在于它展示了一种可落地的验证路径：即使问题本身由复杂搜索或外部程序求解，最终结论仍然可以通过一个小型可信核心得到严格保证。对于追求高可信度的系统设计者来说，这种“生成器不可信、验证器可信”的模式具有广泛的借鉴意义。