Source-linked AI summary
Logical Neural Networks
Ryan Riegel, Alexander Gray, Francois Luus, Naweed Khan, Ndivhuwo Makondo, Ismail Yunus Akhalwaya, Haifeng Qian, Ronald Fagin, Francisco Barahona, Udit Sharma, Shajith Ikbal, Hima Karanam, Sumit Neelam, Ankita Likhyani, Santosh Srivastava
TL;DR
LNNs address the gap between learnable neural models and interpretable symbolic reasoning by mapping neurons directly to weighted real-valued logical formulae. They use bidirectional bound propagation and contradiction-aware learning to reason over incomplete or inconsistent knowledge, with preliminary experiments supporting theorem-proving capability.
Problem
Existing approaches do not simultaneously provide neural learning, interpretable logical structure, rich knowledge use, and general theorem-proving ability.
Method
LNNs map neurons one-to-one onto weighted real-valued logical formula elements, constrain activations to logical truth functions, and perform bidirectional truth-bound inference.
Results
LNNs provide open-world truth bounds with possible probabilistic semantics, support omnidirectional inference, and proved all 25 evaluated TPTP problems within seconds.
Takeaways & Limitations
The framework combines interpretable logical representations with differentiable learning and reasoning that can accommodate incomplete and inconsistent knowledge.
Takeaways & Limitations
Learning requires constraints such as nonzero weights and classical behavior, motivating slack variables or an alternative approach to constrained optimization.
Abstract
from arXiv · showhide
We propose a novel framework seamlessly providing key properties of both neural nets (learning) and symbolic logic (knowledge and reasoning). Every neuron has a meaning as a component of a formula in a weighted real-valued logic, yielding a highly intepretable disentangled representation. Inference is omnidirectional rather than focused on predefined target variables, and corresponds to logical reasoning, including classical first-order logic theorem proving as a special case. The model is end-to-end differentiable, and learning minimizes a novel loss function capturing logical contradiction, yielding resilience to inconsistent knowledge. It also enables the open-world assumption by maintaining bounds on truth values which can have probabilistic semantics, yielding resilience to incomplete knowledge.
1 Introduction and related work
Logical Neural Networks (LNNs) align neural learning with symbolic knowledge and reasoning by making neurons correspond directly to logical formula elements. They support interpretable, bidirectional inference over incomplete or inconsistent knowledge.
- LNNs create a 1-to-1 correspondence between neurons and logical formula elements, avoiding conversion between logic and neural-network representations.Neuron weights can be constrained to implement logical gates such as AND and OR.
- Each neuron represents a concept or connective, exposing meanings and relationship importance while providing a compositional, modular, disentangled representation.Unlike clause-weighting approaches that hide internal logical structure, LNNs represent each element of a clause explicitly.
- LNNs support full function-free first-order logic with real-valued truth values, including classical 0/1 logic as a special case.
- Truth-value bounds support the open-world assumption by representing incomplete knowledge and can carry probabilistic semantics.Bounds provide more interpretable information than single truth values.
- Bidirectional relationships enable inference in any direction and support many-task use, including theorem proving.On a filtered subset of 25 TPTP problems, LNN proved all problems within seconds.
2 Overview
An LNN is a recurrent neural network whose neurons correspond one-to-one with weighted real-valued logical formulae, so evaluation performs logical inference. It propagates truth bounds through formula structure and can accept knowledge-base facts or injected queries.
- An LNN is a recurrent neural network with a 1-to-1 correspondence to logical formulae, and its evaluation performs logical inference.
- Neural activations implement the truth functions of logical operations, while outputs are expressed as bounds distinguishing known, approximate, unknown, and contradictory states.Classical behavior can be recovered when the inputs are classical.
- Inference is bidirectional, allowing ordinary evaluation of x → y as well as proving y from x or ¬x from ¬y.
- Inputs include initial truth bounds from knowledge-base data and may include injected formulae representing a query or inference problem.Outputs are typically final truth bounds at queried atoms or formulae.
- Figure 1 illustrates neurons and alternative activation functions configured to match connective truth functions across unambiguously True, False, and intermediate regions.
3 Model structure
LNN model structure mirrors logical syntax: neurons encode propositions and operations, activation functions implement selected real-valued logics, and bounds aggregate evidence across formulae. Weighted, differentiable activations provide a learnable but logically constrained model.
- Logical structure: An LNN graph combines syntax trees for represented formulae with neurons for each logical operation and unique proposition, returning lower and upper truth bounds.In propositional LNNs, each neuron returns values in [0, 1].
- Activation functions: Connective neurons receive operand outputs and use activation functions configured to match the corresponding logical truth functions.Different activation choices implement different real-valued logics, including Gödel, product, and Łukasiewicz logic.
- First-order extension: First-order LNNs add predicate and quantifier neurons, representing each grounded formula as a proposition and aggregating quantifiers over grounding dimensions.Universal and existential quantifiers use min and max aggregation, respectively.
- Activation functions: Activation functions must be differentiable and monotonic in the directions required by conjunction, disjunction, and implication.Importance weighting gives larger-weight neural inputs more influence on outputs.
- Weighted logic: Weighted generalizations use nonnegative weights and bias terms to define learnable nonlinear conjunctions, disjunctions, and implication.The bias term can align classically equivalent implication formulations in weighted nonlinear logic.
- Evidence aggregation: Atom neurons aggregate bounds from formulae that constitute proofs or disproofs of the atom, using maxima and minima or weighted logical alternatives.Aggregation weights can be inherited from atom occurrences in proof formulae.
4 Inference
LNN inference repeatedly propagates and tightens truth-value bounds both upward from subformulae and downward from formulae to their inputs. The resulting bidirectional computations correspond to logical inference rules and converge in finite steps.
- Inference process: Inference computes truth bounds for formulae and atoms from initial knowledge by repeatedly propagating tightened bounds until convergence.
- Logical reasoning: Inference rules propagate bounds from a connective’s output to its inputs, corresponding to familiar classical-logic reasoning patterns.
- Logical reasoning: When implication is defined as a residuum, modus ponens is performed through the logic’s t-norm, corresponding to AND.
- Bound propagation: Negation exchanges lower and upper bounds through complements, with inequalities preserving tighter bounds available from other sources.For example, evidence from both y and x → ¬y can contribute to the lower bound of ¬y.
- Upward and downward passes: The upward pass computes each formula’s bounds from its subformula bounds, while the downward pass uses formula bounds to tighten bounds for subformulae and atoms.
5 LNN bounds as probability bounds
LNN represents uncertainty using lower and upper truth bounds, which can serve as bounds on classical probabilities while supporting incomplete knowledge.
- 5 LNN bounds as probability bounds: LNN assigns lower and upper bounds to each subformula as bounds on the probability that it is True in classical logic.Different activation functions compute the lower and upper bounds.
- 5 LNN bounds as probability bounds: A sentence pairs a formula σ with lower and upper values l and u in [0, 1], while a theory is a set of such sentences.
- 5 LNN bounds as probability bounds: A probability model satisfies a theory when each formula’s probability lies between its specified lower and upper bounds.
- 5 LNN bounds as probability bounds: Given initially consistent bounds, LNN-computed bounds satisfy the theorem’s stated inequalities for the corresponding formulas.
6 Learning
LNN learning optimizes differentiable logical parameters while penalizing contradiction, and tailored activations preserve classical behavior while improving optimization flexibility.
- 6 Learning: Differentiability enables backpropagation to optimize operand weights, formula truth bounds, and atomic truth bounds.
- 6 Learning: Classical-behavior constraints require disjunctions to return True when any input is true and impose corresponding weight conditions.
- 6 Learning: LNN loss functions combine neural learning objectives with a contradiction penalty based on violations where lower bounds exceed upper bounds.The contradiction term penalizes the total contradiction observed across the system.
- 6 Learning: The constrained-optimization formulation cannot set operand weights to zero or relax constraints for nonclassical behavior without introducing slack variables.
- 6 Learning: Tailored activation functions interpolate between unambiguous, intermediate, and false truth regions, with smaller α values producing more classical behavior.They also permit weights to drop to zero and provide large, reliable gradients.
7 Empirical evaluation
Experiments evaluate LNN on inconsistent open-world knowledge and theorem-proving benchmarks, reporting contradiction removal, logical consequence inference, and successful proofs on a filtered TPTP subset.
- 7 Empirical evaluation: LNN training completely removes contradictions in the Smokers and friends experiment by relaxing facts and inferences.
- 7 Empirical evaluation: LNN adjusts conflicting axiom bounds to remove contradictions and infers logical consequences, including friendship symmetry that LTN cannot produce.
- 7 Empirical evaluation: LUBM evaluation uses 102707 triples, a 257-node LNN graph, and three bidirectional inference passes before computing 14 benchmark queries.
- 7 Empirical evaluation: 25 filtered Common Sense Reasoning problems from TPTP were all proved by LNN within seconds.The evaluated problems excluded functions and equality, which LNN does not currently support.
- 7 Empirical evaluation: LNN supports general first-order logical expressions, whereas the cited neural theorem provers are limited to Horn clauses.
8 Conclusions
The paper introduces LNN’s weighted real-valued logic, contradiction-minimizing learning, and finitely convergent inference, supported by preliminary comparative experiments.
- 8 Conclusions: The paper contributes a neuro-symbolic framework with probabilistically interpretable truth bounds, learnable parameters, contradiction-minimizing loss, and convergent reasoning procedures.
Broader Impact
Logical neural networks support interpretability, auditing, and human control by aligning neural computation with logical formulae and exposing inference chains.
- LNNs are interpretable through their 1-to-1 correspondence with systems of logical formulae.
- Users can audit a query by examining the chain of inferences computed for it.
- Human users can control modeled tasks by specifying logical constraints.
- The framework may improve transparency and fairness and offer an alternative when explainability is a design requirement.
Supplementary material for Logical Neural Networks
The supplementary material extends LNNs to first-order representations and describes grounding-based inference, quantifier handling, guided reasoning, and computational constraints.
- A.1 Overview: First-order LNNs represent constants, predicates, quantifiers, and logical connectives using atomic, connective, and quantifier neurons.
- A.1 Overview: Each neuron returns tables of groundings and corresponding truth-value bounds, with arity determining grounding-tuple size.
- A.1 Overview: Inference treats each grounding separately and propagates groundings through neurons with shared variables.
- A.1 Overview: Quantifier inference reduces or broadcasts bounds across quantified variables, with existential inverse computation requiring special handling because functions are not supported.
- A.1 Overview: Variable binding supports inference tasks such as query answering while retaining variables needed for joins across formula occurrences.
- A.5 First-order logical inference: Large knowledge bases can create substantial computational and memory demands, motivating avoidance of storing groundings with unknown bounds.
- A.5 First-order logical inference: Guided inference can limit expanded grounding sets by combining goal-driven and data-driven reasoning, trading computation against reasoning capacity.
- Łukasiewicz norms have associative and classical behavior only under specific bias and weight conditions, which LNNs do not require universally.
C.1 Proof of Theorem 1
The theorem proves finite ε-convergence for propositional LNN inference, while explicitly limiting that result because first-order evaluation can introduce indefinitely many new groundings.
- Algorithm 3 converges within ε in finite time for the propositional case.
- Monotonic updates make lower bounds increase toward 1 and upper bounds decrease toward 0, producing convergent bound sequences.
- For n total lower and upper bounds, the sum of deviations from their sequence endpoints is at most ε.
- The proof does not apply to FOL because evaluation can introduce new predicate groundings throughout computation.
- An infinite number of groundings can prevent convergence of the entire first-order system even when each grounding converges independently.
D Proof of Theorem 2
Theorem 2 establishes finite-step convergence of LNN bound updates and characterizes tailored activations that preserve logical behavior while retaining useful gradients. The section also identifies design trade-offs involving weight constraints, α, and n-ary formulations.
- Activation design: Tailored activation functions enforce logical outputs through weight-dependent functions, avoiding direct constraints on the weights.This approach is equivalent to weighted Łukasiewicz logic when α = 1.
- Activation design: Dynamic boundary points create a non-singleton classically True region, allowing smooth activations such as sigmoid to represent classical truth without reaching 1.The same design provides useful gradients throughout the domain.
- Design choice concerning xF: The tailored approach chooses the largest operand weight for boundary placement, preventing a very low-weight operand from exerting undue influence.This choice also yields the identity function when all but one conjunction weight approach zero, and removes the operator when all weights are zero.
- Logical behavior: Tailored activations preserve classical identities and guarantee upward modus ponens for classical values, whereas the n-ary form is not equivalent to the classically guaranteed decomposed form.The n-ary form is nevertheless used experimentally because it produces a simpler logical tree.
- Alpha interpretation: Per-node α values remain future work because differing local α values may require two-stage optimization of weights and α parameters under constraints.Per-node α values are motivated by training with sub-symbolic or real-valued inputs and by selectively modifying fact bounds.
F.7 Proof that zero weighting leads to identity
The tailored activation function is designed so zero-weighted inputs remove their influence, recovering identity when only one input remains weighted. The section also identifies limits of functional-inverse downward inference and motivates conditioning it with logical inference.
- Zero weighting and identity: The tailored activation function uses wmax so an n-ary conjunction with all but one zero-weighted inputs recovers the remaining operand’s identity.This behavior is proved from first principles and illustrated for a binary conjunction with one zero weight.
- Zero weighting and identity: When every input weight is zero, the operator becomes an impulse-like function, yielding True conjunction, False disjunction, and False implication behavior.Contradictions in this dead-state cannot be removed without directly modifying neuron bounds or deferring to a learnable β.
- Downward-inference limitations: Functional-inverse downward inference can produce classically incorrect bounds when real-valued inputs or outputs represent Unknown and False states.Examples include an Unknown input inferred as False and bounds tightened beyond the classically Unknown range.
- Downward-inference limitations: Logical downward inference recasts modus ponens-like reasoning as upward inference of a tautology, but the tautology can have undesired non-classical behavior.The issue appears when enforcing the requirement that a neuron should not learn from nothing.
F.8.1 Learning from nothing
The section examines whether downward inference can make an unknown neuron learn without informative output bounds, and develops a conditioned approach to limit unjustified tightening. It also connects contradiction handling and gradient-transparent clamping to LNN training.
- Learning from nothing: The functional inverse and logical inference tighten bounds differently across classical and non-classical regions, so neither method alone is uniformly appropriate.The functional inverse can be too aggressive in classical regions, while logical inference can learn too much in some non-classical bounds.
- Learning from nothing: Selecting the looser bound from conditioned logical inference and the functional inverse provides more consistent behavior while preserving the weight assignment.This conditioning targets the requirement that a neuron should not learn from nothing across real-valued bounds.
- Learning from nothing: A test of a binary conjunction evaluates upward and downward passes to determine whether an Unknown neuron can receive tighter bounds without informative supervision.The experiment varies α and compares computed output bounds with identity-function ground truth.
- Contradictions and training: Conditioned logical inference requires additional handling for intra-classical contradictions because aggressive tightening can make contradictory bounds no longer appear contradictory.The interpretability of the operation is not thereby broken, but contradiction detection is affected within classical regions.
- Contradictions and training: For classical inputs, self-supervised LNN training is expected to match supervised outputs, although it may require longer training.The stated advantage is reducing reliance on many labeled data points by directing neurons toward logical self-consistency.
- Gradient transparency: Gradient-transparent clamping preserves intended value clamping while retaining gradients across the full output range, addressing gradient loss caused by ordinary clamping.The construction uses detached value copies so clamping does not destructively interfere with automatic differentiation.
H.1 Smokers and friends
The Smokers and friends experiments train LNNs to reduce contradictions while balancing factual alignment and tight inferences. Across five- and eight-axiom settings, learned bounds and connective weights support contradiction removal, while gradient availability affects convergence speed.
- Setup: The experiments use Smokers and friends facts with five original axioms and an expanded eight-axiom set including MLN-induced formulae.The larger set introduces more simultaneous constraints and can produce more inconsistencies.
- Learning objective: The system loss minimizes contradiction while balancing fact alignment and tightness of inferred bounds across the network.The objective is (1 + contradiction)/(1 + factalign + tightbounds), with learning relaxing initial facts, axioms, and inferences as needed.
- Results: Learned fact and axiom bounds remove contradictions by trading off factual correctness against the tightness and informativeness of inferences.Excessive relaxation can create factual incorrectness or less tight, more unknown conclusions.
- Gradient effects: The loss can exhibit a flip-flop pattern because corrected contradictions detach gradients and slight contradictions reappear in alternating epochs.A decreasing learning rate and gradient clipping can provide convergence toward part of the real optimum.
- Gradient effects: Non-zero gradients in clamped Łukasiewicz regions accelerate convergence, although conventional zero gradients can still remove contradictions in this CNF system.The zero-gradient baseline changes fewer parameters and converges more slowly.
- Limitations: Full-domain gradient introduction may become necessary for more complex formula systems, while sigmoidal and tailored activations can provide broader gradient coverage.It is not strictly necessary for contradiction removal in the reported CNF formulae.
H.2 LUBM benchmark
The LUBM experiments evaluate LNN reasoning on synthetic OWL data and explore tolerance to noisy axioms. LNN answered the benchmark queries with perfect precision and recall and located and down-weighted a simple inconsistent axiom.
- Limitations: The reported noise experiment is preliminary and currently covers simple noise axioms, with broader ontological inconsistency handling left for future work.The authors plan to test more varied inconsistencies and self-correction capabilities.
- Reasoning procedure: LNN uses multiple forward and backward inference passes over one network, with final groundings at query nodes serving as query answers.Inference continues until the network converges.
- Soundness and completeness: 100% precision and recall were achieved on all 14 LUBM queries, matching Stardog and exceeding Virtuoso’s 72% and Blazegraph’s 78% average recall.The queries require reasoning from shallow to deep, and the result is reported as sound and complete reasoning on this task.
- Noise handling: With a deliberately incorrect domain-and-range axiom, contradictions appeared at the corresponding axiom node and LNN down-weighted it before further inference.The noisy axiom was designed to make the ontology inconsistent.
- Noise handling: After down-weighting the inconsistent node, LNN converged through additional inference passes and answered all 14 queries with 100% precision and recall.The experiment used simple noise axioms that did not require deep reasoning to identify conflicts.