PPES: A Probabilistic Execution Semantics for Foundation Models

Foundation models are increasingly deployed as execution engines mediating the mapping from symbolic inputs to concrete actions. Traditional metaphors-treating models as programs, interpreters, or knowledge bases-fail to account for their stochastic, latent, and training-dependent execution behavior. We propose Probabilistic Program Execution Semantics (PPES), a formal framework in which foundation models are interpreted as probabilistic interpreters: runtime programs correspond to prompts, execution states include both observable outputs and hidden latent variables, and transitions are governed by learned parameters 𝜃. Execution is resolved at infer-time, a distinct semantic phase absent in classical computing. PPES provides a rigorous account of key phenomena in foundation-model-based systems, including non-determinism, sensitivity, irreversibility, and historical entanglement. We develop small-step probabilistic semantics, define probabilistic reachability over execution traces, and identify formal properties suitable for metatheoretic reasoning. This framework establishes the foundation for formal verification and reasoning about software systems built atop large-scale foundation models [1-5, 7].