This technical note presents the formal Colored Petri Net (CPN) specification for AXIOM (Automated eXpert for Industrial Output Management), a neuro-symbolic architecture that constrains Large Language Model (LLM) outputs through formal process supervision. The specification defines the complete CPN tuple CPN = (P, T, A, Σ, V, C, G, E, I) for the design supervision workflow, including eight places representing design lifecycle states, six transitions encoding processing steps, five color sets carrying typed design data, and fourteen guard functions implementing physics constraints for lithium-ion battery cell specifications. The CPN uses process supervision (logic control) rather than system simulation, orchestrating the generate-validate-retry cycle while PyBaMM provides physics simulation. Key architectural contributions include: (1) the corrective feedback loop, where structured error messages from failed validation guide LLM regeneration; (2) formal termination guarantees through bounded retry counters; and (3) separation of symbolic verification from neural generation. The specification is implemented in the CellCAD-Python framework with a 346-test validation suite. This document establishes priority for the following novel contributions: (a) the first formal CPN model for supervising LLM-generated engineering outputs in safety-critical domains; (b) the corrective feedback arc as a typed Petri Net arc carrying structured constraint-violation data between symbolic verifier and neural generator; (c) the systematic mapping of fourteen domain-specific physics constraints to CPN guard functions with an associated hallucination taxonomy; and (d) formal proofs of termination, soundness, and boundedness for the neuro-symbolic supervision workflow.
Dumitru-Cristian Leu (Fri,) studied this question.