Open Problems in Formal Verification of Modular Compositional AI Systems

We describe an AI architecture in which independently trained expert modules are permanently frozen after creation and dynamically composed through sparse top-K routing in a shared representation space. This architecture differs structurally from standard mixture-of-experts systems in four respects: modules are trained independently (no shared gradients), permanently frozen (immutable functions), dynamically added or removed (open pool), and composed via an explicit sparse graph at each inference step. We present empirical evidence from 260+ experiments suggesting that these structural constraints may enable formal mathematical reasoning about safety-relevant properties, specifically attribution, guaranteed forgetting, non-degradation, memory isolation, and compositional monotonicity, that are intractable in jointly-trained architectures. We state each property precisely and pose open mathematical questions amenable to formal analysis, inviting contributions from the formal methods, learning theory, and information theory communities