The Double Life of Code World Models: Provably Unmasking Malicious Behavior Through Execution Traces

arXiv 25.12 2025 39.8 method

TLDR

A protocol using semantic orbit analysis of execution traces to detect backdoors in LLM-generated code, with theoretical guarantees but high false positives.

Reasoning

The paper introduces a novel verification framework (CTVP) with strong theoretical foundations (non-gamifiability, information-theoretic bounds), which is a strength. However, the abstract acknowledges high false positive rates and practical deployment challenges, limiting immediate applicability. The core contribution is about code verification, not world models.

Read-first score

Read-first score 39.8, weighted from topical fit, citation, graph, method, reproducibility, and recency signals. Original total remains 1.

Methodology quality 25%

Screens visible abstract and analysis fields for experiment, dataset, baseline, metric, and limitation evidence. markers=analysis,baseline,evaluation,validation

Recency 8%

86.7

Uses a gentle age decay so recent papers surface without erasing older foundations. 2025

Reproducibility 25%

Screens links and visible text for paper, code, dataset, artifact, and repository signals. pdf=True; code=False; dataset=False; markers=code

Topical relevance 42%

1.4

Uses existing LLM keyword relevance scores normalized to 0-100. world model,world simulator,generative world model,interactive world model,video world model,world dynamics prediction,model-based reinforcement learning world model

Field roles

FrontierMethodology anchor

Rank sensitivity

Stability: volatile; rank range: 390.

Keyword Scores

world model

world simulator

generative world model

interactive world model

video world model

world dynamics prediction

model-based reinforcement learning world model

Deep Analysis

Innovations

Cross-Trace Verification Protocol (CTVP) for detecting backdoors in code-generating LLMs without direct execution
Semantic orbit analysis using model-predicted execution traces across semantically equivalent program transformations
Adversarial Robustness Quotient (ARQ) quantifying verification cost relative to baseline generation, showing exponential growth with orbit size
Theoretical non-gamifiability proof based on information-theoretic bounds and space complexity constraints

Methodology

CTVP verifies untrusted code-generating models by leveraging the model's own predictions of execution traces across multiple semantically equivalent program transformations. It analyzes consistency patterns in these predicted traces to detect behavioral anomalies indicative of backdoors, without directly executing potentially malicious code.

Key Results

The Adversarial Robustness Quotient (ARQ) demonstrates exponential growth with orbit size, and theoretical analysis establishes information-theoretic bounds showing non-gamifiability. However, initial evaluations reveal high false positive rates that need to be addressed for practical deployment.

Limitations

High false positive rates observed in initial evaluations
Practical deployment requires addressing the high false positive rates
Limited empirical validation implied by 'initial evaluations'

Resources

Paper