{"id":"31668ce1-6405-4d63-8c5f-6a59169148c0","arxiv_id":"2505.20313","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":4.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"Any propositional logic formula can be encoded as an RBM such that energy minimization finds the satisfying assignments, and the system can also learn from data and knowledge.","lead":"This chapter describes Logical Boltzmann Machines, which translate any propositional logic formula into a restricted Boltzmann machine whose lowest-energy states are exactly the satisfying assignments. It reports experiments on reasoning, learning from data and knowledge, and MaxSAT solving, with mixed comparisons against symbolic solvers.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Eq. (18) CNF-to-RBM translation is not equivalent to the original CNF; the RBM for clause (x1∨x2) encodes XOR, undermining the SAT/MaxSAT experiments.","rationale":"The reader's weakest assumption was that Lemma 2 (Gibbs sampling equivalence) is unproven, an algorithmic heuristic. That is a valid practical concern, but the more severe issue is a formal error in the CNF-to-RBM conversion, which directly affects the validity of the SAT and MaxSAT experiments. The central SDNF theorem itself is sound, and the full-DNF route would still allow representation of any WFF, so the headline claim survives in principle. However, the paper's efficient CNF translation, which underpins several claimed contributions, is incorrect as stated. Since the paper is a chapter that largely repackages prior work and includes preliminary experiments, the appropriate verdict remains conditional: the authors should correct Eq. (5)/(18) or clearly restrict its use, and re-run the affected experiments. The reader's condition on Gibbs sampling is still relevant but secondary; hence I disagree with the reader's identification of the weakest assumption, while agreeing with the overall conditional verdict.","tokens_in":32307,"tokens_out":14208,"duration_ms":103223,"concrete_test":"Take the CNF φ = (x1 ∨ x2). Apply Eq. (5)/(18) to produce the SDNF D = (¬x2∧x1) ∨ (¬x1∧x2). Enumerate all four truth assignments and verify whether sφ(x) equals the truth value of D for each assignment. If D is false when x1=x2=T (as the formula gives), the translation is not equivalent. For a more direct check, construct the RBM from D with ε=0.5 and verify whether the global energy minima correspond exactly to the satisfying assignments of φ: they will not, because the assignment (T,T) is a satisfying assignment of φ but is not a model of D.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central SDNF-to-RBM theorem (Theorem 1) is correct: for a strict DNF, minimizing over hidden units gives -ε for satisfying assignments and 0 otherwise. However, the claimed efficient CNF translation (Section 3.6.1, Eq. (18)) relies on Eq. (5), which is not a valid SDNF conversion. For a clause γ ≡ x1 ∨ x2, ST is empty and SK={1,2}, so Eq. (5) yields (¬x2∧x1) ∨ (¬x1∧x2), which is the XOR of x1 and x2, not their disjunction. Enumerating truth assignments confirms the mismatch: for x1=T, x2=T, the original clause is true but the transformed SDNF is false. Consequently, the RBM constructed from a CNF via Eq. (18) does not have its global energy minima at the satisfying assignments of the CNF. Since Section 3.6.4 (SAT solving) and Section 4 (MaxSAT) explicitly convert CNF inputs using 'the transformation described earlier' (Eq. (18)), those experimental results are built on an unsound representational step. The full-DNF route to SDNF is correct but exponential, so the paper's claim of an efficient CNF conversion is false. The theorem statement also says sφ(x) = -E(x) while the proof establishes sφ(x) = -1/ε min_h E(x,h); this is a lesser typo, but the CNF error is substantive and load-bearing for the claimed practical scope.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The manuscript, framed as a book chapter, proposes Logical Boltzmann Machines (LBM), an energy-based neurosymbolic framework. It defines a translation from SDNF propositional formulas to RBM energy functions (Theorem 1), argues that any WFF can be represented via full DNF, and claims that inference can be performed by energy minimization, Gibbs sampling, or free-energy optimization. It reports experiments on model coverage, ILP benchmarks, SAT solving, MaxSAT, and a semantic image interpretation task, alongside broad discussion of LLMs, accountability, and future neurosymbolic challenges.","tokens_in":32690,"tokens_out":10931,"duration_ms":92538,"significance":"If the central construction is accepted, the paper offers a clean formal bridge between propositional logic and a restricted Boltzmann machine, extending earlier penalty-logic ideas to a tractable restricted architecture and enabling logical constraints to be inserted as verifiable neural modules. The SDNF-to-RBM construction in Theorem 1 is explicit, simple, and mostly correctly proved once the min_h typo is fixed. The paper also provides worked examples and compares LBM with several neurosymbolic systems. However, the broader practical claims are currently undercut by an invalid CNF conversion, an unsupported sampling equivalence, and a confounded experimental comparison in Section 5, so the manuscript needs substantial revision before the practical claims can be accepted.","major_comments":[{"comment":"The proposed CNF-to-SDNF conversion is not logically valid. For the clause γ = x1 ∨ x2 (so ST = ∅, SK = {1,2}), Eq. (5) yields (¬x2 ∧ x1) ∨ (¬x1 ∧ x2), which is the XOR of x1 and x2; in particular it evaluates to False on x1 = x2 = 1, where the original clause is True. Consequently, the RBM constructed from Eq. (18) does not in general have its global energy minima at the satisfying assignments of the CNF. Since the SAT experiments in §3.6.4 and the MaxSAT construction in §4 explicitly use this translation, those empirical results are built on an unsound representational step. The correct strict DNF for a clause is obtained by an ordering construction (e.g. x1 ∨ x2 ≡ x1 ∨ (¬x1 ∧ x2)), which the paper itself uses in Example 6; Eq. (5) should be replaced accordingly and the experiments redone.","section":"§3.6.1, Eq. (18) and Eq. (5)"},{"comment":"The statement of Theorem 1 writes sφ(x) = -E(x), but the proof establishes sφ(x) = -1/ε min_h E(x,h); these are not the same object, since the right-hand side requires minimization over hidden units and normalization by ε. Relatedly, Eq. (13) writes sφ(x) = -1/(cε) min_h E(x,h), which cannot equal 1 for a satisfying assignment when min_h E = -ε. The theorem statement, Eq. (13), and the free-energy expressions in Eq. (12) should be corrected, including the missing minus sign in the denominator of Eq. (12) and the consistent use of the temperature τ in Eq. (11).","section":"§3.2, Theorem 1 and Eq. (13)"},{"comment":"Lemma 2 asserts that Gibbs sampling on the constructed RBM is equivalent to searching for a satisfying assignment, but the proof merely notes that energy minimization correlates with satisfaction; it gives no convergence or correctness argument for the sampling process. The paper's own §3.6.4 reports that Gibbs sampling often gets stuck in local minima for formulas with more than 40 variables, and proposes to declare formulas likely unsatisfiable when the free energy does not decrease after 1000 steps. That heuristic is not sound, because a local minimum is not evidence of unsatisfiability. The lemma should be weakened to a heuristic claim, and the coverage experiments in §3.5.1 should not be presented as a general equivalence between Gibbs sampling and model search.","section":"§3.3.1, Lemma 2"},{"comment":"The experimental comparison on the semantic image interpretation task is confounded: the text states that the rule (pt1 ∧ pt2) → (ppo ↔ ppt) was used only by LBM and not by the comparison systems DLN, CNLP, and LTN. The higher AUC reported for LBM in Table 3 can therefore be explained by the additional knowledge given to LBM, not by the LBM mechanism itself. A fair comparison requires either giving the same rule to the baselines or ablating the rule from LBM.","section":"§5, Table 3"}],"minor_comments":[{"comment":"The acceptance criterion is written as \"free energy is lower than or equal to − log(1 + exp(cϵ)\" and is missing a closing parenthesis; it should also specify that cϵ denotes c·ε with c=5 and ε=0.5.","section":"§3.5.1"},{"comment":"The roles of ST and SK are swapped between the conjunctive-clause setting in Theorem 1 and the clause setting in Eq. (3); using different symbols for the two settings would avoid confusion.","section":"§3.6.1, Eq. (5)"},{"comment":"The learning analysis in this section relies on an unproved assumption that for a large confidence value c∞ exactly one hidden unit is activated for each satisfying assignment; this should be stated as a heuristic or proved, since it is used to argue that a solution is found.","section":"§3.4"},{"comment":"The abstract contains the typo \"neurosynbolic\" in the final sentence; it should read \"neurosymbolic\".","section":"Abstract"}],"recommendation":"major_revision","confidential_remarks":"The manuscript is very close to the authors' previous AAAI paper [52]; most figures and tables are reproduced from that source. The genuinely new material is the SAT/MaxSAT extension, which currently rests on the erroneous CNF translation. If the conversion is repaired and the experiments are rerun, the technical contribution may be publishable; as it stands, the incremental contribution is largely a chapter-length exposition of prior work. The long survey and opinion sections are likely more appropriate for a book chapter than a research article, so the editor may wish to consider scope and novelty expectations."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Two things to know. The SDNF-to-RBM construction in Theorem 1 is sound and is honestly credited to your earlier AAAI 2023 paper; the chapter repackages it with context. The genuinely new piece is the claim that CNF can be translated directly via Eq. (18), and that claim is wrong. For a clause x1∨x2, with ST empty and SK={1,2}, Eq. (5) gives (¬x2∧x1)∨(¬x1∧x2), i.e. XOR. So the 'efficient CNF route' does not produce an RBM whose minima are the satisfying assignments of the CNF. The SAT experiments in Sec. 3.6.4 and the MaxSAT experiments in Sec. 4 use exactly this transformation, so those results don't test what they claim. This is a load-bearing flaw, not a typo.\n\nWhat's good: the SDNF construction is clear and correct, and the proof, modulo the -1/ε scaling and a sloppy theorem statement, holds. Lemma 3 on weighted knowledge bases is a reasonable extension. The survey of neurosymbolic AI and the placement of LBM relative to LLMs is readable and useful. The learning results on the ILP benchmarks are re-presented from [52] but are honestly labeled.\n\nSoft spots beyond the CNF error: Lemma 2 asserts Gibbs sampling is equivalent to model search without proof; the paper later admits local minima for >40 variables, so the coverage experiments are on a specially structured formula class. The semantic image experiment (Table 3) has no error bars on the comparison models and no code/data, so it's hard to assess. The MaxSAT comparison with Loandra on six instances is preliminary, and with the CNF encoding wrong, it's moot.\n\nWho should read this: someone wanting an accessible introduction to energy-based neurosymbolic reasoning, or a recap of the LBM idea. The SAT/MaxSAT sections should not be cited until Eq. (18) is fixed and the experiments redone. I'd send this to referees because the core SDNF theorem is worth having in print in a survey venue, but the verdict should be conditional on correcting the CNF transformation and re-running the affected experiments.","headline":"The SDNF-to-RBM construction is sound but is prior work; the new CNF translation (Eq. 18) is wrong and invalidates the SAT/MaxSAT experiments.","tokens_in":33196,"tokens_out":3741,"would_cite":false,"duration_ms":31972,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Every propositional logic formula can be built into a Restricted Boltzmann Machine whose minimum-energy states are exactly its satisfying assignments, turning logical reasoning into energy minimization.","keywords":["Neurosymbolic AI","Restricted Boltzmann Machines","Logical Boltzmann Machines","propositional logic","SAT solving","MaxSAT","energy-based learning","logical reasoning"],"falsifier":"Take a satisfiable random CNF with about 60 variables, compile it to an LBM, and run the paper's Gibbs-sampling procedure; if the sampler never reaches an energy minimum corresponding to a satisfying assignment within a fixed large number of steps while a symbolic solver confirms satisfiability, the claimed equivalence between sampling and reasoning fails for that instance class.","tokens_in":32076,"feed_emoji":"🧠","tokens_out":6166,"duration_ms":46662,"temperature":0.7,"pith_summary":"The paper claims that any propositional logic formula can be translated into a Restricted Boltzmann Machine (RBM) so that the formula's satisfying truth assignments are exactly the network's global energy minima. The resulting system, called the Logical Boltzmann Machine (LBM), therefore performs logical reasoning by searching for low-energy states. If correct, this gives a provably sound way to embed logical knowledge into a neural network and to add a verifiable reasoning module on top of deep networks that must respect constraints such as fairness or safety. The paper backs the claim with a proof, illustrative examples, and experiments on reasoning coverage, SAT and MaxSAT solving, and learning from data plus knowledge.","feed_headline":"Any logic formula turns into an energy-minimizing neural net","feed_subtitle":"A provably sound RBM construction makes logical reasoning a search for the lowest-energy state, with learning on top.","key_machinery":"The central object is the per-clause energy term $e_j(x,h_j) = -h_j(\\sum_{t\\in ST_j} x_t - \\sum_{k\\in SK_j} x_k - |ST_j| + \\varepsilon)$. When the clause's literals are exactly satisfied, the expression inside the parentheses equals $\\varepsilon$, so $e_j$ is minimized at $-\\varepsilon$ with $h_j = 1$; otherwise it is non-negative and minimized at $0$ with $h_j = 0$. Summing these terms over all clauses makes the total energy count how many clauses are violated, so finding a satisfying assignment is equivalent to finding a global minimum of the RBM's energy (or, with confidence values, its free energy). This construction is what lets reasoning be carried out by Gibbs sampling, gradient descent, or global optimization methods.","core_discovery":"The central claim is Theorem 1: any strict DNF (SDNF) formula $\\varphi \\equiv \\bigvee_j (\\bigwedge_{t\\in ST_j} x_t \\wedge \\bigwedge_{k\\in SK_j} \\neg x_k)$ can be mapped onto an RBM with energy function $E(x,h) = -\\sum_j h_j(\\sum_{t\\in ST_j} x_t - \\sum_{k\\in SK_j} x_k - |ST_j| + \\varepsilon)$, where $0<\\varepsilon<1$, such that $s_\\varphi(x) = -E(x)$. Because every well-formed formula can be converted into a full DNF and hence an SDNF, every propositional formula has such an RBM. The construction gives each conjunctive clause its own hidden unit; the clause contributes $-\\varepsilon$ to the minimized energy exactly when all its positive literals are true and all its negative literals are false, and $0$ otherwise, so the number of satisfied clauses is proportional to the negative energy. The paper extends the same idea to CNF, to weighted knowledge bases in the style of penalty logic, and to MaxSAT by minimizing free energy.","pith_inferences":["A testable extension is that the sampling efficiency reported here transfers to other structured formula classes only when the energy landscape has no deep local minima; random CNFs beyond 40 variables are predicted to defeat plain Gibbs sampling, which the paper already observes.","The construction implies an ordering of all truth assignments by energy, not just a satisfiability test; this ranking could be exploited for approximate reasoning, counting models, or sampling near-solutions, directions the paper mentions but does not develop.","If the equivalence holds for weighted knowledge bases, the same hidden-unit construction gives a natural way to revise knowledge during learning: start with weights from the logical rules and let contrastive divergence adjust them, which is what the LBM learning experiments do.","The free-energy confidence parameter $c$ provides a continuous knob between a smooth optimization landscape and a sharp satisfiability threshold; an adaptive schedule for $c$ during optimization would be a natural extension of the SAT experiments."],"forward_implications":["Any propositional knowledge base can be compiled into an RBM with weights and biases read directly off the formula, and the compilation carries a soundness guarantee: satisfying assignments and energy minima coincide.","MaxSAT becomes an energy-minimization problem, solvable by off-the-shelf optimizers such as dual annealing on the RBM's free-energy landscape, without training data or a symbolic SAT solver.","A verified LBM module can be placed on top of a convolutional or encoder-decoder network to enforce logical constraints during training, as demonstrated on a semantic image interpretation task.","Learning from data plus background knowledge in LBM outperforms a purely symbolic system, a purely neural system, and a state-of-the-art neurosymbolic system on five of seven benchmark datasets.","For a class of formulas with millions of possible assignments, LBM finds all satisfying assignments after sampling only about 0.37--0.75% of the search space, suggesting reasoning can be efficient despite exponential worst-case growth."],"supporting_citations":[{"why":"Supplies the LBM construction, the earlier empirical evaluation, and the figures and tables that this chapter reviews and extends.","marker":"[52]"},{"why":"Defines the equivalence between propositional knowledge and symmetric network energy that Theorem 1 adapts to restricted Boltzmann machines.","marker":"[37]"},{"why":"Provides the RBM architecture and the energy function that the translation algorithm targets.","marker":"[44]"},{"why":"Provides contrastive-divergence learning, used to train LBM and standard RBM baselines from data.","marker":"[19]"},{"why":"Provides the CILP++ neurosymbolic system and the seven benchmark datasets used in the learning comparison.","marker":"[13]"},{"why":"Provides the Aleph symbolic ILP baseline that LBM is compared against on the learning tasks.","marker":"[46]"},{"why":"Earlier mapping of SAT onto Boltzmann machines that LBM contrasts with its simpler two-layer RBM construction.","marker":"[17]"},{"why":"Earlier high-order Boltzmann machine approach to MaxSAT that motivates the LBM free-energy formulation.","marker":"[18]"},{"why":"Supplies the semantic image interpretation task, dataset, and logic tensor network setup used in the LBM logical-layer experiment.","marker":"[11]"}],"fun_headline_variants":["Every logic formula maps to an energy-minimizing RBM","Logic reasoning as energy search in a neural net","Provably sound: any formula becomes an RBM","Neurosymbolic reasoning: from logic to RBM energy","Turn any propositional logic into a Boltzmann machine"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that searching the RBM's energy landscape reliably reaches the global minima corresponding to satisfying assignments, which is asserted heuristically and which the paper itself reports can fail for formulas with more than 40 variables.","fun_headline_variants_meta":{"raw":{"variants":["Every logic formula maps to an energy-minimizing RBM","Logic reasoning as energy search in a neural net","Provably sound: any formula becomes an RBM","Neurosymbolic reasoning: from logic to RBM energy","Turn any propositional logic into a Boltzmann machine"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000293,"raw_usage":{"total_tokens":1760,"prompt_tokens":1049,"completion_tokens":711,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":665,"completion_tokens_details":{"reasoning_tokens":633}},"tokens_in":665,"tokens_out":711,"duration_ms":6123,"temperature":1.0,"reasoning_tokens":633,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T14:57:45.188949+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a satisfiable random CNF with about 60 variables, compile it to an LBM, and run the paper's Gibbs-sampling procedure; if the sampler never reaches an energy minimum corresponding to a satisfying assignment within a fixed large number of steps while a symbolic solver confirms satisfiability, the claimed equivalence between sampling and reasoning fails for that instance class.","supporting_citations":[{"cited_title":"Tran and Artur d’Avila Garcez","cited_arxiv_id":null,"evidence_quote":"Supplies the LBM construction, the earlier empirical evaluation, and the figures and tables that this chapter reviews and extends."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines the equivalence between propositional knowledge and symmetric network energy that Theorem 1 adapts to restricted Boltzmann machines."},{"cited_title":"Smolensky","cited_arxiv_id":null,"evidence_quote":"Provides the RBM architecture and the energy function that the translation algorithm targets."},{"cited_title":"Hinton, Simon Osindero, and Yee-Whye Teh","cited_arxiv_id":null,"evidence_quote":"Provides contrastive-divergence learning, used to train LBM and standard RBM baselines from data."},{"cited_title":"Fran¸ ca, G","cited_arxiv_id":null,"evidence_quote":"Provides the CILP++ neurosymbolic system and the seven benchmark datasets used in the learning comparison."},{"cited_title":"Srinivasan","cited_arxiv_id":null,"evidence_quote":"Provides the Aleph symbolic ILP baseline that LBM is compared against on the learning tasks."},{"cited_title":"Hernandez, F","cited_arxiv_id":null,"evidence_quote":"Earlier mapping of SAT onto Boltzmann machines that LBM contrasts with its simpler two-layer RBM construction."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Earlier high-order Boltzmann machine approach to MaxSAT that motivates the LBM free-energy formulation."},{"cited_title":"Donadello, L","cited_arxiv_id":null,"evidence_quote":"Supplies the semantic image interpretation task, dataset, and logic tensor network setup used in the LBM logical-layer experiment."}],"review_version":1}