From Specification to Architecture: A Theory Compiler for Knowledge-Guided Machine Learning
Organizations: AI, Optimization and Pattern Recognition Research Group, Faculty of Engineering and Information Technology, University of Melbourne, Melbourne, Australia
Abstract
Theory-guided machine learning has demonstrated that including authentic domain knowledge directly into model design improves performance, sample efficiency and out-of-distribution generalisation. Yet the process by which a formal domain theory is translated into architectural constraints remains entirely manual, specific to each domain formalism, and devoid of any formal correctness guarantee. This translation is non-transferable between domains, not verified, and does not scale. We propose the Theory Compiler: a system that accepts a typed, machine-readable domain theory as input and automatically produces an architecture whose function space is provably constrained to be consistent with that theory by construction, not by regularisation. We identify three foundational open problems whose resolution defines our research agenda: (1) designing a universal theory formalisation language with decidable type-checking; (2) constructing a compositionally correct compilation algorithm from theory primitives to architectural modules; and (3) establishing soundness and completeness criteria for formal verification. We further conjecture that compiled architectures match or exceed manually-designed counterparts in generalisation performance while requiring substantially less training data, a claim we ground in classical statistical learning theory. We argue that recent advances in formal machine learning theory, large language models, and the growth of an interdisciplinary research community have made this paradigm achievable for the first time.
Figures & tables
| Approach | Constraints by Construction | Soundness Certificate | Domain Reusability | OOD Robustness | Zero Human Translation Effort |
| Physics-Informed NNs (PINNs) | ✗ | ✗ | ✗ | ||
| Equivariant Networks | ✓ | ✗ | ✗ | ✓ | ✗ |
| Soft Constraint / Regularisation | ✗ | ✗ | ✗ | ✗ | |
| Causal Generative Models | ✗ | ✗ | ✗ | ||
| Neural Architecture Search (NAS) | ✗ | ✗ | ✗ | ||
| AutoML | ✗ | ✗ | ✓ | ✗ | ✓ |
| Type | Primitive | Module |
| Sym | Symmetry group | Equivariant layer |
| Cons | Conservation law | Hard constraint module |
| Diff | Differential operator | Constrained function class |
| Caus | Causal graph | Structured generative model |
| ⋮ | ⋮ | ⋮ |
| Horizon | Target | Key Challenge | Success Criterion |
| Near term (1–2 yrs) | Single-domain compiler for classical mechanics or molecular symmetries | Decidable type-checking for | Known architecture derived automatically with a machine-checkable soundness proof |
| Medium term (3–5 yrs) | Multi-primitive compiler with LLM-assisted theory parsing | Compositional correctness across interacting primitives | Novel inductive bias synthesised with measured gain in the low-data regime |
| Long term (5 yrs) | Full pipeline from theory specification to verified architecture | Certificates for nonlinearly interacting constraints | Reliable OOD extrapolation across diverse domains |
Scientific ML
Scientific machine learning combines data-driven models with scientific knowledge to analyze, predict, and simulate complex systems.
See all 122 papers