结果族 116：Uniform black-box noncommutative identity testing across characteristics · 学科：Theoretical computer science · 验证状态：主结果已 Lean 形式化
这篇的电路多了”除法”键——矩阵世界的除法是求逆，一旦代进去的矩阵不可逆，整个求值就地卡死。于是单个万能钥匙不够用了，论文改配一整串钥匙：只要公式本身”有救”（存在合法求值），钥匙串里总有一把既不把锁芯卡死、还能拧出非零的转动。
关键词卡片
看个具体例子
先看一个带除法的迷你公式长什么样：
论文定理：只凭 @@M@@n@@ 和 @@M@@s@@，确定性机器在多项式比特时间内输出一份多项式长的有理矩阵元组列表；任何规模 @@M@@\le s@@ 的非零可采纳公式，必在列表中某处取到有定义且可逆的值——与公式里有理常数的位数、逆门嵌套多深都无关。
为什么值得关心
它把含除法门的黑盒非交换恒等测试从拟多项式打击集降到多项式大小的列表，解决了 Garg–Gurvits–Oliveira–Wigderson 提出的黑盒 SINGULAR 构造问题的有理系数版本。
已 Lean 形式化
第一级台阶
入门导读说：电路多了”除法”键，矩阵世界的除法是求逆，碰到不可逆的矩阵求值就卡死，所以单个万能钥匙不够，要配一串钥匙。翻译成半数学语言：对象是允许”对中间结果取逆”的算术表达式；代入的是一组组方阵；一把钥匙合适，指的是在这组方阵上每一步求逆都遇到可逆矩阵、且最终读数不为零。钥匙串的配方只凭变量个数与规模上限两个数字磨出，与被检表达式无关。
第二级台阶
用本科术语说：有理非交换公式是一棵树，叶为变量或有理常数，二元门做加法或按序乘法，一元门做求逆，规模 @@M@@s@@ 连叶与逆门一起数。可采纳（admissible）指它至少有一处正维数的有理矩阵求值有定义；非零指某个有定义的求值非零。打击列表（hitting list）是一列矩阵元组：每个非零可采纳公式都在其中某处取得有定义且可逆的值。仿射铅笔 @@M@@L(x)=A_0+\sum_iA_ix_i@@ 则是把公式树翻译成线性代数的载体。
第三级台阶
定理（引言 thm:main）在此陈述：确定性图灵机输入 @@M@@1^n,1^s@@，在 @@M@@C(n+s+1)^k@@ 比特时间内输出有限列表 @@M@@\mathcal H_{n,s}@@（输出总长同界）。假设”可采纳”挡住了求值域为空、无从谈测试的公式；”保留原树”意味着后来会消去的分支里的求逆条件同样要满足；”规模 @@M@@\le s@@“对应至多 @@M@@s+1@@ 个阶 @@M@@\le B=2s+1@@ 的铅笔。结论：任何非零可采纳公式在列表某处取得有定义且可逆的值——与有理常数位数、逆门嵌套深度无关；推论还打击一切有界的可行仿射铅笔，并给出恢复长方铅笔非交换秩的非自适应列表。
对含求逆门的有理非交换公式，确定性生成器仅凭变量数 @@M@@n@@ 与规模 @@M@@s@@，在多项式比特时间内输出多项式大小的有理矩阵列表，使每个非零且可采纳的公式在某个元组处求值有定义且取值可逆，把黑盒有理恒等测试的打击集从拟多项式降到多项式规模。
有理非交换公式（noncommutative rational formula）在加法、有序乘法之外允许一元求逆门，求值时要求每个逆门遇到的矩阵都可逆，否则该求值无定义。Hrubeš–Wigderson（2015）建立了这一计算模型并把它化为线性矩阵奇异性测试；随后算子缩放与非交换秩计算（GGOW、IQS 等）给出读取输入的白盒确定性多项式时间算法，但它们都要用到公式的具体系数。黑盒方面，Arvind–Chatterjee–Mukhopadhyay 先后对逆高度 2 与任意逆嵌套给出拟多项式大小的有理矩阵打击集；Derksen–Makam 证明可采纳公式存在定义求值所需的维度多项式界并由此得到随机算法。悬而未决：能否只凭规模参数、不依赖输入系数，确定性生成通用打击列表并具多项式维度？这正对应 Garg–Gurvits–Oliveira–Wigderson 提出的黑盒 SINGULAR 构造问题的有理系数版本。本文在 @@M@@\mathbb Q@@ 上解决。
定理 1.1：存在确定性图灵机 @@M@@G@@ 与常数 @@M@@C,k@@：输入 @@M@@1^n,1^s@@，输出有限列表 @@M@@\mathcal H_{n,s}@@，成员是 @@M@@n@@ 个有理方阵构成的元组；生成时间与输出总比特长均不超过 @@M@@C(n+s+1)^k@@。对每个规模至多 @@M@@s@@ 的非零可采纳（admissible，即存在某个正维数的有理矩阵求值有定义）有理公式 @@M@@\Phi@@，列表中某元组给出 @@M@@\Phi@@ 的一个有定义求值，且取值可逆。可逆值结论强于非零值要求。同一列表适用于一切这样的公式，与其有理常数的比特长、逆门嵌套深度无关；生成器不接收公式、不用随机性或外部建议，所有元组共享仅依赖 @@M@@n,s@@ 的同一维数。论文另有推论：同一构造打击每个阶至多 @@M@@B@@ 的可行（feasible）有理仿射铅笔（affine linear pencil，形如 @@M@@A_0+\sum_iA_ix_i@@ 的矩阵）；并构造非自适应列表，用归一化求值的秩恢复长方有理铅笔的非交换秩（noncommutative rank，即自由除环上的秩）。
证明按”桥接—扩张—变形—有理化”四步展开。第一步把公式树编码为线性代数：对每个子树 @@M@@h@@ 构造仿射铅笔 @@M@@L_h@@ 与常值行、列 @@M@@u_h,v_h@@，使 @@M@@h=u_hL_h^{-1}v_h@@，其中逆门对应块矩阵 @@M@@\begin{pmatrix}L_g&v_g\\u_g&0\end{pmatrix}@@，铅笔阶数为 @@M@@|h|+1@@。规模 @@M@@s@@ 的公式由此给出至多 @@M@@s+1@@ 个阶 @@M@@\le B=2s+1@@ 的铅笔，它们同时可逆恰保证原树每个逆门有定义且终值可逆。配合除环提升引理——把任一有定义非零求值中的矩阵提升进循环符号除环（cyclic/symbol division algebra），非零值即成可逆值——非零可采纳公式必拥有这样一族可行铅笔。这一步保留了原公式树：后来会消去的分支里的求逆条件同样要满足。
第二步解决”在与系数无关的矩阵上取得高秩”：构造 @@M@@n+1@@ 个 @@M@@\mathbb Q[t]@@ 上的长方矩阵 @@M@@R_i(t)@@，它们反转在互异点 @@M@@0,\ldots,n@@ 处的 Taylor 展开并以 @@M@@t@@ 的幂加权 Taylor 系数；Wronskian 界表明，任何维数 @@M@@\le B@@ 的非零子空间（系数甚至可取 Laurent 级数）的诸像之和的维数严格超过其维数的 @@M@@n@@ 倍，从而可行铅笔满足 @@M@@\rank\bigl(\sum_iA_i\otimes R_i(t)\bigr)>(q-1)M@@。第三步做除环变形：引入参数 @@M@@p,r@@，以 @@M@@X=pD@@、@@M@@Y=rS@@（@@M@@XY=\omega YX@@，@@M@@\omega@@ 为单位根）生成嵌于 @@M@@M\times M@@ 矩阵的除环，块元素落入其中时普通秩被 @@M@@M@@ 整除，故上述严格不等式强制满秩 @@M@@qM@@；相应行列式是 @@M@@t,p,r@@ 的次数 @@M@@\le3BM^2@@ 的非零多项式，左除 @@M@@R_0^*@@ 则恢复铅笔的常数项。第四步消除单位根并落到有理数：用代数 @@M@@\mathcal R=\mathbb Q[\xi]/(\xi^\ell+1)@@（@@M@@M@@ 取 2 的幂，@@M@@\ell=M/2@@）的正则表示把单位根系数替换为有理矩阵，可逆条件须在全部 @@M@@\ell@@ 个根处同时成立。对固定公式，至多 @@M@@s+2@@ 个铅笔与 @@M@@\ell@@ 个根的行列式条件之积是次数有界的非零多项式，因此固定的三维整数网格 @@M@@\{1,\ldots,H\}^3@@ 中必有一点使其非零；生成器对每个格点计算 @@M@@Z_i=\rho_M(\widetilde R_i(t_0,p_0,r_0))@@，凡 @@M@@Z_0@@ 可逆即输出元组 @@M@@(Z_0^{-1}Z_1,\ldots,Z_0^{-1}Z_n)@@。精确有理算术给出时间与输出的比特界。
据结果族元信息，本文主结果已附 Lean 形式化证明；本族另两篇姊妹篇（无除法公式的单个打击点、正特征素域打击点）暂无形式化，按 OpenAI 官方声明”未经形式化的结果可能有问题”，宜以社区核验为准。三篇共享”编码 + 秩或阶数界 + 有限化下降”的框架并互相支撑，本文处理其中最一般的带除法情形，且其打击列表只需规模参数即可生成。
问 1：证明里最关键、最脆弱的一步是什么？
答：四步链中第二、三步的衔接。”扩张”一步用 @@M@@\mathbb Q[t]@@ 上的长方矩阵 @@M@@R_i(t)@@ 与 Wronskian 界得到 @@M@@\rank(\sum_iA_i\otimes R_i(t))>(q-1)M@@；”变形”一步把矩阵提升进循环除环，利用”块矩阵在此代数中的秩被 @@M@@M@@ 整除”把严格不等式强制成满秩 @@M@@qM@@。秩的可整除性与不等式只差 1 的余量，是整条证明最紧的地方；最后的固定三维整数网格能命中非零行列式，也全靠这条满秩链给出的次数界。
问 2：”可采纳”这个假设为什么不能去掉？
答：不可采纳的公式求值域为空——任何代入都卡死在某处逆门，根本没有”有定义的读数”可供判零，测试问题无从谈起。引言特意采用这套操作性定义，避免构造自由除环；论文未讨论不可采纳公式的处理。
问 3：为什么必须保留原表达式、不许先化简消去分支？
答：引言明言：等价的表达式可对中间逆施加不同条件，代数消去并不扩大求值域。列表里的元组必须满足该树施加的一切定义域条件，”包括后来会消去的分支里的求逆条件”；若先化简再测试，就会漏掉这些条件，结论对原公式失效。
问 4：与已有工作相比，真正的新意是什么？
答：黑盒方向上，Arvind–Chatterjee–Mukhopadhyay 对逆高度 2 及任意逆嵌套都只有拟多项式大小的打击集；白盒方向上 GGOW/IQS 的多项式时间算法要读取输入系数。本文只凭 @@M@@(n,s)@@ 确定性生成多项式规模的列表，给出可逆值（强于非零），且不依赖常数位数与逆深度，回答了 GGOW 提出的黑盒 SINGULAR 构造问题的有理系数版本，并给出 ACM 前言结论中所问的多项式矩阵维数。
问 5：这一篇的 AI 出错风险与姊妹篇有何不同？
答：据结果族元信息，本文主定理已附 Lean 形式化证明，这是三篇中可信度最高的一篇，经典的”符号算错一步全塌”风险已大幅降低。残余风险在形式化之外的部分：恢复非交换秩的推论的代价核算、以及与 ACM 拟多项式界的定量比较（论文自己注明依赖特定预印本版本的定理编号）。
问 6：为什么是列表而不是单个元组？
答：含逆门后，每个公式自带一族不同的定义域条件（各子公式求逆处的可逆性），通用元组要同时满足所有公式的所有条件；构造上，证明靠固定整数网格逐点尝试非零行列式，天然产出一列元组。单个多项式维数元组是否足够，论文未讨论。
问 7：谁会用到它？
答：做非交换有理恒等测试与非交换秩计算的人：黑盒 SINGULAR 有了多项式规模的有理构造；长方仿射铅笔的非交换秩可由非自适应列表的归一化求值秩恢复，直接服务算子缩放与线性代数正则化方法的使用者。
总评
这是本族最一般的一篇：允许除法、只凭规模参数、多项式成本，且主定理经 Lean 形式化，分量扎实；最大风险不在主定理本身，而在推论的代价陈述与对外部文献版本的定量比对。