AI 코딩 에이전트(AI coding agents)는 확률적 워크플로(stochastic workflows)입니다. 즉, 프롬프트(prompts)가 해석되고, 결과물(artifacts)이 샘플링되며, 검증기(validators)가 관찰(observations)을 생성하고, 오케스트레이터(orchestrators)가 커밋(commit)하거나 수리(repair)합니다. 따라서 작은 프롬프트나 명세(specification)의 변화는 텍스트가 동의어로 보일 때조차 프로그램 동작 분포(program-behavior distributions)를 변경할 수 있습니다. 기존 시스템들은 정확성(correctness)을 평가하지만, 완전한 에이전트 워크플로(agentic workflow) 내에서 프롬프트, 계약(contract), 생성기(generator) 또는 프로그램을 안전하게 교체하기 위한 구성적 기준(compositional criterion)이 부족합니다.

우리는 이 교체 문제(replacement problem)를 위한 확률적 운영 의미론(probabilistic operational semantics)인 GenOS를 소개합니다. 각 계층(layer)은 마르코프 커널(Markov kernel)로 모델링되며, 각 인터페이스는 관찰자 상대적 동치(observer-relative equivalence)를 가집니다. 우리는 동치 호환 커널(equivalence-compatible kernels)이 몫 클래스(quotient classes)로 내려가며, 몫 구성(quotienting)이 분포 확장(distributional extension) 및 순차적 합성(sequential composition)과 교환 가능하다는 것을 증명합니다. 따라서 동등한 프롬프트는 검증된 커밋(verified commit)을 포함하여 모든 하위 동치 폐쇄 이벤트(downstream equivalence-closed events)에 대해 동일한 확률을 유도합니다.

또한 우리는 워크플로 이심뮬레이션(workflow bisimulation), 건전한 검증(sound validation) 하에서의 가드된 커밋 안전성(guarded-commit safety), 총 변동 비확장성(total-variation non-expansiveness), 그리고 근사 오차(approximation error)를 개별 파이프라인 계층에 귀속시키는 가산적 강건성 경계(additive robustness bound)를 확립합니다. 실행 가능한 삽입 정렬 감사(insertion-sort audit)는 자연어 의역(natural-language paraphrases), 공식 계약(formal contract), 6개의 프로그램, 2개의 관찰자, 그리고 121개의 입력에 대한 철저한 실행을 통해 이 이론을 실체화합니다. 동등한 프롬프트는 동일한 코드 클래스(code-class) 및 커밋 분포를 생성합니다. 인플레이스 계약(in-place contract)에 5%의 확률을 할당하는 프롬프트는 변이 관찰자(mutation observer)에 의해 구별되지만, 하위 거리(downstream distances)는 예측된 경계 내에 머뭅니다. 20,000회의 무작위 유한 커널(finite-kernel) 실험 전반에 걸쳐, 어떠한 정확한 법칙이나 근사 법칙도 위반되지 않았습니다. GenOS는 모델 매개변수적(model-parametric)입니다. 즉, 호환성(compatibility)은 언어 모델(language-model) 동작에 대한 가정이 아니라 테스트 가능한 측정 가능한 속성입니다.