Abstract
Neural networks excel at pattern recognition but struggle with reliable logical reasoning, often violating basic logical principles during inference. We address this limitation by developing a categorical framework that systematically constructs neural architectures with provable logical guarantees. Our approach treats logical theories as algebraic structures called Lawvere theories, which we transform into neural networks using categorical algebra in the 2-category of parametric maps. Unlike existing methods that impose logical constraints during training, our categorical construction embeds logical principles directly into the network's architectural structure, making logical violations mathematically impossible. We demonstrate this framework by constructing differentiable neural architectures for propositional logic that preserve boolean reasoning while remaining trainable via gradient descent. Our main theoretical result establishes a bijective correspondence between finitary logical theories and neural architectures, proving that every logically constrained network arises uniquely from our construction. This extends Categorical Deep Learning beyond geometric symmetries to semantic constraints, enabling automatic derivation of verified architectures from logical specifications. The framework provides mathematical foundations for trustworthy AI systems, with applications to theorem proving, formal verification, and safety-critical reasoning tasks requiring verifiable logical behavior.
Abstract (translated)
神经网络在模式识别方面表现出色，但在可靠的逻辑推理方面存在困难，在推理过程中常常违反基本的逻辑原则。我们通过开发一个范畴框架来解决这一限制，该框架系统地构建具有可证明逻辑保证的神经架构。我们的方法将逻辑理论视为称为Lawvere理论的代数结构，并使用参数映射2-范畴中的范畴代数将其转换为神经网络。与现有方法在训练期间施加逻辑约束不同，我们的范畴构造直接将逻辑原则嵌入到网络的架构中，使得逻辑违规从数学上是不可能的。我们通过构建用于命题逻辑的不同iable神经架构来展示这一框架，这些架构在保持布尔推理的同时可以通过梯度下降进行训练。我们主要的理论成果确立了有限逻辑理论和神经架构之间的一一对应关系，证明每个受逻辑约束的网络都唯一地源自我们的构造。这将范畴深度学习从几何对称性扩展到语义约束，使能够自动从逻辑规范中推导出可验证的架构。该框架为值得信赖的人工智能系统提供了数学基础，并在定理证明、形式验证和需要可验证逻辑行为的安全关键推理任务中有着应用。
URL
https://arxiv.org/abs/2508.11647
