GenOS: Compositional Certificates for Semantic Robustness in AI Code Generation
- URL: http://arxiv.org/abs/2608.03588v1
- Date: Tue, 04 Aug 2026 12:42:11 GMT
- Title: GenOS: Compositional Certificates for Semantic Robustness in AI Code Generation
- Abstract summary: GenOS is a probabilistic operational semantics for replacing a prompt, contract, generator, or program.<n>We prove that equivalence-compatible kernels descend to quotient classes and that quotienting commutes with distributional extension and sequential composition.<n>We also establish workflow bi-commit safety under sound validation, total-variation non-expansiveness, and an additive bound.
- Score: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: 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.
Related papers
- Probabilistic Model Checking of Autoregressive Neural Sequence Models [4.570003973862485]
Test-set accuracy is silent on two issues that matter when deploying autoregressive neural sequence models.<n>How much probability mass the system under test places on constraint-violating alternatives that are reachable under sampling.<n>We answer both with probabilistic model checking.
arXiv Detail & Related papers (2026-09-01T07:37:55Z) - Structuring Semantic Embeddings for Principle Evaluation: A Prototype-Guided Contrastive Learning Approach [58.15427952222424]
General-purpose text embeddings are widely deployed for such tasks, but broad semantic similarity can place semantically similar yet task-distinct examples.<n>We introduce Prototype-Guided Contrastive Learning (PGCL), a prototype-guided geometric regularization module built on top of frozen text embeddings.
arXiv Detail & Related papers (2026-08-15T13:19:25Z) - AEVAL: From Anecdotal to Deterministic Testing for Agentic Skill Workflows [1.6785141970297952]
AEVAL (Agentic Evaluation) is a CI-integrated framework that replaces this practice with a deterministic, reproducible test pipeline for agentic skills.<n>Every skill change triggers a test event: the skill runs against a developer declared evaluation contract inside an automated executor.<n>A key ingredient is a structural separation between executor and grader, preventing a subtle but pervasive failure mode.
arXiv Detail & Related papers (2026-07-16T21:33:05Z) - The Token Not Taken: Sampling, State, and the Variability of AI Agent Outputs [0.0]
Agentic AI systems can behave differently across runs.<n> variability arises from several layers that are often conflated.<n>This manuscript clarifies what it means to call agentic AI systems, when such variability can be reproduced under matched conditions.
arXiv Detail & Related papers (2026-06-08T03:53:55Z) - Mitigating Bias in Locally Constrained Decoding via Tractable Proposals [73.78736135699953]
Existing locally constrained decoding approaches enforce constraints by myopically masking out next tokens.<n>Recent work uses sequential Monte Carlo methods to mitigate such biases, but designing effective proposal distributions or potential functions remains a key challenge.<n>We propose a generic approach to construct proposals and potentials for SMC sampling from $p_mathrmlm( cdot mid mathrmconstraint)$.
arXiv Detail & Related papers (2026-06-01T08:58:18Z) - Correction and Corruption: A Two-Rate View of Error Flow in LLM Protocols [51.56484100374058]
We propose a paired-outcome measurement interface for auditing a single protocol step on exact-match tasks.<n>For each instance, the interface records a baseline correctness bit and a post-step correctness bit.<n>These rates predict accuracy changes and define a reusable empirical interface testable across seeds, mixtures, and pipelines.
arXiv Detail & Related papers (2026-04-20T13:25:40Z) - Zonkey: A Hierarchical Diffusion Language Model with Differentiable Tokenization and Probabilistic Attention [0.0]
Zonkey is a hierarchical diffusion model that addresses limitations through a fully trainable pipeline from raw characters to document-level representations.<n>At its core is a differentiable tokenizer that learns probabilistic beginning-of-sequence (BOS) decisions.<n>Zonkey generates coherent, variable-length text from noise, demonstrating emergent hierarchies.
arXiv Detail & Related papers (2026-01-29T14:17:37Z) - Scaling the Scaling Logic: Agentic Meta-Synthesis of Logic Reasoning [18.75349680577575]
SSLogic is a framework for continuous family evolution with controllable difficulty.<n>Training on SSLogic-evolved data yields consistent gains over the seed baseline at matched steps.
arXiv Detail & Related papers (2026-01-23T13:26:01Z) - Taming Imperfect Process Verifiers: A Sampling Perspective on Backtracking [54.43083499412643]
Test-time algorithms that combine the generative power of language models with process verifiers offer a promising lever for eliciting new reasoning capabilities.<n>We introduce a new process-guided test-time sampling algorithm, VGB, which uses theoretically grounded backtracking to achieve provably better robustness to verifier errors.
arXiv Detail & Related papers (2025-10-03T16:21:14Z) - The Lie of the Average: How Class Incremental Learning Evaluation Deceives You? [48.83567710215299]
Class Incremental Learning (CIL) requires models to continuously learn new classes without forgetting previously learned ones.<n>We argue that a robust CIL evaluation protocol should accurately characterize and estimate the entire performance distribution.<n>We propose EDGE, an evaluation protocol that adaptively identifies and samples extreme class sequences using inter-task similarity.
arXiv Detail & Related papers (2025-09-26T17:00:15Z) - Reviving Any-Subset Autoregressive Models with Principled Parallel Sampling and Speculative Decoding [55.2480439325792]
In arbitrary-order language models, it is an open question how to sample tokens in parallel from the correct joint distribution.<n>We find that a different class of models, any-subset autoregressive models (AS-ARMs), holds the solution.<n>We show that AS-ARMs achieve state-of-the-art performance among sub-200M parameter models on infilling benchmark tasks, and nearly match the performance of models 50X larger on code generation.
arXiv Detail & Related papers (2025-04-29T06:33:13Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.