发表机构
Università di Pisa; Fondazione Start Attractor（比萨大学; Start Attractor基金会）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
GenOS是针对AI代码生成语义鲁棒性的概率操作语义，通过马尔可夫核与等价关系确保工作流中组件替换的安全性，经实验验证其鲁棒性界与兼容性可测性。
AI 中文摘要
AI编码智能体是随机工作流：提示被解析、产物被采样、验证器生成观测结果，而协调器则执行或修复。因此，即使文本看似同义，微小的提示或规范变化也会改变程序行为分布。现有系统评估正确性，但缺乏在完整智能体工作流中安全替换提示、契约、生成器或程序的组合式准则。我们提出GenOS，一种针对该替换问题的概率操作语义。每层被建模为马尔可夫核，每个接口携带与观测者相关的等价关系。我们证明等价兼容的核可降至商类，且商化与分布扩展及顺序组合可交换。因此，等价提示会为所有下游等价封闭事件（包括经验证的执行）诱导相等概率。我们还建立了工作流互模拟、健全验证下的受保护执行安全、全变差非扩张性，以及将近似误差归因于各流水线层的加性鲁棒性界。可执行插入排序审计用自然语言 paraphrase、形式契约、六个程序、两个观测者，以及对121个输入的穷举执行实例化该理论。等价提示产生相同的代码类和执行分布；将5%概率分配给就地契约的提示会被变异观测者区分，而下游距离保持在预测界内。在20000次随机有限核试验中，未违反任何精确或近似定律。GenOS是模型参数化的：兼容性是可测试的可测属性，而非对语言模型行为的假设。
英文摘要
AI coding agents are stochastic workflows: prompts are interpreted, artifacts are sampled, validators produce observations, and orchestrators commit or repair. Small prompt or specification changes can therefore alter program-behavior distributions even when the texts appear synonymous. Existing systems evaluate correctness, but lack a compositional criterion for safely replacing a prompt, contract, generator, or program inside a complete agentic workflow. We introduce GenOS, a probabilistic operational semantics for this replacement problem. Each layer is modeled as a Markov kernel, and each interface carries an observer-relative equivalence. We prove that equivalence-compatible kernels descend to quotient classes and that quotienting commutes with distributional extension and sequential composition. Hence, equivalent prompts induce equal probabilities for all downstream equivalence-closed events, including verified commit. We also establish workflow bisimulation, guarded-commit safety under sound validation, total-variation non-expansiveness, and an additive robustness bound that attributes approximation error to individual pipeline layers. An executable insertion-sort audit instantiates the theory with natural-language paraphrases, a formal contract, six programs, two observers, and exhaustive execution on 121 inputs. Equivalent prompts yield identical code-class and commit distributions; a prompt assigning 5% probability to an in-place contract is distinguished by a mutation observer, while downstream distances remain within the predicted bound. Across 20,000 randomized finite-kernel trials, no exact or approximate law is violated. GenOS is model-parametric: compatibility is a measurable property to test, not an assumption about language-model behavior.
