AI 中文总结
本文提出一个认证延续框架，用于深度平衡网络的推理与训练，通过同伦跟踪和加载Tikhonov修复实现多项式比特复杂度保证，并用Lean 4验证核心。
AI 中文摘要
我们为平衡计算和深度平衡网络（DEQs）的训练开发了一个认证延续框架，其中训练被表述为精度为 $2^{-b}$ 的插值问题。对于推理，紧凑输入同伦从提供的起始根中选择唯一分支，并且舍入牛顿跟踪器在认证的边界、条件数、导数和管半径界限下跟踪该分支。对于训练，我们通过可编程的休眠双线性秩一通道增强了局部加低秩递推。加载的Tikhonov求解在不进行谱分解的情况下诊断失败的插值过程；与过程残差对齐的保持输出的修复提供了所需的方向。训练需要在每个过程区域上实现认证的门控实现和列稳定性、良置的推理以及有限更新的误差预算。利用多项式几何、编码、精度和完整后端预算，认证推理和训练的比特成本均为 $O(\operatorname{poly}(L+b))$，其中 $L$ 是编码实例长度。训练器使用 $O(b+\ell)$ 次过程，并从由 $2^\ell$ 限定的初始残差中预留通道。这些保证涉及一个认证承诺类。Lean 4 验证了定量核心和具体推理后端；数值比较说明了加载机制。
英文摘要
We develop a certified continuation framework for inference and training in deep equilibrium networks (DEQs), with training posed as interpolation to accuracy $2^{-b}$. For inference, input homotopy selects an equilibrium branch from a supplied start root, and a rounded tracker follows it under quantitative conditioning, derivative, boundary, and tube-radius certificates. The framework includes structured factorized certificates, sequential block elimination, inheritance of contraction guarantees in adapted coordinates, and bordered continuation through simple folds. For smooth multidimensional DEQs, including tanh networks, rational local tests can construct and validate oriented continuation charts under explicit geometric promises. For training, programmable dormant bilinear rank-one channels provide output-preserving residual-aligned repairs. Loaded Tikhonov solves diagnose insufficient parameter-to-output directions, while certified gate realization, column stability, well-posed inference, and finite-update error budgets control each pass. Under polynomially bounded certificate, encoding, precision, and backend costs, both inference and training have bit complexity $O(\mathrm{poly}(L+b))$, where $L$ is the encoded instance length; training uses $O(b+\ell)$ passes and reserve channels from an initial residual bounded by $2^\ell$. A budgeted implementation returns either certified success or inconclusive termination. The quantitative core and local certificate machinery are machine-checked in Lean 4, while numerical experiments illustrate the training mechanism.
CommentsPython scripts and Lean formalization are included as ancillary files
