查询即计算：机器之外的Oracle计算及其在智能体上的应用 We Query, Therefore We Compute: On Oracle Computation beyond the Machine, with an Application to Agents
把LLM当作Oracle接入双栈自动机，推导出操作系统，统一Agent与Workflow
前置知识
双栈下推自动机（2-PDA）与图灵完备性
下推自动机是带一条栈的有限状态机，只能识别上下文无关语言；若给它两条栈，两条栈可分别充当图灵机纸带在读写头左右两侧的部分，因此2-PDA与图灵机计算相同的函数，是图灵完备的。本文把2-PDA写成push/pop/jeq/halt风格的程序，栈还可以用分隔符切分成任意多个逻辑栈。
整台O-2-PDA-TS机器的底座就是这台写成程序的2-PDA，Priestess（图灵完备部分）的全部推导都建立在它上面，不理解2-PDA就无法理解栈、颜色与局部性引理。
Oracle图灵机与相对化（relativization）
图灵1939年提出的oracle机：一台图灵机外加一个黑箱Oracle，机器可以询问Oracle问题并获得回答，对Oracle内部不做任何假设。相对化方法让证明对每一个Oracle都成立。本文的关键改动是：查询不是写在单独查询带上，而是整条栈的内容，答案追加回同一条栈。
本文全部核心定理（内核契约、安全边界）都带"对每一个Oracle"的量词，这正是相对化带来的证明强度；理解Oracle作为黑箱的语义才能分清哪些结论不依赖LLM的任何内部性质。
自回归生成与KV缓存（prefill/decode）
语言模型每次调用读取全部历史并逐token生成，历史只增不减；推理引擎把每个前缀的注意力键值状态缓存在KV cache里：新前缀未缓存的部分要prefill重算，已缓存部分decode直接续写，vLLM/SGLang等系统用分页和前缀树共享KV缓存。
论文把"程序只追加时历史自回归生长"和"一次Oracle调用是KV缓存上的一层缓存层级"作为连接抽象机与真实推理系统的桥梁，缓存模型的每token一次计算、prefill/decode分工都依赖这些概念。
Call-by-push-value（CBPV，按值推送调用）
Levy提出的一种计算类型论，把类型分为值类型（静态存在的数据）与计算类型（会运行的东西），用 $\mathbf{thunk}\,M$ 把计算挂起为值、用 $\mathbf{force}\,V$ 运行挂起的计算。它给出了"存储内容何时被当数据读、何时被当程序执行"的精确词汇。
本文用CBPV片段给机器的栈单元分型：O色栈上内容可以是thunk（Oracle要运行的程序），P色栈上只能是数据。存储对称性破缺S、uret指令的force语义、答案永不自动获得执行权的结论都靠这套词汇陈述。
特权级、陷入（trap）与系统调用
处理器用特权级区分内核态与用户态：用户程序只能通过陷入（trap）到固定入口请求内核服务，xRET类指令从陷入返回；SMEP/SMAP等机制禁止内核执行或直读用户页，保证代码段与数据段分离。
转移对称性破缺T引入的O-mode/P-mode正是"用户态/内核态"在抽象机上的对应物：屈服符$\natural$触发的yield trap就是系统调用，uret对应xRET，取指条件对应SMEP。ArchNights的Oracle模式就插在用户态之下。
研究动机
智能体系统爆发式增长后其研究正变得系统化，但作者指出头顶飘着"两朵乌云"。第一朵是基础缺失：现有工作要么走形式化路线（$\lambda$A、ZipperGen、LLMbda、Calculus of Intelligence、运行时规则语言AgentSpec），定义语言并证明程序不能做什么；要么走结构类比路线（AIOS、两个AgentOS、AOS、把智能体实现为宿主POSIX进程的Quine），从操作系统逐块借用调度、缓存、隔离等抽象。类比的理论只能到达类比所及之处，没有一个工作说明"某部分凭什么成为另一部分的操作系统、又保证什么"。以缓存为例：智能体构建者眼中的缓存是程序保留复用的上下文，模型服务者眼中的缓存是注意力状态即KV cache，两种说法各自正确、都解决了实际问题，却缺乏可陈述和检验的共同基础。第二朵是统一缺失：Workflow与Agent通常从其一出发各自研究——FMOS把两者当作共享原语上的两种执行形式但在接口处假设虚拟化条件；Harness as a Language从单一原语派生两者却不定义操作系统；具体机制（工具调用期间任务状态的保留/丢弃/换出与Workflow前缀的按需预取）瞄准同一区间却在两种形态下被重复研究，作者借Levy之口称这种重复劳动"令人厌倦"，还让系统显得任意。
本文的目标是本文的目标是构造一台抽象机器，为智能体系统提供共同基础与统一视图。具体而言：把LLM当作Oracle，用一条指令接入图灵完备的双栈下推自动机；通过两次对称性破缺从机器规则中推导出"谁是谁的操作系统"，使内核契约、跨越不变量、缓存模型和安全边界成为对每一个Oracle都成立的不变量；在同一台机器上把Agent与Workflow统一起来，让缓存与调度等机制一次建模、两种形态通用；最后用构造V把机器装进冯·诺依曼计算机，给出扩展RISC-V指令集与Linux风格内核的原型ArchNights（在gem5上运行），证明该机器可以实现并足以充当智能体框架（harness）的基础。最终愿景是让智能体系统能像计算机系统那样被设计——每个设计决策从不变量和界出发论证，并附带其成立条件。
与已有工作不同的是，本文的独特切入是"推导而非类比"。以往工作把模型放在借用概念所处的位置——AIOS视模型为资源、AgentOS视模型为内核、MemGPT视模型加上下文为计算机、Quine视智能体为宿主进程——位置由类比决定；本文则从图灵1939年的oracle机出发，但做了一个关键改动：查询不是写在独立查询带上，而是整条栈的内容，答案追加回同一条栈，于是自回归形态属于程序与Oracle的交互而非模型本身。随后不再增加任何公理，仅通过打破双栈颜色的对称性（存储S与转移T），让操作系统的存在从转移规则中自动浮现，契约成为对每个Oracle（含对抗性回答）都成立的机器不变量。作者明确声明其主张的边界：只说所引工作没有同时给出"对每个Oracle的量词"与"在同一台机器上派生出的操作系统"这两样东西，而非断言没有其他形式化能够做到。
核心方法
直觉上，一次LLM智能体会话就是：整段历史作为查询发给模型，模型输出与工具结果追加进历史，如此往复——这正是本文抽象机的行为。技术路线分四步。第一步构造O-2-PDA：把双栈下推自动机写成程序（push/pop/jeq/halt），加入指令 oracle s le，它把栈 $s$ 的全部内容经编码器 $E$ 送给Oracle，答案经解码器 $D$ 追加回 $s$；只要程序只追加，历史就按 $Q_{t+1} = Q_t \cdot r_t \cdot p_t$ 自回归生长（命题2.7）。第二步用CBPV片段给存储内容分型（数据 $D$ 或挂起计算 $U\,B$），再做两次对称性破缺：S规定P色栈上一切皆数据、只有O色栈可容纳Oracle运行的程序；T引入O-mode（Oracle连续自查询、无Priestess指令穿插，直到答案以屈服符 $\natural$ 结尾则陷入唯一标签 $\ell_{trap}$）与特权P-mode，得到O-2-PDA-TS。第三步从规则推出内核契约K1–K4与跨越不变量，定义操作系统=内核+库，Agent与Workflow成为任务程序在机器上的两种摆放。第四步对内部自回归（AAR）Oracle打开黑箱：经编解码器在Step/Frame粒度同步两个自回归过程，把一次Oracle调用写成答案缓存套状态缓存套编码缓存的层级，给出调度代价与安全边界；最后构造V把机器装进冯·诺依曼计算机（栈变内存段、Oracle操作化为一条指令、O-mode仅运行AAR Oracle），并在gem5上实现为ArchNights。
核心创新有三。其一，一条指令 oracle s 造成"查询即整栈、答案回写同栈"，使得自回归形态（历史只增长）属于交互而非模型：不需要对模型内部做任何假设，语言模型的chat式使用自动落入此形态，命题2.7保证 $Q_{t+1}=Q_t\cdot r_t\cdot p_t$。其二，操作系统的存在是两次"最小"对称性破缺的推论而非设计选择：命题3.12证明，在"不对程序施加任何条件"的前提下要让任务的两种摆放（程序在Oracle侧或在Priestess侧）都存在且不互相混淆，唯一的选择就是S加T（或其颜色互换）。于是内核契约K1–K4（游程只追加写自己的栈、只读自己的栈、控制只在 $\ell_{trap}$ 返回、答案对Priestess永远是数据）成为对每个Oracle、每个程序、每段运行都成立的机器不变量——与seL4/CertiKOS"先写规范再证明内核"不同，这里的契约是从规则免费派生的。其三，同一次转移有两种读法（Priestess侧是force、Oracle侧是return），Agent与Workflow因此不是两种系统，而是同一架构上任务程序的两种摆放；命题3.11的解释器与编译器保证两种摆放互译，且保证在任一侧都成立。
方法步骤详情
第一步：定义程序式2-PDA（配置=标签+存储，指令push/pop/jeq/halt），引理2.2允许把物理栈切分为多个逻辑栈并保持可观测步语义。第二步：给栈着色（a为P、b为O），派生栈继承颜色。第三步：加入Oracle三元组 $(A,E,D)$ 与指令 oracle s le，定义答案映射 $\mathcal{O}(w)=\{D(y):(E(w),y)\in A\}$，编码拒绝则跳转 le，得到O-2-PDA，并证明它与同Oracle的oracle图灵机计算相同的偏函数。第四步：命题2.7证明只要程序在两次查询间对 $s$ 只push/jeq，历史满足 $Q_{t+1}=Q_t\cdot r_t\cdot p_t$。第五步：CBPV分型后施加S（P栈全为D型）与T（O-mode/P-mode、屈服符 $\natural$、陷入标签 $\ell_{trap}$、指令uret），得O-2-PDA-TS。第六步：定理3.4证内核契约K1–K4，推论3.5证内容只经force/return跨越两态；预算 $\beta$ 下在好机器上证K5控制必返回。第七步：定义3.8给出操作系统=内核+库（声明 $\delta_\Lambda$、请求语言 $L_\Lambda$），定义3.10区分Agent/Workflow/混合三种摆放。第八步（§4）：定义内部自回归Oracle与Step/Frame接口，引入损失 $\mathrm{loss}_E(w,v)=|E(w)|-\mathrm{lcp}(E(w),E(wv))$、在 $\natural$ 处因子化与Frame保真两条件，定理4.4证双向Frame同步；把一次调用写成层级 $C_O \triangleright D\circ G_\rho \circ \langle\hat{s},C_{\hat{s}}\rangle \circ \langle E,C_E\rangle$，命题4.9/4.10给出"超额重算=编码损失"与"每token只算一次"，命题4.11给出不知返回时间的2倍代价，定理4.12与命题4.13给出安全边界。第九步（§5）：构造V——栈变为带基址/栈顶/界限的内存段、Oracle操作化为一条指令、O约束（仅AAR Oracle可入O-mode）、取指条件（类SMEP）。第十步（§6）：RV64扩展出Oracle模式与PROBE/STEP/RUN/uret指令，内核PRTS实现fork/exec/调度/检查点/swap与操作符库，在gem5 SE模式运行并评测。
技术新颖性
技术新颖性在于组合而非任何单个配料：oracle机、双栈、整栈查询、不受信Oracle、模型背后的指令、学习函数作为指令都有先例，但"整栈查询+答案回写同栈"的下推自动机、"由对称性破缺推导出操作系统"、"契约对每个Oracle成立"三者并存前所未有。与形式化路线（$\lambda$A、LLMbda定义语言与类型）相比，本文不定义语言而定义机器，语言可以叠加其上且保证互不冲突：契约仲裁空间与控制，标签系统仲裁信息流。与结构类比路线相比，模型的位置由S和T的排序唯一决定而非任意选择：Agent形态下Priestess是操作系统，特权反转后同一构造给出人机交互与自动化系统两象限。与FMOS相比，虚拟化条件在这里由规则自动成立而无需接口假设；与Quine相比，操作系统的位置从宿主内核下移到Oracle与Priestess之间。缓存模型把vLLM/SGLang的前缀复用与CPU缓存层级纳入同一套函数-存储演算，一次陈述覆盖两种形态，这是Agent侧状态管理与Workflow侧前缀调度两条文献线此前未曾共享的。
实验结果
理论结果：定理3.4证明内核契约K1–K4对每个Oracle、每个程序、每段运行成立（K1游程只追加写自己的栈；K2只读自己的栈；K3控制只在 $\ell_{trap}$ 返回；K4答案对Priestess永远是数据，绝不成为代码地址）；命题3.7在预算与好机器下补上K5（游程在 $\beta$ 次O-mode转移内必然返回）；命题3.12证明S与T是保持两种摆放分离的唯一最小选择；定理4.4在 $\natural$-因子化加Frame保真下证得机器侧历史与Oracle内部历史逐Frame同步；命题4.9证明状态缓存的超额重算恰为编码损失 $\mathrm{loss}_E$，Frame边界处损失为零；命题4.10证明append-only纪元内私有状态缓存使每个token恰好计算一次（Priestess写的部分prefill、Oracle写的部分decode）；命题4.11证明不知返回时间 $T$ 的最优确定性保留策略最坏花费 $2\,\mathrm{opt}(T)$，其中 $\mathrm{opt}(T)=\min(\mu T, R)$，阈值 $\theta=R/\mu$ 时恰取2倍，随机化下界为 $e/(e-1)$；定理4.12与命题4.13证明：对每个Oracle成立的保证只能固定内容"在哪"跨越边界而非"什么内容"跨越——这解释了为何本机不是prompt injection的防御、却给出每个防御的安放位置。实现结果：ArchNights-SE在gem5 SE模式运行完整发行版（PRTS内核、系统库、init、shell）；Terminal-Bench 2.1共89题、每题1试（1题1.1分）、Oracle为deepseek-v4.1-flash，ArchNights-SE得77.5–83.1 Pass@1（最小系统+额外prompt为83.1，最小与完整系统的默认prompt均为77.5），同设置下mini-swe-agent为80.9、Terminus 2为78.7；厂商在自家设置下同harness（mini-swe-agent）报90.3，存在9.4分的设置差距。演示：加虚拟显示器与音频输出后，ArchNights-SE制作了 world.execute(me); 的音乐视频，证明该机器同时是智能体系统与通用计算机。
查看结构化数据
| 任务 | 指标 | 本文 | 基线 | 提升 |
|---|---|---|---|---|
| Terminal-Bench 2.1（89个终端任务，每题1次尝试） | Pass@1 (%) | ArchNights-SE：最小系统+额外prompt 83.1；最小系统默认prompt 77.5；完整系统默认prompt 77.5 | 同模型同设置：mini-swe-agent 80.9；Terminus 2 78.7。厂商自报（自家设置）：mini-swe-agent 90.3，八个harness配置区间84.1–90.6 | 对本设置基线为 -3.4 到 +4.4 个百分点（每题1.1分）；与厂商同harness差距9.4分，归因于评测设置而非机器本身 |
| Agent任务的前缀复用（命题4.10，append-only纪元） | 每个token的预计算次数 | 私有状态缓存下每token恰好计算1次（Priestess写入prefill、Oracle生成decode） | 黑箱Oracle只有整史答案缓存，纪元内历史严格增长导致零命中，每token需重编码整段历史 | 每token成本从 $O(|Q_t|)$ 降到 $O(1)$（Frame边界处损失 $\mathrm{loss}_E=0$；开放式Frame内至多回溯 $L_{GE}$ 个符号） |
| 工具调用期间任务状态的保留/丢弃决策（命题4.11，租或买问题） | 相对最优成本 $\mathrm{opt}(T)=\min(\mu T,R)$ 的竞争比 | 已知返回时间 $T$ 的策略恰达 $\mathrm{opt}(T)$；不知 $T$ 时确定性最优阈值 $\theta=R/\mu$ 最坏2倍 | 不知返回时间的任意确定性保留策略 | 给出精确因子2的不可改进界（随机化策略可降到 $e/(e-1)$，机器额外给出重建成本 $R$ 的缓存学定义） |
局限与改进
作者承认的局限：全文不证任何时间/空间复杂度界，一次偏离可耗尽任意预算；机器是同步的，不含并发、容错与恢复；ArchNights只是"按设计实现"，没有精化（refinement）证明；真实语言模型输入有界，机器一般不是好机器，ArchNights靠把故障吸收为陷阱来保住K5；在 $\natural$ 处因子化与Frame保真是逐tokenizer、逐模型的实现性质，文中未对所用模型验证；Lynchpin假设（历史越长下一次调用越可能出错）只是工作假设；chat接口隐藏Step数（命题4.6）；ArchNights-FS与ZOOT仅是设计，未构建未验证；本文不给安全保证，安全边界不防prompt injection，只能告诉防御应放在哪里。我补充的观察：评估为单模型、每题单次试验，harness对比引入的9.4分差距无法归因（厂商不公开其prompt）；PRTS的正确性是设计保证而非证明，与seL4式验证尚有距离；语义委托"结果等价"的义务是非形式化的；O-mode由微码执行的硬件成本未量化；所有语句针对可能运行的集合而非概率分布，缺少对采样随机性的定量分析。
独立分析的弱点
弱点一：缓存结论（命题4.9/4.10）依赖四个理想化假设——tokenizer在 $\natural$ 处因子化、Frame保真、内核纪元纪律、内核写入以 $\natural$ 结尾；真实BPE只在词典决定的有界前瞻内稳定，chat模板的服务端重渲染会破坏前缀链，实际部署前需逐tokenizer审计。改进方向：提供可执行的因子化/保真检查器，或在服务端用约束解码强制Frame保真。弱点二：2倍调度界假设保持成本 $\mu$ 与重建成本 $R$ 为常数，且未纳入换出（swap）这第三选择与缓存有限容量；可延伸到带返回时间预测的策略（如运行中工具上报）并给出有限容量下的分析。弱点三：机器无时钟，一次Oracle调用的墙钟延迟在模型之外，而真实harness的并行与异步收益恰恰来自延迟；异步实现被列为开放问题。弱点四：单处理器、单陷阱标签，多核扩展（义务表I-9/I-10行）只有调度不变量设想。弱点五：契约不约束Oracle内部，投机执行等Oracle内侧信道（附录C只作讨论）无界。弱点六：评估只覆盖代码型终端任务，缺少多智能体、长程任务和人机交互（人作为Oracle）的定量案例。
未来方向
作者列出的方向：机器层面——复杂度界、精化证明、异步性、Priestess内部多用户隔离、前缀之外的缓存复用、有限容量、非内部自回归Oracle的接入；原型层面——微码或OS层面的异步实现、多处理器内核、构建并验证ArchNights-FS/ZOOT（候选方案是修改KVM以支持宿主驱动的Oracle硬件）；语言模型层面——逐tokenizer、逐模型检验 $\natural$-因子化与Frame保真，用随机Oracle设定研究Lynchpin假设，量化语义委托何时有益；下一步是AgentNights：在宿主软件中直接实现机器、内核与系统库（不经模拟器），并结合更广泛的harness质量评估。基于本文成果可延伸的：对PRTS做seL4/CertiKOS式精化验证（契约恰好是规范中机器已免费提供的部分）；把随机Oracle机（SOTM）系列的期望成本与认证界搬到本机，给出概率化的缓存与调度分析；实现Workflow到Agent的编译器，并按缓存模型为上下文压缩/截断策略定价；把O-mode推广到视觉-语言-动作模型等自回归Oracle，使机器人控制任务也纳入同一机器。
复现评估
复现前景较好但代码尚未放出：文中明确说ArchNights-SE"will be open source"，基准Terminal-Bench 2.1公开可得，Oracle是deepseek-v4.1-flash（API可用），gem5 SE模式是体系结构社区的标准模拟器，算力需求主要是模型API调用，单机即可完成。理论部分自足：附录B、C给出全部构造与证明，定义-命题链条完整，作者也指出在完整CBPV演算下的严格化与机械化是明确留出的工作，适合用Lean/Coq/Isabelle重做。难度主要在工程量：完整发行版包含内核PRTS、系统库、init、shell与操作符表，表5/6列出的约20条实现义务需逐条满足；此外要复现83.1那一档需小心对齐额外prompt的两条规则、超时与半在线代理设置——作者自己承认与厂商评测的9.4分差距无法完全归因，因此分数层面的精确复现有一定不确定性，而机器行为与理论命题层面的复现是确定的。
论文图表
附录D中shell会话循环的流程图：P-mode侧session读取用户输入的一行（经Human类Oracle调用，答案为数据），写入历史后uret进入O-mode让Oracle作为shell程序继续运行，直到下一个yield trap返回。
具体展示shell作为混合形态（定义3.10）如何同时使用O-mode与P-mode，是Agent/Workflow混合体的一手实例。
附录D中以记录为单位给出一次真实ArchNights-SE会话历史的缩略示意，蓝色方块等记号区分Priestess写入与Oracle追加的记录及 $\natural$ 结尾。
把抽象的"历史=任务程序"落到可见的记录序列，帮助读者对照Figure 1理解真实系统的历史布局。