Executive summary
Henry Kautz’s taxonomy of neurosymbolic AI reaches its most ambitious form in Type 5, where symbolic rules work inside the neural network itself. Frontier models reach the world through interfaces that keep their internals closed, so that version of Type 5 cannot be built on them. This paper asks what Type 5 should mean for models like these, and finds that the ambition survives. A frontier model can be held to hard rules from the outside, with formal guarantees, as long as enforcement never depends on the model’s own judgement. The stakes are clearest in work like a grant application, where one eligibility rule settled early decides whether everything after it counts.
Findings
- A rule binds a model only if checking it is compulsory. Popular fixes leave that check to the model’s discretion and fall short of the standard, and the paper proves that a compulsory check cannot be bypassed.
- Some conditions can’t be settled on the evidence available, and the framework keeps that ambiguity from turning into a wrong decision.
- The framework applies beyond grants, to any work where a frontier model has to reason under hard constraints and demonstrate its reliability.
Nenya grew from this work, and it holds Claude Code and Codex to the rules you set whether or not the agent stops to check them.