自适应学习运行时的观察保持门控与语义：Lean 4.19.0 验证 21 条新定理

版本 1.1 - 2026年10月12日 - 为编辑审阅准备

作者：匿名

摘要

我们为具有优化器记忆、模型修订、请求队列和被拒绝事件的自适应学习运行时给出了一个集合值语义。数值数据是不透明载荷，具有单独的验证回执接口。到离散控制器的投影保留单步结果和有限记录。我们证明了类型化检查点往返、编码单射性、延续保持，以及一个根据模型检查提议转换的门控。Lean 4.19.0 检查了 21 个新定理；相同的步骤和门控定义被编译进实时控制器。证据包括 45 个测试、124,064 次有界控制器比较、300 个生成事件，以及两个 NumPy/JAX 场景。编译器、JSON、Python 适配和数值内核仍是明确的信任边界。贡献在于一个经过检查的实例化，将控制观测和完整检查点载荷结合在一个感知修正的工件中。

1. 背景与先前工作

配套手稿分别讨论了更高时间组合、类型化张量响应和有状态目标查询 [1-3]。本笔记将一个小型学习运行时与一个精确控制模型和一个集合中的实时对应门控连接起来。一般无穷范畴一致性、实本原导数和一致数值模拟仍是单独的义务。

编译器语义保持和翻译验证为实现对应提供了成熟方法 [4,5]。这里，各个提议转换根据可执行模型进行检查。贡献在于经过检查的实例化，具有修订敏感的请求、保留的优化器载荷和拒绝观测；归纳精化或基于等式的验证均不被声称为新贡献。Lean 提供证明和控制器源代码 [6]；JAX 提供单独测试的数值后端 [7]。

2. 完整状态、投影和观测

固定一个程序标识 $p$ 和一个有限后端名称列表 $B$。一个票据是 $(i,r)\in\mathbb N^2$：标识符和修订。待处理请求和完成携带票据以及特征或输出胶囊。胶囊是有限字符串。适配器对 float64 数组使用规范 JSON，包括形状和 dtype；Lean 将其数值含义保持为未解释。

定义 2.1（完整状态）。 一个状态 $s\in S$ 包含程序和 backend 标识；参数、速度、学习率、动量和查询历史胶囊；修订 $r$；容量 $c$；下一标识符 $n$；以及有序的待处理和已完成列表。这些保留每个运行时检查点字段，包括查询胶囊中的目标、点、投影、响应和损失数据。保留并不证明数值真实性。

定义 2.2（控制投影）。 映射 $\alpha:S\to C$ 遗忘胶囊并保留程序、后端、修订、容量、下一标识符和有序票据列表。不同的参数或记忆可以投影相等，因此控制相等并不意味着训练等价。

$C$ 上的布尔谓词 $V$ 检查程序 $p$、后端属于 $B$、容量至多 1024、待处理长度至多等于容量、标识符小于 $n$、两个列表中的标识符互不相同、待处理修订等于 $r$，以及完成修订至多等于 $r$。自然数类型提供非负性。完整模型已证明的不变式是 $V(\alpha(s))$。形状、有限性、量级和超参数条件是额外的 Python 侧数值域检查，而不是由该 Lean 不变式证明的谓词。

定义 2.3（结果）。 一个结果是 $(s',a,\rho)$，其中 $a$ 是布尔接受标志，$\rho$ 是以下之一

$$ \{\mathsf{accepted},\mathsf{capacity},\mathsf{pending},\mathsf{stale}, \mathsf{domain},\mathsf{unsupported}\}. $$

其擦除为 $\alpha_O(s',a,\rho)=(\alpha(s'),a,\rho)$。该定律涵盖这些规范化观测，而不是每个 Python 诊断字符串或值；梯度范数诊断未被认证。

3. 事件与受保护转移

事件包含其种类、载荷胶囊，以及用于受支持数值运算的布尔回执。回执表示提议域检查，而不是导数或舍入证明。

• 提交。 离散前置条件：待处理长度低于容量；候选变更：前插 $(n,r)$ 及其特征胶囊；递增 $n$。
• 完成 $i$。 离散前置条件：$i$ 处于待处理状态；候选变更：移除该待处理票据；追加 $(i,r)$ 及输出胶囊。
• 训练。 离散前置条件：待处理列表为空；候选变更：替换参数、速度和查询胶囊；递增 $r$。
• 重配置。 离散前置条件：无额外事件前置条件；候选变更：替换后端、容量、速率和动量字段。

域失败和不支持的事件永远不会提交候选。重配置保留参数、速度、查询、待处理和已完成请求、修订、下一标识符以及程序身份。训练不会跨越活跃请求修订：当任何请求处于待处理状态时，它会被阻塞。

将完整候选构造记为 $K:S\times E\to S$，控制候选构造记为 $\bar K:C\times\bar E\to C$，事件擦除记为 $\epsilon:E\to\bar E$。令 $P(c,e)$ 为所展示的离散前置条件，$N(e)$ 为回执。接受测试为

$$ A(c,e)=P(c,e)\wedge N(e)\wedge V(\bar K(c,e)). $$

当 $A(\alpha(s),\epsilon(e))$ 成立时，完整步骤 $F(s,e)$ 返回 $(K(s,e),\mathsf{true},\mathsf{accepted})$。否则它原样返回 $s$，并带有假接受和相应的失败标签。控制器步骤 $G$ 使用 $\bar K$ 进行相同的测试并产生相同的标签。失败的离散前置条件优先于不良的数值回执。因此，在请求待处理时提交的无效训练数据仍然具有待处理观测。数值域和配置失败共享域标签。

命题 3.1（帧与拒绝）。 被拒绝的步骤保留完整状态。从有效初始状态出发，每一步都保持 $V\circ\alpha$。重配置保留上述字段，包括速度记忆；待处理列表非空时的训练会被拒绝。

证明。 拒绝选择旧状态；接受要求候选满足 $V$。重配置仅赋值其四个字段。当请求待处理时，训练的前置条件为假。Lean 检查 rejected_unchanged、control_preserves、step_preserves、reconfigure_frame 和 training_blocked。$\square$

4. 观察感知对应

引理 4.1（候选擦除）。 对每个状态和类型化事件，

$$ \alpha(K(s,e))=\bar K(\alpha(s),\epsilon(e)). $$

证明。 Submit 将新请求映射到其票据。Complete 按标识符过滤，因此票据映射与过滤和追加可交换。Training 在擦除后仅改变修订；重配置改变后端和容量。失败构造子是恒等。Lean 检查列表过滤引理和 candidate_refines。$\square$

定理 4.2（单步对应）。 对所有 $s,e$，

$$ \alpha_O(F(s,e))=G(\alpha(s),\epsilon(e)). $$

证明。 两个步骤评估相同的接受测试。引理 4.1 识别被接受的后续控制；其他观察按定义一致。拒绝保留旧控制和匹配的失败标签。这是 step_refines。结构相等既不需要初始有效性也不需要收据正确性；不变量保持和活适配器需要有效起始。$\square$

令 $T_F(s,w)$ 为通过运行有限事件词 $w$ 获得的有序结果列表，使用每个结果的状态作为下一个输入。类似地为控制器定义 $T_G$。

定理 4.3（有限记录）。 对每个有限 $w$，

$$ \operatorname{map}(\alpha_O,T_F(s,w)) =T_G(\alpha(s),\operatorname{map}(\epsilon,w)). $$

如果 $V(\alpha(s))$ 成立，则 $T_F(s,w)$ 中的每个结果状态也满足该谓词。

证明。 对词进行归纳。定理 4.2 识别第一个结果和后续控制；在那里应用归纳。命题 3.1 提供后续不变量。Lean 检查 transcript_refines 和 transcript_valid，保留被拒绝的自环及其观察。$\square$

推论 4.4（路径解释）。 考虑有向转移图，其顶点是有效的完整状态或控制状态，其边保留类型化事件及其规范化结果。擦除定义了它们自由路径范畴之间的函子。它保持恒等和有限路径拼接。

证明。 定理 4.2 给出具有正确端点的边映射，命题 3.1 保持端点有效。将边映射扩展到词。空词映射到空词，映射拼接就是拼接映射后的词。定理 4.3 识别相应的观察。$\square$

这是对已检查列表定律的书面范畴论解释，不是形式化的 Lean Functor、等价或更高相干定理。它提供了与 [1] 相关的集合值片段。

5. 已检查的运行时门

定义 5.1（门）。 对于提议的完整结果 $o$，定义

$$ \Gamma(s,e,o)= \begin{cases} \operatorname{some}(o),&o=F(s,e),\\ \operatorname{none},&o\ne F(s,e). \end{cases} $$

相等包括每个完整状态字段、接受和规范化原因。状态相等使用载荷字符串本身，而不仅仅是摘要或控制投影。匹配的被拒绝结果是成功的门检查；门不匹配是中止调用的错误。

定理 5.2（门可靠性和完备性）。 如果 $\Gamma(s,e,o)=\operatorname{some}(u)$，则 $u=F(s,e)$。模型结果总是通过。不同的提议产生 none。

证明。none 分支无法产生 some。在另一分支中，相等性测试给出 $o=F(s,e)$，而 some 的单射性给出 $u=o$。剩余两条陈述是同一测试的真分支和假分支。Lean 检查 gate_sound、gate_complete 和 gate_mismatch。$\square$

因此，从匹配状态和类型化事件流得到的成功检查给出模型的完整结果，并由定理 4.3 给出其擦除后的记录。将其应用于原生执行需要第 7 节的信任边界；这不是对未监控 Python 的静态验证。

重配置期间的速度重置可以保留每个控制字段，但无法通过全状态帧检查。双重修订递增和过期接受也会失败。训练胶囊通过提议接口进入；门控不会独立区分它们的目标。

6. 检查点与延续

类型化线路代数具有字符串、自然数、布尔值和有限数组构造子。状态编码是一个包含 13 个字段的数组：一个模式标签、七个字符串、三个自然坐标，以及待处理和已完成数组。每个请求或完成都是一个数组，包含其标识符、修订号和负载字符串。解码器要求完整的模式和精确的构造子模式。它拒绝缺失速度字段，或在需要自然坐标处出现布尔值。

定理 6.1（类型化往返与单射性）。对于每个完整状态 $s$，

$$ \operatorname{decode}(\operatorname{encode}(s))=\operatorname{some}(s). $$

状态编码是单射的。类型化事件编码具有相同的往返性质。

证明。请求和完成的往返直接归约。列表归纳将解码器的左逆提升到映射列表；将其应用于两个状态列表。相等的状态编码随后解码为 some$(s)=$some$(t)$，因此 $s=t$。事件构造子逐个归约。Lean 检查 decodeList_encode、state_roundtrip、encoding_injective 和 event_roundtrip。$\square$

推论 6.2（延续）。如果对 $s$ 的编码进行解码返回 $t$，那么对于每个有限类型化事件字 $w$，有 $T_F(t,w)=T_F(s,w)$。

证明。定理 6.1 确定 $t=s$；在记录中代入。 Lean：decoded_checkpoint_continuation。$\square$

未来的类型化事件包括其数值提议和回执；独立重新运行的内核无需提供相同的提议。运行时测试恢复相同的后端和完整状态。仅参数导出会丢弃内存和控制字段，并且没有这样的延续声明。

7. 可执行桥接与信任边界

该工件包含一个 NumPy 参考解释器和一个针对共享参数块的 JAX 降级

$$ H=\tanh(XW+\mathbf1b^T),\qquad Y=X+HW+\mathbf1b^T. $$

动量训练对平方损失使用 $v'=\beta v+\nabla L(\theta)$ 和 $\theta'=\theta-\eta v'$。新的 CheckedRuntime 首先计算 Python 提议，规范化类型化事件和状态，并将两者发送到本地控制器。控制器调用实际编译的 checkedGate 定义。Python 仅在匹配响应、全状态恢复检查和擦除观察检查之后才提交。门控不一致、服务不可用或响应格式错误会在会话更新其状态或追加正常转换记录之前引发错误。不存在静默的未监控回退。

已接受的特征事件在胶囊构造之前将输入列表规范化为拥有的 float64 数组。负整数完成请求始终是未知的；适配器通过同一陈旧观测的未使用下一个标识符来表示它们。其他格式错误的标识符类型具有域观测。原始尝试事件保留在 Python 审计日志中。类型化事件编解码器定理涉及类型化事件，而不是此原始输入规范化的单射性。

经检查的源代码导入捆绑的 Std，且不需要 Mathlib。Lean 4.19.0 在 Correspondence.lean 中检查了 21 个新定理声明；未更改的第一内核提供了 14 个较早的定理。没有证明漏洞或自定义应用公理。打印的传递依赖包括标准 propext 和 Quot.sound。编译后的程序使用经检查的转换和门定义。Lean 编译器、C 编译器/链接器、原生执行、JSON 解析器/打印器、Python 适配器和数值域接收计算仍然可信。构建报告将当前源摘要绑定到控制器摘要；这是相对于可信摘要的完整性记录，而不是身份验证或编译器正确性证明。

具体的 JSON 和 Python 到线路的往返经过测试，但未证明，包括 $2^{80}$ 个标识符、转义负载、格式错误的元数以及布尔/自然数区分。运行时是单线程且同步的；数值内核、资源耗尽、并发和外部效应不在证明范围内。

8. 可复现证据

使用了 Python 3.12.14、NumPy 2.3.5 和 CPU JAX/JAXlib 0.4.38。依赖版本、源代码、控制器哈希和输出随工件提供。相同 JAX 固定版本的新的隔离安装解决了先前的 JIT 进程崩溃；其原因尚未确定，失败已被记录。本地 Lean 构建使用了有记录的仅启动进程路径适配器；官方内核和库未更改。原生控制器在没有该适配器的情况下运行。故意错误的等式被拒绝，作为证明检查器的阴性对照。

• 组合套件。 结果和范围：45 个测试通过，无跳过；包括原始数值检查、检查点恢复和实时门测试。
• 有界模型/适配器枚举。 结果和范围：4,184 个有效控制和 124,064 个转换与独立的 Python 表一致；计数器 0-3、修订 0-2、容量 0-3、提议容量 0-4；两个注册的后端标签；所有待处理/已完成的排序和允许的完成修订。
• 生成的实时运行时。 结果和范围：300 个种子事件产生 300 个匹配的门检查；80 个被接受；端点有效，每一步都经过验证。
• 集成轨迹。 结果和范围：NumPy 启动和 JAX 启动运行均有 42 个匹配检查，38 个接受和 4 个拒绝，31 次更新和 62 条目标查询记录。
• 数值比较。 结果和范围：观察到的最终参数/速度最大差异 $1.12\times10^{-16}$（向上取整），在声明的 $2\times10^{-11}$ 容差范围内。
• 缺陷注入。 结果和范围：双重修订、陈旧接受和速度重置被阻止；中断的会话不会提交提议的转换。

枚举中既包含回执值、受支持的事件种类、未知完成、非法容量变更、缺失后端，也包含显式的 domain/unsupported 事件。该枚举中的数值载荷是符号性的；它并非对实数或浮点数组的穷尽测试。这些实测运行既未确立统一的数值精化界，也未确立一般优化器收敛性。

9. 校正感知的兼容性

所提供的源代码发布保留了原始手稿和示例，并记录了其有界检查的重新运行。本期刊附件保留了可执行示例；历史手稿和完整的早期 ZIP 仍保留在源代码发布中，不在本附件内。台账保留其五条旧记录，并新增 C006（精确的自然工单元数据）、C007（更强的控制器/编解码器/门控范围）和 C008（一个未发布的原始列表/规范化数组适配器缺陷的见证）。

早期结果保留其适用的假设；无效断言保留见证和替代项，而非真理性主张。旧队列的未知完成自环并未指定新的陈旧观测。台账记录的是研究谱系，而非所有新旧理论的等价性。

10. 主张与剩余义务

已完成的里程碑证明了精确擦除、离散不变量、载荷帧、门控健全性和类型化编解码器定律，并使用经过测试的适配器执行门控。静态 Python 验证、经验证的 JSON/提取、真实逆向正确性、统一的浮点保护裕度以及更高一致性仍是各自独立的义务。

自动化披露。 OpenAI ChatGPT/Codex 协助了实现、证明开发、手稿起草、参考文献核对和工件验证。提交所有者授权了匿名署名和提交。未主张任何独立审稿报告或录用决定。

参考文献

1. Anonymous. Higher Lenses and Temporal Descent for Certified Adaptive Systems. Higher Categorical Semantics (2026), editorially reviewed. 历史源代码发布包含版本 1.1。 2. Anonymous. LensIR: Compositional Reverse Semantics for a Typed Tensor Fragment. 未发表的配套手稿，版本 1.1 (2026)；保留在历史源代码发布中。 3. Anonymous. Oracle and Jet Semantics of Stateful Optimization. 未发表的配套手稿，版本 1.1 (2026)；保留在历史源代码发布中。 4. Xavier Leroy. *Formal verification of a realistic compiler*. Communications of the ACM 52(7), 107-115 (2009). doi:10.1145/1538788.1538814. 5. Amir Pnueli, Michael Siegel, and Eli Singerman. *Translation validation*. TACAS 1998, LNCS 1384, 151-166. Institutional record. 6. Leonardo de Moura and Sebastian Ullrich. *The Lean 4 Theorem Prover and Programming Language*. CADE 28, LNCS 12699, 625-635 (2021). doi:10.1007/978-3-030-79876-5_37. 7. JAX developers. Forward- and reverse-mode autodiff in JAX. 实现版本已固定在工件中；所链接的文档为当前版本。