In plain words: Instead of running suspicious code, the checker asks the model to predict what the code would do across many equivalent rewrites and flags inconsistent answers as possible backdoors. Theory shows no training can fool this check, but early tests produced too many false alarms.
Abstract · The Double Life of Code World Models: Provably Unmasking Malicious Behavior Through Execution Traces
Large language models (LLMs) increasingly generate code with minimal human oversight, raising critical concerns about backdoor injection and malicious behavior. We present Cross-Trace Verification Protocol (CTVP), a novel AI control framework that verifies untrusted code-generating models through semantic orbit analysis. Rather than directly executing potentially malicious code, CTVP leverages the model's own predictions of execution traces across semantically equivalent program transformations. By analyzing consistency patterns in these predicted traces, we detect behavioral anomalies indicative of backdoors. Our approach introduces the Adversarial Robustness Quotient (ARQ), which quantifies the computational cost of verification relative to baseline generation, demonstrating exponential growth with orbit size. Theoretical analysis establishes information-theoretic bounds showing non-gamifiability - adversaries cannot improve through training due to fundamental space complexity constraints. This work demonstrates that semantic orbit analysis provides a theoretically grounded approach to AI control for code generation tasks, though practical deployment requires addressing the high false positive rates observed in initial evaluations.
Subramanyam Sahoo
arXiv:2512.13821 · cs.LG · submitted Dec 15, 2025 · updated Feb 5, 2026
abstract · pdf · html · 13 Pages, A Preprint
It doesn't seem worth it to try to follow the math to see if there is something interesting.