Existence of the Core in Approval-Based Committee Elections
Patrick Becker, Matthias Greger, Dominik Peters
cs.GT
2026-09-11
Becker、Greger与Peters用谐波熵目标证明：任意批准制多赢家选举都存在core委员会；单人替换的局部最优即可，Hare配额下多项式时间可算。
批准制多赢家选举要做的事很具体：n 个选民每人交一份批准名单，从 m 个候选人里选出恰好 k 个。选民效用是「自己批准的人里进了几个」。比例代表要求足够大、口味接近的群体，拿到跟规模成比例的席位。
2017 年 Aziz 等人把合作博弈的 core 搬进来。core 是一组稳定性条件：没有哪个联盟能按人数集资另组班子，还让每个成员都严格变好。形式化之后，联盟 S 可以按 Hare 配额 q = n/k 另组候选人 T；如果 |S| ≥ (n/k)|T|，且 S 里每个人对 T 的效用都严格高于现委员会 W，W 就被挡住。JR、EJR、FJR 还要求联盟对同一批候选人足够齐心。core 不要求齐心，各自变好就算数，因此更硬。
存在性从那时起就是公开问题。Lackner 与 Skowron 2023 年的综述把它标成该理论的主悬案。绕路的成绩单是：Proportional Approval Voting（PAV）给 2-近似，Method of Equal Shares（MES）给对数近似，Lindahl 均衡路线最近到 3.65-近似。精确存在只在委员会至多 8 席、候选人至多 15、至多 7 种选民类型、至多 8 个选民、一维定义域、或每个候选人有 k 份拷贝这些特例里成立。
一般实例空不空，一直没人能拍板。
新规则在所有 k 人委员会 W、以及该委员会上的支付系统上，最大化谐波熵（harmonic entropy）。
支付系统给每个选民 1 单位预算，钱只能付给自己批准的当选者，剩下的叫储备 ri；每个当选者收到的总付款不超过配额 q。这套会计来自 MES、Phragmén 那一支。差别是这里只卡收款上限，不要求付满。单独一个支付系统给不出公平性，还要限制落选者支持者手里剩多少钱。
谐波熵是给支付向量准备的势函数。对概率向量 x，先按水位填充定义一串高度 fℓ(x)：把高于 τ 的坐标削到 τ，释放的质量刚好够新造 ℓ 个高度为 τ 的坐标。直觉像往一组柱子上倒水，一直倒到能再添 ℓ 只等高的杯子。然后
F(x) = Σ{ℓ=0}^∞ (1/(ℓ+1) − fℓ(x))
钱全堆在一个坐标上，F = 0。均匀摊在 d 个坐标上，F 等于第 d−1 个调和数 H{d−1}。Shannon 熵在同一点是 log d。F 连续、凹、对称，末尾补 0 不变值。均匀摊开得分最高，这就是「别让少数人把预算砸在少数人身上」。
水位填充算子 Φ 从现有坐标里舀出一块新坐标。Φ 把水位序列平移一格，于是 F(Φ(x)) − F(x) 正好等于 x 的最大坐标。加候选人、删候选人的目标变化因此能被配额钉住：
两边一对：单人替换若抬不高 q − n/(k+1)，每个落选者的储备负载就严格小于 q。再配上「付给当选者的单价不超过自己的储备」，这就是 core+ 的支付证书。core+ 把联盟与提案松弛到 [0,1] 分数，比整数 core 更强，过了 core+ 一定过 core。证书来自 Farkas 引理，对偶于那张分数阻挡线性规划。给定委员会是否 core+，解一个线性规划就能判定。
谐波熵这条路是把 PAV 那种全局福利最大化，和 MES 那种付款记账焊在一起。势函数专门为「加一个、删一个」的交换论证设计，所以局部最优就够，不必先找到全局最大。
对任意配额 n/(k+1) < q ≤ n/k，任意选举实例都存在满足 core+ 的 k 人委员会。谐波熵全局最大者在里面，单人替换下的局部最优也在里面。
Hare 配额 q = n/k 下可以多项式时间算出来。做法是局部搜索：把无穷级数截到 T = 8k²(k+1) 项，截断目标变成规模 O(nkT) 的线性规划。从任意 k 人委员会出发，某个单人替换若把截断目标抬高至少 δ/2 就走过去。算法实际使用的配额是 Hare 与 Droop 的中点 q = ½(n/k + n/(k+1))，改进阈值 δ = n/(2k(k+1))。中点比 Hare 更严（更小的配额让更小的联盟也能集资），过了中点的 core+ 一定过 Hare 的 core。替换次数至多 4k(k+1)Hk，每轮最多看 k(m−k) 个邻居。
Droop 配额 n/(k+1) 下 core+ 也非空：从上方用一串配额逼近，有限个委员会里必有一个无限次出现，这个委员会挡住所有严格 Droop 分数异议。这一侧没有多项式算法。
Hare core 存在性已在 Lean 项目 ABCVotingLean 里形式化验证。
| 方法 | 保证 | 范围 |
| PAV | 2-近似 core | 一般实例 |
| MES | 对数近似 | 一般实例 |
| Lindahl 取整 | 3.65-近似 | 一般实例 |
| PAV 等特例 | 精确 core | k≤8 / m≤15 / ≤7 类型 / ≤8 选民 |
| 谐波熵规则 | 精确 core+ | 任意实例，多项式可算 |
批准制多赢家选举是比例委员会、参与式预算、多席位代表制的标准模型。core 问的是：有没有一种选法，能挡住所有「按人数集资另组班子、人人严格变好」的集体抗议。答案现在是有，而且不必穷举 C(m,k) 个委员会。局部搜索加 LP 就能交出委员会和一张支付证书。
这还不是能直接替换 PAV 或 MES 上线的规则。每步要评估 k(m−k) 个邻居，每个邻居解一次 O(nk⁴) 规模的 LP。理论位置变了：core 从「也许是空集」变成「总能找到、还能用 LP 审计」。
作者说还在探这条规则在 core+ 之外的公理表现，并希望谐波熵能用到别的比例代表问题上。
致谢写明：规则和 core+ 证明是 GPT-6 Astra 在长时间交互里找到的。起点是 Lindahl 取整，模型先给出约 2.065 的近似比，再被推到精确 core。作者做了核验，并把证明改写成人类可读。这不改变定理内容，但改变了这条证明是怎么出现的。
「多项式时间」是复杂度上界，不是实用速度。T = 8k²(k+1)，LP 规模 O(nk⁴)，再乘至多 4k(k+1)Hk 轮、每轮 k(m−k) 个邻居。论文没有实现，也没有运行时间数字。k=20、m=100 这种规模，按上界估会非常重。
Droop 配额只证了存在，没有多项式算法。Hare 那套局部搜索跑的是介于两者之间的配额。
core+ 比整数 core 强，所以推到 core 没有缺口。谐波熵规则与 PAV、MES 在 JR、EJR、FJR、单调性、计算代价上的对照，论文没有给。作者承认这些性质还在探。
Lean 验证覆盖 Hare core 存在，不覆盖算法正确性，也不覆盖 Droop。
证明绑在批准效用（效用等于交集大小）和单位预算上。一般单调偏好、参与式预算的加性效用，core 是否非空仍开放；先前 3.65-近似走的就是那条更广的路。把谐波熵原样搬过去，水位填充那一串交换不等式未必还成立。