Verified World Models Can Still Fail in AI Planning

Large Language Models (LLMs) can generate executable code representing game rules, known as Code World Models (CWMs), which are then used by classical planners. These models are typically deemed adequate if they achieve high transition accuracy on sampled trajectories. However, this paper argues that such prediction accuracy is an insufficient measure of a CWM's true utility for planning. The research presents four key findings. First, a CWM can exhibit 100% transition accuracy and over 98% state accuracy on a planner's search distribution, yet consistently lose in actual gameplay. This "verified-vs-correct gap" occurs because the small percentage of errors often pertains to pivotal game dynamics. Second, this harm follows a quantitative law, where the danger is proportional to the play cost of the omitted rule and inversely related to its rarity. Third, the study shows that increasing training data does not fix this issue, as LLM synthesis acts more as rule translation than rule inference, failing to infer critical omitted rules across different models and data regimes. Finally, the same mechanism applies to belief-inference functions in imperfect-information CWMs, where a verified-but-wrong function can pass accuracy gates but still lead to systematic losses. These results emphasize that adequacy for planning-oriented world models should be measured directly by play performance or on the planner's search distribution, rather than solely by prediction accuracy on sampled transitions.