> For the complete documentation index, see [llms.txt](https://neurosymbolicai.gitbook.io/neuro-symbolic-ai-in-practice/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://neurosymbolicai.gitbook.io/neuro-symbolic-ai-in-practice/part-iii-core-approaches/chapter-4/4-2-neural-helps-symbolic/4-2-differentiable-reasoning.md). # 4.2.1 Differentiable Reasoning **Definition:** Translating formal logic rules into continuous, differentiable neural network components, allowing systems to *learn* logical rules from data, or to reason using logic while remaining end-to-end differentiable.(Sheth et al., 2023)(Serafini & d'Avila Garcez, 2022) This approach dissolves the hard boundary between neural and symbolic computation. Rather than running a discrete logical reasoner as a separate module, the reasoning process is *implemented* as differentiable operations on continuous representations — making it trainable by gradient descent. ### Markov Logic Networks (MLN) **Markov Logic Networks** (Richardson & Domingos, 2006) are the classical foundation of combining first-order logic with probabilistic graphical models — the framework that DeepProbLog, LTN, and modern differentiable logic directly respond to and improve upon. An MLN is a set of first-order logic formulas, each paired with a real-valued weight reflecting the strength of belief in that formula. Weights can be learned from data via maximum likelihood or discriminative training. The joint distribution over all ground atoms is a Markov random field whose energy equals the negative sum of weights for satisfied formulas. Every deterministic first-order knowledge base is a special case: assign infinite weight to each formula and the distribution becomes uniform over the set of models that satisfy the knowledge base (i.e., worlds where all formulas hold), and queries reduce to model-theoretic consequence within those satisfying worlds. **Key capability:** MLNs support both *discriminative* and *generative* inference, enabling both classification and knowledge base completion. They have been applied to link prediction, relation extraction, and collective classification — tasks where the truth of one fact probabilistically influences the truth of related facts. **Limitation that motivates later work:** MLN inference requires grounding all formulas over all constants in the domain. On a domain with $n$ entities and a formula with $k$ variables, grounding produces $O(n^k)$ propositional clauses — polynomial in $n$ for fixed $k$, but exponential in $k$, and rapidly intractable for large domains with multi-variable formulas. This grounding bottleneck is precisely what LTN (by working in continuous embedding space) and DeepProbLog (by tabling proofs) were designed to overcome. MLNs thus occupy the essential historical position of defining the problem space that all subsequent neuro-symbolic probabilistic reasoning approaches have refined. *Reference:* Richardson, Matthew, and Pedro Domingos. "Markov Logic Networks." *Machine Learning* 62.1–2 (2006): 107–136. | Code: *** ### Logic Tensor Networks (LTNs) **Logic Tensor Networks** (Serafini & d'Avila Garcez, 2016; updated 2021)(Serafini & d'Avila Garcez, 2022) are the canonical example of differentiable reasoning. LTNs ground the symbols and quantifiers of First-Order Logic in a continuous, differentiable space: * **Constants and variables** in FOL correspond to real-valued vector representations (embeddings). * **Predicates** (e.g., `Red(x)`, `LeftOf(x, y)`) are implemented as neural networks that map from object embeddings to a truth value in $\[0, 1]$. * **Logical connectives** ($\land$, $\lor$, $\lnot$, $\Rightarrow$) are implemented using fuzzy logic operators. The **product t-norm** ($A \land B = A \times B$) is recommended for gradient-based training as it is differentiable everywhere. The Gödel t-norm ($A \land B = \min(A, B)$) is an alternative but is not differentiable at $A = B$. * **Quantifiers** ($\forall$, $\exists$) are implemented as aggregations over object embeddings. The **generalized mean (p-mean)** is the recommended differentiable approximation:(Serafini & d'Avila Garcez, 2022) $$\forall x., P(x) ;\approx; \left(\frac{1}{|\mathcal{D}|}\sum\_{x \in \mathcal{D}} P(x)^p\right)^{1/p}$$ **Sign convention:** For the **universal quantifier** ($\forall$), $p$ must be a **large negative integer** (as $p \to -\infty$, the p-mean approaches $\min$); for the **existential quantifier** ($\exists$), $p$ is large and positive (approaching $\max$). For $p = 1$ the formula gives the arithmetic mean. The Serafini & d'Avila Garcez (2022) paper recommends $p\_\forall = -10$ as a practical default. The result is a system where *knowledge base axioms* — "all red objects are cubes", "if X is left of Y and Y is left of Z, then X is left of Z" — can be expressed as logical formulas and incorporated into the loss function: $$\mathcal{L}\_\text{LTN} = -\Phi(\text{KB})$$ where $\Phi(\text{KB})$ is the aggregated truth value of the knowledge base under the current predicate networks. Maximizing $\Phi(\text{KB})$ is equivalent to satisfying the logical axioms. **Key capability:** LTNs can simultaneously learn from labeled data *and* satisfy logical constraints, and they support both *learning* (training predicate networks from examples) and *reasoning* (querying truth values and inferring missing facts). **Applications:** * **Semantic image interpretation:** LTNs have been applied to part-of-speech relationships in images ("the wheel is part of the car") where spatial reasoning rules (transitivity, symmetry) are embedded as logical axioms. * **Link prediction in knowledge graphs:** Given a partial knowledge graph, an LTN learns embeddings and predicate networks that satisfy known logical constraints (e.g., `spouse` is symmetric, `subClassOf` is transitive). *Reference:*\ Serafini, Luciano, and Artur d'Avila Garcez. "Logic Tensor Networks." *Artificial Intelligence* 303 (2022): 103649. | Code: ### End-to-End Differentiable Proving **Rocktäschel & Riedel (2017)**(Rocktäschel & Riedel, 2017) introduced *end-to-end differentiable proving* — an approach where theorem proving over knowledge bases is made differentiable by replacing discrete unification with soft, continuous analogues. Given a knowledge base of rules and facts, the system attempts to prove a query by searching over proof trees. Each unification step (matching variables to entities) is replaced by a similarity function over entity embeddings, making the entire proof search differentiable. The system learns entity embeddings that make true facts provable and false facts unprovable. Key contribution: this work showed that simple recursive theorem proving (backward chaining) could be implemented as a recurrent neural network, inheriting gradient-based training while maintaining logical interpretability in the proof structure. *Reference:*\ Rocktäschel, Tim, and Sebastian Riedel. "End-to-End Differentiable Proving." *Advances in Neural Information Processing Systems (NeurIPS)*, 2017. ### DeepProbLog **DeepProbLog** (Manhaeve et al., 2018/2021) integrates neural networks with probabilistic logic programming (ProbLog). It extends ProbLog with **neural predicates** — predicates whose truth probability is computed by a neural network: ```prolog % Neural predicate: digit/2 maps an image to a digit label nn(mnist_net, [X], Y, digit) :: digit(X, Y). % Symbolic rule: addition addition(X, Y, Z) :- digit(X, N1), digit(Y, N2), Z is N1 + N2. ``` The `digit/2` predicate runs a neural network (an MNIST classifier) on image input and produces a probability distribution over digit labels. The symbolic rule composes two such predicates to reason about addition. DeepProbLog enables end-to-end learning of tasks that require both perception (neural) and symbolic reasoning (logic), with probabilities propagated through the logic program via the ProbLog inference engine. **MNIST Addition example:** Given pairs of MNIST handwritten digit images, the system learns to add them. No labeled digit identities are provided during training — only the sum. The model learns what each digit looks like by being trained on the downstream task of producing the correct sum. This demonstrates the power of *weak supervision* through symbolic task constraints.(Manhaeve et al., 2018/2021) *Reference:*\ Manhaeve, Robin, et al. "DeepProbLog: Neural Probabilistic Logic Programming." *NeurIPS 2018 Workshop on Modeling and Decision-Making in the Spatiotemporal Domain* (2018); extended version in *Machine Learning* 110.7 (2021): 1637–1679. | Code: ### Scallop — Scalable Neurosymbolic Reasoning **Scallop** (Li et al., 2023) is the production-grade successor to DeepProbLog. It compiles Datalog-like probabilistic logic programs into differentiable functions using *semiring provenance semantics*, enabling integration with arbitrary PyTorch modules while scaling to millions of facts. The key innovation is the **provenance semiring**: instead of tracking exact probabilities over all proofs (which is #P-hard in general), Scallop parameterizes inference with a family of approximate semirings. The `top-k` semiring tracks only the $k$ highest-probability proofs, trading exactness for scalability. This enables inference on datasets with millions of facts (where DeepProbLog is limited to hundreds), a standard `torch.nn.Module` API that plugs into any training pipeline, and support for complex relational queries including joins, aggregations, and negation. ```python import scallopy ctx = scallopy.ScallopContext() ctx.add_relation("digit", (int, int)) # (image_id, digit_label) ctx.add_rule("sum(x, y, z) = digit(x, a), digit(y, b), z = a + b") ctx.add_neural_module("digit", mnist_net) # neural predicate # End-to-end differentiable: loss propagates through the logic result = ctx.forward({"digit": image_batch}) ``` **Applications:** Visual QA (CLEVR, GQA), relational reasoning, and neuro-symbolic scene understanding. Scallop achieves 10–100× speedup over DeepProbLog at equivalent accuracy on these benchmarks, making it the practical choice for production systems requiring probabilistic logic with neural perception. *Reference:* Li, Ziyang, et al. "Scallop: A Language for Neurosymbolic Programming." *Proceedings of the ACM on Programming Languages (OOPSLA)*, 2023. | Code: ### A-NeSI: Scalable Approximate Neurosymbolic Inference **Motivation**: DeepProbLog and Scallop perform exact or near-exact probabilistic NeSy inference. The fundamental bottleneck is that probabilistic inference in ProbLog is #P-hard — the number of proofs grows exponentially with the number of random variables. DeepProbLog breaks on MNIST-Addition with N > 4 digits (\~10^8 groundings). Scallop's provenance semirings reduce this but still hit a ceiling. A-NeSI replaces the exact inference step with a trained neural approximator. **Architecture**: ``` Neural Perception: x → p(z | x) [e.g., p(digit=k | image)] │ ▼ A-NeSI Approximator: q_φ(y | z) ≈ P_ProbLog(y | z) [trained MLP] │ ▼ Answer distribution: y ~ q_φ(y | z) ``` The approximator $q\_\phi$ is trained offline: sample random inputs to the ProbLog program, run exact inference to get $P\_\text{ProbLog}(y | z)$, train $q\_\phi$ to match this distribution. At test time, $q\_\phi$ replaces the expensive symbolic inference. **Key result**: A-NeSI achieves within 2% of DeepProbLog's accuracy on MNIST-Addition while scaling to 15-digit addition (10^15 groundings) — two orders of magnitude beyond DeepProbLog's ceiling of \~4 digits. Training time is reduced from hours to minutes. **Scalability comparison**: | System | Max MNIST digits | Inference time (per example) | | --------------- | ---------------- | ---------------------------- | | DeepProbLog | 4 | \~2 s | | Scallop (top-k) | \~8 | \~0.5 s | | A-NeSI | 15+ | \~0.001 s | > \[!WARNING] **Limitation**: A-NeSI is approximate — the neural approximator may deviate from exact probabilistic inference. For safety-critical applications requiring certified probabilistic bounds, use exact methods. A-NeSI is appropriate when scalability matters more than exactness. > \[!TIP] **When to use**: large-scale structured prediction problems where the symbolic constraint has a known structure but exact inference is intractable; when DeepProbLog or Scallop are too slow for your dataset size. *Reference:* van Krieken, Emile, et al. "A-NeSI: A Scalable Approximate Method for Probabilistic Neurosymbolic Inference." *Advances in Neural Information Processing Systems* 36 (NeurIPS 2023). | Code: *** ### ∂ILP — Differentiable Inductive Logic Programming **∂ILP** (Evans & Grefenstette, 2018) makes the *search* for logical rules itself differentiable. Given positive and negative examples of a target predicate, ∂ILP learns a logic program (a set of Horn clause rules) by gradient descent over a continuous relaxation of the discrete rule space: ``` Input: examples of ancestor(X, Y) Output: rules: ancestor(X, Y) :- parent(X, Y). ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y). ``` The system learns from very few examples (sometimes as few as 3–5 positive examples) and discovers human-interpretable logical rules. This is in contrast to neural network learning, which typically requires thousands of examples and produces opaque representations. *Reference:*\ Evans, Richard, and Edward Grefenstette. "Learning Explanatory Rules from Noisy Data." *Journal of Artificial Intelligence Research* 61 (2018): 1–64. | Code: ### FlashFill — The First Commercial Program Synthesis Deployment Before the neural program synthesis approaches of ∂ILP and DreamCoder, **FlashFill** (Gulwani, 2011) demonstrated that program synthesis from examples is commercially viable at scale. FlashFill is the "Flash Fill" feature in Microsoft Excel: given 2–3 input-output examples of a text transformation (e.g., extracting first names from "Smith, John" → "John"), it synthesizes a string processing program that generalizes to the entire column. The synthesis algorithm uses a **version-space algebra** — a purely symbolic inductive inference technique that efficiently represents the intersection of all programs consistent with the given examples. It requires no neural component; its power comes entirely from the structured program space (a domain-specific language of string operations) and the symbolic enumeration over that space. FlashFill's significance for neuro-symbolic AI is twofold. First, it demonstrated that purely symbolic program synthesis can be deployable and user-friendly at massive scale (hundreds of millions of Excel users). Second, it defined the benchmark against which neural approaches like DreamCoder must be measured: DreamCoder's library learning provides generalization across task domains that FlashFill's hard-coded DSL cannot achieve, while FlashFill's symbolic backbone provides exact correctness guarantees on every synthesized program. The neuro-symbolic frontier — combining FlashFill-style symbolic correctness with DreamCoder-style library learning — remains an active research direction.(Gulwani, 2011) *Reference:*\ Gulwani, Sumit. "Automating String Processing in Spreadsheets Using Input-Output Examples." *ACM SIGPLAN Notices* 46.1 (2011): 317–330. | Excel integration: ### DreamCoder — Library Learning for Program Synthesis **DreamCoder** (Ellis et al., 2021) extends the ∂ILP paradigm to a fundamentally different scale: rather than learning individual rules, DreamCoder learns a *growing library of reusable symbolic primitives* through an alternating wake-sleep procedure. **The Wake-Sleep Loop:** ``` ┌─────────────────────────────────────────────────────────┐ │ DreamCoder Loop │ │ │ │ WAKE phase │ │ Neural recognition model proposes programs P │ │ for each task using current library L │ │ Symbolic interpreter evaluates correctness │ │ │ │ SLEEP phase (two components): │ │ 1. Dreaming: sample programs from generative prior │ │ add to training set (fantasy programs) │ │ 2. Consolidation: abstract successful programs │ │ into new library primitives via compression │ │ │ │ Neural model retrained on augmented library │ │ → Each iteration: richer library, easier tasks │ └─────────────────────────────────────────────────────────┘ ``` The consolidation step performs **program compression**: if the same sub-program appears in many solutions, it is abstracted into a new named primitive and added to the library $L$. The library grows from a handful of primitives to hundreds over training, dramatically simplifying the programs needed to solve each task — a form of automatic curriculum learning in which the system constructs its own vocabulary of concepts. **Key results:** In list processing, DreamCoder learns `map`, `filter`, and `fold` from examples and then solves complex transformations by composing them. In physics, it learns Newton's laws as primitives and solves trajectory problems with one-line programs. On ARC-like visual puzzles, it achieves compositional generalization that pure neural approaches cannot replicate because the learned library provides a reusable symbolic scaffold. **Connection to HTN planning:** The DreamCoder library is structurally identical to an HTN method library: both represent reusable, compositional task decompositions. LLM-driven HTN method induction (§3.4) is the language-model analogue of DreamCoder's neural consolidation step — using language model inference rather than program compression to grow the method library from experience. *Reference:* Ellis, Kevin, et al. "DreamCoder: Bootstrapping Inductive Program Synthesis with Wake-Sleep Library Learning." *Proceedings of PLDI*, 2021. | Code: ### Classical ILP: Popper and ILASP The differentiable ILP approaches (∂ILP, §4.2.1) are end-to-end trainable but limited to short programs and require continuous relaxations of discrete structure. Classical ILP systems learn crisp, provably correct logic programs from positive and negative examples without gradient descent — complementing the differentiable approaches by providing soundness and completeness guarantees. **Popper** (Cropper & Dumancic, 2022) is the current state of the art in classical ILP. It uses a constraint-driven hypothesis search over a hypothesis space encoded as a meta-level SAT/ASP problem. Popper learns programs of arbitrary complexity, not limited to short clauses, and is sound and complete: if a correct program exists within the hypothesis space, Popper will find it. The programs it produces are interpretable Prolog programs that can be directly inspected and edited by domain experts. Search scales via constraint propagation: constraints learned from failed hypotheses prune the remaining hypothesis space, making each iteration faster. **ILASP** (Law et al., 2020) extends ILP to **Answer Set Programming** (ASP), enabling learning with non-monotonic background knowledge — defaults, exceptions, and negation-as-failure. ILASP is the appropriate tool when background knowledge includes "unless otherwise specified" reasoning patterns, such as learning rules about medical contraindications or regulatory exceptions. > \[!TIP] **When to use classical vs. differentiable ILP:** > > * **∂ILP / Scallop:** when you need end-to-end training with neural perception, gradient-based optimization, or probabilistic inference > * **Popper:** when you need programs of arbitrary length, high interpretability, and a provably correct solution from clean examples > * **ILASP:** when your background knowledge includes non-monotonic rules (defaults, exceptions) *References:* Cropper, Andrew, and Sebastijan Dumancic. "Learning Programs by Learning from Failures." *Machine Learning* 111.3 (2022): 801–856. | Code: Law, Mark, Alessio Russo, and Krysia Broda. "The ILASP System for Inductive Learning of Answer Set Programs." *arXiv preprint*, 2020. | Code: ### Neural Predicate Invention: Learning New Symbolic Vocabulary **Motivation**: Popper and ILASP learn programs over a *fixed* predicate vocabulary. If the target concept requires an intermediate predicate not in the background knowledge (e.g., "grandparent" from "parent"), classical ILP uses predicate invention heuristics. Neural predicate invention uses neural embeddings to discover useful new predicates automatically. **Core idea** (Cropper et al., 2022): * A meta-learning outer loop proposes new predicate definitions by clustering neural embeddings of training examples * The proposed predicates are tested as background knowledge extensions in a classical ILP system (Popper) * Predicates that reduce the hypothesis search space are retained * The invented predicate library grows across tasks — enabling transfer **Key result**: On the LARC visual concept learning benchmark, neural predicate invention reduces the number of training examples needed from \~50 to \~8 per concept, by inventing reusable intermediate predicates (e.g., "same-row", "adjacent-column") from raw grid observations.(Stahl et al., 2024) > \[!IMPORTANT] **Relationship to DreamCoder**: DreamCoder (§4.2.1) performs library learning over *program primitives* (procedural abstractions); neural predicate invention performs library learning over *relational predicates* (logical abstractions). Both address the same underlying problem — building a reusable symbolic vocabulary from data — but at different levels of the symbolic hierarchy. > \[!TIP] **When to use**: few-shot concept learning from structured relational data; when the predicate vocabulary for your ILP system is incomplete and you have the computational budget for the meta-learning outer loop. *References:* Cropper, Andrew, and Sebastijan Dumancic. "Learning Programs by Learning from Failures." *Machine Learning* 111.3 (2022): 801–856. (Section 7 on predicate invention.) Stahl, Isabelle, et al. "Neural Predicate Invention for Visual Concept Learning." *Proceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence (AAAI-24)*. 2024. *** The ILP approaches above all operate on structured data with explicit logical language. The following pattern takes a different approach: it leverages any existing programming language as the symbolic oracle, making the symbolic component accessible to any domain with a Python interface. ### Program Execution as Symbolic Oracle — PAL, PoT, VisProg, ViperGPT Among the most widely deployed neuro-symbolic patterns in 2023–2026 is one that requires no specialized architecture at all: the **LLM generates a program; a symbolic interpreter executes it and returns the ground-truth result.** The interpreter is the symbolic oracle; the LLM is the neural generator. Neither can solve the problem alone — the LLM cannot reliably compute, and the interpreter cannot understand the problem statement. This pattern has four prominent instantiations: **PAL — Program-Aided Language Models** (Gao et al., 2023) addresses mathematical reasoning. Rather than generating a final numerical answer (which LLMs hallucinate unreliably), PAL prompts the LLM to generate a Python program that *computes* the answer, then executes the program to obtain the result.(Gao et al., 2023) On GSM8K (grade-school math), PAL with Codex achieves 72% accuracy — a substantial improvement over chain-of-thought prompting alone, and the pattern generalizes further as model capability increases. **Program of Thoughts (PoT)** (Chen et al., 2023) extends PAL by explicitly separating *reasoning* (expressed as Python comments and variable names) from *computation* (expressed as executable code).(Chen et al., 2023) This separation allows the LLM to focus on translating the problem into a computational structure while delegating all arithmetic to the interpreter. The key insight: reasoning and computation are different cognitive operations, and the LLM is good at the former but unreliable at the latter. **VisProg** (Gupta & Kembhavi, 2023) extends the pattern to **compositional visual reasoning**.(Gupta & Kembhavi, 2023) The LLM generates a Python program that calls a library of vision modules — `LOC(image, object)`, `CLASSIFY(image, query)`, `CROP(image, region)`, `COUNT(objects)` — each implemented as a specialized neural model. The LLM reasons about *how to compose* vision operations; the individual modules handle *what to perceive*. ```python # VisProg example: "How many red objects are to the left of the large blue sphere?" OBJECTS = LOC(image, "objects") BLUE_SPHERE = FILTER(OBJECTS, "large blue sphere") LEFT_OBJECTS = FILTER(OBJECTS, f"to the left of {BLUE_SPHERE}") RED_LEFT = FILTER(LEFT_OBJECTS, "red") RESULT = COUNT(RED_LEFT) ``` **ViperGPT** (Suris et al., 2023) operates similarly but generates programs that call pretrained vision APIs (CLIP, DepthEstimator, ObjectDetector) as Python functions, enabling compositional visual reasoning about depth, relationships, counting, and attributes that single-model approaches fail on.(Suris et al., 2023) **Why this pattern is the most practically important in §4.2.** The LLM-generates-program-interpreter-executes pattern is: * **The most deployed NeSy pattern in production:** virtually every major LLM API now supports code execution, making this pattern accessible with zero additional infrastructure. * **The clearest demonstration of LLM-Modulo in practice:** the interpreter provides *ground truth* feedback (not a learned approximation), and its correctness is unconstrained by the LLM's probability distribution. * **Extensible to any domain with a formal interpreter:** symbolic math (SymPy), database queries (SQL), formal planning (PDDL parsers), chemistry (RDKit), CAD (OpenSCAD). Any domain with a Python interface becomes a neuro-symbolic system via this pattern. **The neuro-symbolic architecture:** ``` Problem statement (natural language) │ ▼ LLM (neural generator) generates: Python program / SQL / formal expression │ ▼ Interpreter / solver (symbolic oracle) executes program, returns ground-truth result │ ▼ Result (correct by construction, given correct program generation) ``` **Limitations.** The pattern's correctness guarantee is conditional: if the LLM generates a syntactically valid but semantically wrong program, the interpreter will return a wrong answer. Unlike §4.2.2's MCTS-based approaches (where the symbolic oracle verifies correctness iteratively), this pattern uses the interpreter as a one-shot executor. Integration with test cases (as in SWE-bench, §4.3.10) or self-debugging loops (as in AlphaCode) closes this gap by providing multiple execution opportunities. *References:* Gao, Luyu, et al. "PAL: Program-Aided Language Models." *Proceedings of ICML*, 2023. | Code: Chen, Wenhu, et al. "Program of Thoughts Prompting: Disentangling Computation from Reasoning for Numerical Reasoning Tasks." *Transactions on Machine Learning Research (TMLR)*, 2023. | Code: Gupta, Tanmay, and Aniruddha Kembhavi. "Visual Programming: Compositional Visual Reasoning without Training." *Proceedings of CVPR*, 2023. | Code: Suris, Dídac, Sachit Menon, and Carl Vondrick. "ViperGPT: Visual Inference via Python Execution for Reasoning." *Proceedings of ICCV*, 2023. | Code: ### LLM-to-Logic-Solver: Formal Reasoning via Generated Logical Specifications The PAL/PoT pattern (§4.2.1) uses LLMs to generate Python/arithmetic programs executed by an interpreter. The LLM-to-Logic-Solver pattern is the parallel pattern for *formal logical reasoning*: the LLM generates a formal logical specification (first-order logic clauses, SAT/SMT assertions, or Prolog rules), and an external symbolic solver executes it to produce a certified answer. **Three key systems**: *LOGIC-LM (Pan et al., EMNLP 2023)*: * **Problem**: complex multi-step logical reasoning tasks (ProofWriter, FOLIO, ProntoQA, AR-LSAT) that require sound deductive inference * **Architecture**: LLM translates NL problem → symbolic representation (FOL clauses, constraint programs) → external solver (Pyke for deductive reasoning on ProofWriter/ProntoQA; Z3 for constraint satisfaction on LogicalDeduction/AR-LSAT) → verified answer * **Self-refinement loop**: if the solver throws an error (syntax error, type mismatch), the LLM receives the error message and generates a corrected specification * **Results**: +18.4% average over GPT-4 chain-of-thought across five reasoning datasets; +39.2% over standard (non-CoT) prompting Worked example: ``` NL: "All students are people. John is a student. Is John a person?" LOGIC-LM output (symbolic): ∀x: Student(x) → Person(x) Student(John) Pyke query: Person(John)? Solver: YES (proved via modus ponens in 1 step) ``` *SatLM (Ye et al., NeurIPS 2023)*: * Uses LLM to generate a declarative task specification (Z3 Python API assertions) from word problems; an automated theorem prover derives the final answer * The Z3 solver either proves the specification or returns UNSAT with a counter-model * Key advantage over PAL: the solver's answer is formally certified; arithmetic errors are impossible * Results: +23% over program-aided LMs on a challenging subset of the GSM arithmetic reasoning dataset; new state of the art on LSAT *LINC (Olausson et al., EMNLP 2023 — Outstanding Paper Award)*: * LLM generates Prolog programs from NL premises * SWI-Prolog executes the program and returns a proof trace * Proof trace can be inspected: the reasoning is fully auditable * Results: +26% on ProofWriter over chain-of-thought GPT-4; performance comparable to GPT-4 CoT on FOLIO (Olausson et al., 2023) **Comparison table**: | System | Symbolic Language | Solver | Typical Domain | Certified? | | -------- | ------------------- | ---------------------------------- | ----------------------- | ----------- | | PAL/PoT | Python/arithmetic | Python interpreter | Math, data | Execution | | LOGIC-LM | FOL / constraints | Pyke (deduction), Z3 (constraints) | Logical deduction | Proof | | SatLM | Declarative Z3 spec | Z3 | Constraint satisfaction | UNSAT proof | | LINC | Prolog | SWI-Prolog | NL inference | Proof trace | > \[!TIP] **When to use**: Use PAL/PoT for numerical/computational problems; use LLM-to-Logic-Solver when the task requires *sound deductive reasoning* where errors are unacceptable. SatLM is preferred when the problem is naturally expressed as constraints (scheduling, allocation, feasibility). LINC is preferred when an auditable proof trace is required. *References:* Pan, Liangming, et al. "Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning." *Findings of EMNLP*, 2023. | Code: Ye, Xi, et al. "SatLM: Satisfiability-Aided Language Models Using Declarative Prompting." *Advances in Neural Information Processing Systems* 36 (NeurIPS 2023). Olausson, Theo X., et al. "LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers." *Proceedings of EMNLP* (Outstanding Paper Award), 2023. | Code: *** --- # Agent Instructions This documentation is published with GitBook. GitBook is the documentation platform designed so that both humans and AI agents can read, navigate, and reason over technical content effectively. Learn more at gitbook.com. ## Querying This Documentation If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question. Perform an HTTP GET request on the current page URL with the `ask` query parameter, and the optional `goal` query parameter: ``` GET https://neurosymbolicai.gitbook.io/neuro-symbolic-ai-in-practice/part-iii-core-approaches/chapter-4/4-2-neural-helps-symbolic/4-2-differentiable-reasoning.md?ask=&goal= ``` `ask` is the immediate question: it should be specific, self-contained, and written in natural language. `goal` is optional and describes the broader end goal you are ultimately trying to accomplish on behalf of the user. GitBook uses it to tailor the answer towards what is most useful for that goal. The response will contain a direct answer to the question and relevant excerpts and sources from the documentation. Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.