结果族 113：Approximate counting and entropy of perfect matchings · 学科：Theoretical computer science · 验证状态：主结果已 Lean 形式化
还是全员结对，但换个问法：假如只告诉你”每条线有多大概率被选中”，在这些限制下，最”随机的”配对方案能有多自由？自由度用熵来量——平均每抽一次能携带多少信息。本文证明：这个最大熵被两个只看单条线的量 F 与 B 紧紧夹住，好比给一台只能看局部统计的机器装上了能称全局的秤。
关键词卡片
@@M@@x_e@@。@@M@@H(x)@@ 是给定边际下的最大熵。@@M@@F=-\sum x_e\log x_e@@ 与 @@M@@B=-\sum(1-x_e)\log(1-x_e)@@，各只看单边两个状态。看个具体例子
正方形 4 顶点（2m=4，m=2）恰有 2 个完美匹配——两组对边，各以 1/2 概率取用 ⇒ 每条边边际 1/2，此时 @@M@@H=\log 2\approx0.69@@，@@M@@F=B=2\log 2\approx1.39@@。定理的数字版（系数 @@M@@2-\tfrac2m=2-\tfrac22=1@@）：@@M@@F-\bigl(2-\tfrac2m\bigr)B=0\;\le\;H=\log 2\;\le\;F=2\log 2@@，两个不等式都严丝合缝。论文还证得几何副产品：支撑边数减所在面的维数 @@M@@\le 3m-2@@，且此界可取等。
为什么值得关心
它证明了 Anari–Oveis Gharan–Vinzant 2018 年提出的完美匹配熵猜想，把”近似计数”与”熵优化”两条线焊在一起，还附带一个确定性多项式时间的粗略计数算法。此前系数一的版本只在二部图成立；一般图里奇割会造出反例，本文把系数精确钉在 2−2/m。
已 Lean 形式化
第一级台阶
导读的问法是：只规定”每条线有多大概率被选中”，最自由的配对方案能携带多少信息？半数学地说：对象是”全员两两结对”的随机方案，操作是固定每条线被选中的概率，然后问在这一切约束下，方案的不确定性最大能到多少。导读那台”只看局部却能量出全局的秤”，就是两个各自只看单条线两种状态的信息量 F 与 B，它们把全局自由度夹在中间。
第二级台阶
用本科术语精确化。完美匹配多面体 P(G) 是所有完美匹配指示向量的凸包，其中一点 x 恰是一组可行的边概率（边际）；H(x) 定义为以 x 为边际的匹配分布熵的上确界；F(x)=−Σx_e log x_e 与 B(x)=−Σ(1−x_e)log(1−x_e) 是两个逐坐标的二元熵。一般图区别于二部图的关键约束是奇割：把奇数个顶点切出来的割。
第三级台阶
定理在这样的语境下陈述：对 2m≥2 个顶点、含至少一个完美匹配的无环多重图，每个边际 x∈P(G) 都满足 F(x)−(2−2/m)B(x) ≤ H(x) ≤ F(x)，且在整个多面体上成立、包括边界。上界只是 Shearer 熵不等式在顶点星上的实例，全文贡献在下界；”奇割”正是系数一失败的根源——三角形扩张构造出使 H<F−B 的可行边际，而”系数大于二也做不到多少”则被极限论证与几何维数下界共同挡住。配套的锐维数界说：支撑边数减去所在最小面的维数至多 3m−2，且可取等。导读里”给局部统计装上全局秤”的比喻，至此成为逐点不等式加计数推论。
证明 Anari–Oveis Gharan–Vinzant 的完美匹配熵猜想：任意可行边边际 @@M@@x@@ 处匹配律的最大熵满足 @@M@@F(x)-(2-2/m)B(x)\le H(x)\le F(x)@@（含边界），并证得锐的面维数界 @@M@@|\supp x|-\dim F_x\le 3m-2@@，附带确定性多项式时间近似计数算法。
规定”每条边以多大概率属于随机完美匹配”（边边际）并不能确定整个匹配的分布；在这组边际下可达成的最大熵 @@M@@H(x)@@ 度量匹配选择的自由度。可行边际恰是完美匹配多面体（perfect-matching polytope）@@M@@P(G)@@ 中的点，Edmonds（1965）的经典定理把它描述为度等式、非负性与奇割不等式（odd-cut inequality）的组合。二部图情形早有系数为一的比较：Schrijver 的计数不等式与 Gurvits 的加权 Bethe 不等式，加上熵对偶，给出 @@M@@H\ge F-B@@，但其论证本质上依赖永久积（permanent）结构；一般图里奇割是真正的障碍——论文在例子一章给出一个八顶点非二部图及可行边际，使 @@M@@H<F-B@@。Anari、Oveis Gharan 与 Vinzant（2018，FOCS 版猜想 6）提出用凸优化做近似计数的框架，并问二元坐标熵 @@M@@F+B@@ 的最大值是否只比 @@M@@\log N(G)@@ 大一个顶点数的线性函数。本文以逐点不等式给出显式肯定。面维数方向，整个多面体的维数由 Naddef 与 Edmonds–Pulleyblank–Lovász 刻画，Abdi 等人最近用层束（laminar）族给出 @@M@@3m-1@@ 的秩界，此处被改进到锐的 @@M@@3m-2@@。
设 @@M@@G@@ 为 @@M@@2m\ge2@@ 个顶点、至少含一个完美匹配的无环标记多重图。定理 1.1：对每个 @@M@@x\in P(G)@@，
@@M@@DF(x)-\Bigl(2-\frac2m\Bigr)B(x)\le H(x)\le F(x),\qquad F(x)=-\sum_e x_e\log x_e,\quad B(x)=-\sum_e(1-x_e)\log(1-x_e),@@
其中 @@M@@H(x)@@ 是边际为 @@M@@x@@ 的匹配律（matching law）熵的上确界（必可取到）；不等式在整个多面体上成立，包括边界。上界是 Shearer 熵不等式在顶点星上的直接实例，全文的贡献在下界。几何侧证得锐估计 @@M@@|\supp x|-\dim F_x\le 3m-2@@，其中 @@M@@F_x@@ 是含 @@M@@x@@ 的最小面（minimal face）；三角形扩张构造表明它在每个正偶数阶都能取到，且这些例子同时给出”系数一”的反例。推论方面：@@M@@\log N(G)\le\max_{x\in P}(F+B)\le\log N(G)+3m-2@@；若 @@M@@G@@ 含 @@M@@k\ge2@@ 条两两边不交的完美匹配，则 @@M@@N(G)\ge e^{-2(m-1)}k^m@@；对每个奇割至少 @@M@@k@@ 条边的 @@M@@k@@ 正则图（等价于正偶数阶的 @@M@@(k-1)@@-边连通 @@M@@k@@ 正则图）结论相同——这确立了 Ebrahimnejad–Nagda–Oveis Gharan 猜想的连通性形式。算法章还证明：对二进制编码的重数输入，存在确定性算法在输入长度的多项式时间内返回整数 @@M@@A@@，使 @@M@@N(G)/512^n\le A\le N(G)@@，且 @@M@@A=0@@ 当且仅当 @@M@@N(G)=0@@。
证明分几何与解析两步。几何步先以”跨紧奇割粘合匹配律”重证 Edmonds 多面体定理：两个收缩（contraction）图中的可行均值若在割边坐标上一致，可粘合成原图的可行均值；粘合方式是按公共割边概率选一条边、两侧独立采样后接回。随后对最小面的余维数归纳：取 @@M@@x@@ 处取等的非平凡奇割 @@M@@C=\delta(S)@@，两侧收缩得小图，其面上的方向粘回父面时须在割边坐标上吻合；但每个方向在割上的坐标和恒为零（收缩顶点处的度等式），故吻合条件只有 @@M@@|C|-1@@ 个独立方程而非 @@M@@|C|@@ 个。省下的这一个方程使递推在 @@M@@3m-2@@ 处恰好闭合，改进了 Abdi 等人的 @@M@@3m-1@@。附录另给出层束族的替代证明。
解析步利用指数族（exponential family）结构：最小面上的最大熵律具有 Gibbs 形式 @@M@@p_a\propto e^{\theta\cdot a}@@，其对数配分函数的 Hessian 就是协方差矩阵 @@M@@K@@，且 @@M@@\operatorname{im}K=T(x)@@（面的方向空间）、@@M@@\rank K=d=\dim F_x@@。反设 @@M@@J_c-H@@（@@M@@J_c=F-cB@@）在某点取正的最大值：先删去零坐标边、去掉值为 1 的边的端点，归约到所有坐标严格分数的图——@@M@@F,B,H@@ 三函数与最大化性质在此归约下不变。在最小面内做指数倾斜（exponential tilt）得光滑曲线；一阶平稳条件恰好消去二阶导数中的三阶项，于是二阶条件沿 @@M@@K@@ 的单位正交特征向量代入并求和给出 @@M@@0\ge d+\tr(KD)@@，其中 @@M@@D@@ 是 @@M@@J_c@@ 的对角 Hessian。坐标是布尔值，故 @@M@@K_{ee}=x_e(1-x_e)@@，直接算得 @@M@@\tr(KD)=-|E|+(c+1)m@@，从而 @@M@@0\ge d-|E|+(c+1)m@@。与几何下界 @@M@@d\ge|E|-3m+2@@ 联立得 @@M@@0\ge 2+(c-2)m@@；取 @@M@@c=2-2/M+\varepsilon@@（@@M@@2M@@ 为原图顶点数）而归约图顶点数 @@M@@2m\le 2M@@，右边严格为正，矛盾。先取严格系数再令 @@M@@\varepsilon\downarrow0@@ 才得到 @@M@@2-2/M@@——这一极限步骤不可省略，因为 @@M@@m=M@@ 且 @@M@@\varepsilon=0@@ 时几何比较可以是等号。上界则由链法则给出：每条边属于两个顶点星、每个星处恰选一条边，故 @@M@@\Ent(X)\le\frac12\sum_v[-\sum_{e\in\delta(v)}x_e\log x_e]=F(x)@@。
确定性算法把 AOG 的熵优化路线完全落地：先补全到 @@M@@K_n@@、给缺失对赋微小二进权重以分离零计数；把加权熵目标换成整数斜率的二进插值（dyadic interpolant），并在方盒上加大权精确罚函数（exact penalty），从而在固定网格上做整数化的投影上升迭代；被违反的约束行由保奇偶性的最小奇割递归（承 Padberg–Rao 传统）找到。全程只用整数与有理数运算，输出 @@M@@2^\rho@@，比特复杂度对输入长度多项式。
本文主结果已由 Lean 形式化证明（结果族文档标注 lean/docs/113.md），是族 113 中验证最充分的一篇。姊妹篇给出一般图完美匹配的全多项式随机逼近（相对误差、FPRAS），本文则给出确定性的指数因子近似，两条路线互补支撑同一结果族。按 OpenAI 官方声明，未经形式化的结果可能有问题；本文核心定理已形式化，算法章的比特复杂度账目仍以论文推导为准。
问 1：证明里最关键也最脆弱的一步是哪里？
| 答：几何与解析两步的”合拢处”。几何步靠奇割收缩递推：父面方向由两个收缩面的方向在割边坐标上吻合地拼成，而每个方向的割坐标和恒为零，故吻合只施加 | C | −1 个独立方程——省下的这一个方程让余维数递推闭合在 3m−2。解析步反设 F−cB−H 有正最大值，用指数倾斜加一阶平稳性消去二阶导数中的加速度项，对协方差正特征向量求和得 0 ≥ d− | E | +(c+1)m；与几何下界 d ≥ | E | −3m+2 联立得 0 ≥ 2+(c−2)m。两条异质估计只差一步就要互相矛盾，最后还须取 c=2−2/M+ε 再令 ε↓0——导读明言这一极限步骤不可省略，是全文最细的接缝。 |
问 2：为什么系数一在一般图不行、二部图却行？
答：二部图的 Schrijver 不等式与 Gurvits 加权 Bethe 不等式本质上依赖永久积结构，配合熵对偶给出 H≥F−B。一般图里奇割是真正障碍：论文用三角形扩张（Klee 图式）构造出八顶点非二部图及可行边际使 H<F−B，并在每个正偶数阶同时取等几何界 3m−2。
问 3：与 AOG 2018 猜想及 Abdi 等人的结果相比，真正的新意是什么？
答：AOG 只问 max(F+B) 是否比 log N(G) 多一个顶点数的线性函数；本文给出逐点不等式，把那个线性误差作为优化后的推论钉在 3m−2。面维数方向，Abdi–Cornuéjols–Dadush–Dalirrooyfard 用层束族给出 3m−1，本文改进到锐的 3m−2 且构造取等例子。相比 Ebrahimnejad 等需谱扩张假设的正则图计数，本文的 (k/e²)^m 对满足奇割条件的 k 正则图无条件成立，并确立其连通性形式猜想。
问 4：主结果已 Lean 形式化，风险还剩多少？
答：熵定理经形式化是当前最强核验。剩余风险在形式化边界之外：确定性算法章的比特复杂度账目（512^n 因子、整数斜率二进插值、精确罚函数、保奇偶割递归）”仍以论文推导为准”；且需核对形式化陈述与论文约定逐字一致——自然对数、平行边按颜色区分、m=1 时的退化条款等细节若错位，形式化就保护不到原命题。
问 5：这个结果最可能出错的模式是什么？
答：AI 生成证明在这类”微分—凸几何”论证中的典型病灶是：在面边界上做变分（协方差核奇异、不能在环境空间求逆）。论文明确宣称全部论证”在面内进行，不反演环境协方差核、不跨面求导”（引言末段），这恰是正确做法，也恰是最容易被忽略的做法；此外三角形扩张例子的”取等”计算若差一个顶点，锐性与系数论证都要重开。
问 6：谁会用到它？
答：三条下游：计数推论 log N(G) ≤ max(F+B) ≤ log N(G)+3m−2 直接把凸优化变成近似计数；k 条边不交完美匹配给出 N(G) ≥ e^{−2(m−1)}k^m，覆盖桥立方图指数下界之外的度数增长情形；确定性 512^n 因子算法处理二进制重数输入且精确检测零计数，与姊妹篇 FPRAS 的相对误差路线互补。
总评
它以逐点熵不等式加锐面维数的双重形式了结 AOG 猜想，并经 Lean 形式化背书，是族 113 中验证最充分的一篇；主要保留意见在系数 2−2/m 是否最优（论文自己说例子未确立）与算法章未经形式化的位级账目。