{"id":"1ae26e05-4d33-4545-bf42-2b768284ccf5","arxiv_id":"2412.14814","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Answer Set Networks compile grounded Answer Set Programs into graph neural networks and solve them with GPU message passing, giving large speedups on neural-symbolic reasoning tasks.","lead":"Answer Set Networks turn logic programs into graphs of truth-value nodes and solve them by passing messages on a GPU, instead of running slower CPU answer-set solvers. The paper shows the approach speeding up MNIST-style neuro-symbolic learning, logic-guided fine-tuning of a large language model, and drone route planning over Paris.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The subset-minimal model reduction (Eq. 7) is stated backwards: it removes subset models and keeps supersets, so even a perfect message-passing pass would return non-answer-set models; ASN's central correctness claim is unsupported.","rationale":"The central claim of the paper is that ASN computes stable models of grounded tight ASP programs and thereby enables GPU-accelerated neural-symbolic solving. The reader flagged the unproved equivalence between Eq. 5 plus Eq. 7 and stable-model semantics; I agree that this is the load-bearing step. The concern is more severe than a missing proof: Eq. 7 as stated is internally inconsistent with subset-minimality. Because the paper's own Eq. 6 defines element-wise conjunction to return the smaller model when models are comparable, the set-builder condition in Eq. 7 excludes the smaller model and retains the larger one. This is precisely the opposite of what answer-set semantics requires. The paper does provide code and empirical evaluations, which is real supporting evidence, but those experiments do not validate exactness of the solver on the core reduction step. The MNIST-Addition, ProMis, and LLM fine-tuning results all depend on the solver returning answer sets, so this bug, if present in code, invalidates the reported results. If the code happens to implement a corrected reduction, the paper still needs to state and prove the correct equivalence. Either way, the submission as written cannot be accepted as a correct ASP solver; a revised version with a corrected reduction formula and a formal correctness argument could be reassessed, so my recommendation is REJECT rather than a more severe label.","tokens_in":16296,"tokens_out":10712,"duration_ms":103630,"concrete_test":"Run the released ASN code (github.com/ml-research/answersetnetworks) on the grounded tight program `a | b. b.` and compare returned models with clingo; the true answer set is {b}. Then, as a pure analytical check, apply Eq. 7 to bit-vectors for {b} and {a,b}: the formula returns {a,b}. If ASN returns {a,b} or the code's reduction differs from Eq. 7, the formal claim fails; if ASN returns {b}, the paper's Eq. 7 is still incorrect as written and must be fixed.","verdict_should_be":"REJECT","load_bearing_attack":"Reader's weakest assumption correctly locates the unproved step, but the problem is sharper than a missing proof. In Eq. 7, for interpretations I_i ⊂ I_j, element-wise conjunction gives m_i ⊗ m_j = m_i (Eq. 6's first case). The retention condition 'm_i ⊗ m_j ≠ m_i' is then false, so I_i is removed; the superset I_j is kept. For example, on `a | b. b.` the candidate models after definitization and message passing are {b} and {a,b}; Eq. 7 drops {b} and returns {a,b}. True stable models are just {b}. Thus the stated reduction selects non-minimal interpretations, not answer sets. If the released implementation uses this formula, ASN is not solving ASP; if it uses a different formula, the paper's central specification is wrong and needs correction plus a proof that Eq. 5 fixed points of definitives combined with corrected reduction equal stable-model semantics.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces Answer Set Networks (ASN), a graph-neural-network-based solver for grounded, tight answer set programs. The authors propose a compilation from ASP-Core-2 programs into heterogeneous 'Reasoning Graphs,' a choice-definitization step for disjunctive and choice rules, iterative message passing over the graph, and a model-reduction step intended to select subset-minimal models. The resulting solver is embedded in the SLASH neural-probabilistic programming framework and evaluated on three tasks: abductive fine-tuning of an LLM, probabilistic mission design for UAVs over Paris, and MNIST-Addition. The main claims are that ASN provides GPU-parallel ASP solving and outperforms existing CPU-bound NeSy systems.","tokens_in":16541,"tokens_out":4500,"duration_ms":33604,"significance":"If the central correctness claim were established, the paper would make a useful contribution: a GPU-batched, parallelizable approach to solving tight ground ASP programs within neural-symbolic pipelines, with a concrete implementation, code release, and a first demonstration of DPPL-guided LLM fine-tuning. The experimental results on MNIST-Addition and the Paris-scale ProMis map are suggestive of real practical speedups. However, the paper currently lacks a proof of the equivalence between the proposed message-passing/model-reduction pipeline and stable-model semantics, and the model-reduction formula as written is demonstrably backwards. The strengths are the breadth of the evaluation and the clear presentation of the compilation scheme, but the central solver semantics must be corrected and proven before the performance claims can be accepted.","major_comments":[{"comment":"The subset-minimal reduction in Eq. (7) is stated backwards. For two interpretations I_i ⊂ I_j, element-wise conjunction (Eq. (6)) gives m_i ⊗ m_j = m_i, so the retention condition m_i ⊗ m_j ≠ m_i is false and I_i is removed while the superset I_j is kept. For example, on the program `a | b. b.`, the candidates after definitization and message passing include {b} and {a,b}; Eq. (7) drops {b} and returns {a,b}, although the unique stable model is {b}. The correct condition for keeping a model that is not a superset of any other candidate model is m_i ⊗ m_j ≠ m_j for all j (or an equivalent formulation over all pairs, not only j > i). As written, the central claim that ASN returns answer sets is invalidated; the formula must be corrected and a proof supplied that the corrected reduction together with the message-passing fixed points yields exactly the stable models.","section":"Model Reduction, Eq. (7)"},{"comment":"There is no theorem or formal argument establishing that the pipeline is sound and complete. In particular, the paper does not prove that (a) enumerating all definitives of disjunctive and choice rules covers exactly the answer sets of the original program, and (b) the fixed point of the Eq. (5) update on a definitive's Reasoning Graph equals the unique stable model of that definitive for tight programs. The text asserts these properties ('The RG representing these definitives can be directly constructed...'), but the equivalence is load-bearing: every experimental result depends on ASN returning the correct stable models. This gap should be closed with a precise statement and proof, or by citing an existing theorem that applies verbatim to this construction.","section":"Choice definitization and Message-Passing"},{"comment":"The claimed speedup factors of 194x over ProbLog and 137x over SLASH are not measured at full resolution: the baselines were run on a 500^2 grid and their times linearly extrapolated to the 6500^2 grid, while ASN was run on the full grid. Linear extrapolation of CPU solver time with grid size is an assumption, not a measurement, and the resulting 'three orders of magnitude faster' claim should be either supported by a scaling argument with evidence or qualified as an extrapolation. At minimum, report the measured 500^2 times for all systems, the extrapolation formula, and any observed scaling behavior.","section":"Experiments, Q2 (ProMis)"}],"minor_comments":[{"comment":"The index range in Eq. (7) says i ∈ {1,...,n}, but the set being filtered is over interpretations {I_1,...,I_k}; the bound should be k, not n.","section":"Model Reduction"},{"comment":"The sentence 'Each answer set of the original program consists of the program definitives' is unclear and should be reworded; presumably each answer set of the original program corresponds to at least one definitive whose models are subsets of it, or similar.","section":"Choice definitization"},{"comment":"The notation g_{v,l} = β_{v,l} ⋄_{v,l} is used as a guard, but its type is not defined; clarify whether it is a Boolean predicate or a relation applied to the aggregated value, and define the comparison operators consistently.","section":"Message-Passing, Eq. (5)"},{"comment":"There is a typo in the query atom 'daugther' (line 31), and the query constraints use 'not relation(p1,p2,<relation>)' while the body rules use relation(X1,X2,<relation>); please align the naming and check the spelling.","section":"Appendix B, Listing 1"},{"comment":"The caption states that ASN 'renders Paris in 56m,' but the color scale and coordinate reference for the map are not described; add a legend and clarify whether the colored areas correspond to probability thresholds.","section":"Figure 5b"}],"recommendation":"major_revision","confidential_remarks":"The core idea is promising and the experimental scope is impressive, but the correctness of the solver is the paper's central claim and Eq. (7) is currently wrong as written. Even with a corrected reduction, the missing equivalence proof for message passing and definitization is a substantial gap. This seems fixable within the scope of a revision, so I recommend major revision rather than rejection. The novelty relative to the authors' prior SLASH work is moderate, but the GPU-parallel solver and the LLM fine-tuning demonstration provide a credible increment."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The headline is that this paper's central correctness claim is unsupported, and the printed reduction formula is backwards. Eq. 7 removes subset models and keeps supersets, so even if message passing worked perfectly, the output would not be answer sets. E.g., on `a|b. b.` the candidates {b} and {a,b} are reduced to {a,b}, whereas the only answer set is {b}. So the solver as specified is not solving ASP.\n\nThere is genuinely new material here: a systematic compilation of grounded ASP-Core-2 (facts, rules, choice rules, aggregates, constraints, queries) into heterogeneous Reasoning Graphs with typed nodes and edges, and a GNN message-passing scheme to propagate truth values in parallel. The GPU batching idea is sensible, and the MNIST-addition and Paris drone experiments at least show the pipeline can be scaled beyond toy size. The LLM fine-tuning with a DPPL is a first, though the wall-clock gains over the non-logic baseline are about 2.8x, not the \"order of magnitude\" claimed for epochs.\n\nThe soft spots beyond the backwards formula: there is no proof that message passing (Eq. 5) converges to the models of the definitized program, nor that the fixed point is reached in finite time. The ProMis speedup over ProbLog/SLASH is a linear extrapolation from a 500^2 grid multiplied by 169, not a measured 6500^2 run; the 56m for ASN itself is real, but the comparison numbers are estimates. Table 1 reports averages over five seeds but no variance. The tight (acyclic) restriction is stated, which is fine, but it means the claim of general ASP solving is narrower than the abstract suggests.\n\nIf the released code uses the printed Eq. 7, ASN is not returning answer sets; if it uses a different formula, the paper's specification is wrong and needs correction plus a correctness proof. Either way, the work as submitted cannot be trusted as an ASP solver. That said, the compilation and batching machinery is a solid step toward GPU-native NeSy, and the problems are fixable with a careful semantics argument and a reference implementation audit.\n\nFor a reader in NeSy or GPU-based logic solving, this is worth a look as a flawed but idea-rich proposal. I would not cite it in its current form. If it came across my desk, I'd send it to review anyway, because the idea is important and the flaws are correctable, but I'd expect major revision.","headline":"The GPU compilation idea is promising, but the model reduction in Eq. 7 is backwards, so the paper's core claim of solving ASP is unsupported.","tokens_in":17041,"tokens_out":3990,"would_cite":false,"duration_ms":34166,"reading_group":"maybe","serious_thinker":"no","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Answer Set Networks compile grounded, tight answer set programs into Reasoning Graphs and solve them with GPU-parallel message passing, outperforming CPU-bound neural-symbolic systems and enabling logic-guided LLM fine-tuning and…","keywords":["Answer Set Programming","Graph Neural Networks","Neural-Symbolic AI","Deep Probabilistic Logic Programming","Reasoning Graphs","Model Reduction","LLM Fine-tuning","UAV Navigation"],"falsifier":"Encode a suite of grounded tight answer set programs—including aggregates and choice rules—as Reasoning Graphs, run ASN, and compare its output against a trusted solver such as clingo; any program where ASN returns a non-stable model, misses a stable model, or fails to converge would refute the claimed equivalence.","tokens_in":16142,"feed_emoji":"🧠","tokens_out":10912,"duration_ms":73618,"temperature":0.7,"pith_summary":"Answer set programming (ASP) lets neural-symbolic systems encode constraints declaratively, but computing stable models is slow and confines the symbolic part to the CPU. The paper proposes Answer Set Networks (ASNs), which compile grounded, tight ASP programs into heterogeneous graphs called Reasoning Graphs, then solve them by batched, GPU-parallel message passing. The authors claim that the fixed point of this message passing, followed by a subset-minimality filter, recovers exactly the program's stable models, and that ASNs outperform CPU-bound neural-symbolic solvers on multiple tasks. They also demonstrate two new applications: logic-guided fine-tuning of large language models that mitigates the Reversal Curse, and large-scale UAV routing under aviation law that renders a $169\\,\\mathrm{km}^2$ map of Paris. If the claims hold, ASNs would make ASP-based neural-symbolic AI both faster and better integrated with deep learning on modern hardware.","feed_headline":"GPU solver for answer set programs beats CPU rivals by up to 194x","feed_subtitle":"Logic-based neural-symbolic AI gets a GPU speedup, plus first logic-guided fine-tuning of LLMs.","key_machinery":"The central objects are Reasoning Graphs (RGs): heterogeneous graphs with node types for conjunctions, disjunctions, counts, sums, minima, maxima, and the constant nodes $\\top$ and $\\bot$, with edge weights in $\\{-1, 1\\}$ for logical edges or term weights for aggregate edges. A grounded ASP program is compiled into an RG element-by-element following the ASP-Core-2 syntax. Solving proceeds in three steps: choice definitization, which instantiates separate graph copies for every combination of disjunctive and choice selections; message passing, in which each node updates its Boolean value from its incoming neighbors according to its type, with aggregate nodes comparing weighted sums or counts against their guards; and model reduction, which filters the resulting interpretations by subset-minimality using bitwise operations so that only the program's stable models remain. The same framework also embeds Neural-Probabilistic Predicates (NPPs) from SLASH, letting neural networks or probabilistic circuits supply atom probabilities inside the program.","core_discovery":"The paper's central claim is that any grounded, tight answer set program can be 'neurally compiled' into a Reasoning Graph—a heterogeneous graph whose nodes stand for atoms, conjunctions, disjunctions, and aggregate literals, with special source and sink nodes $\\top$ and $\\bot$—and that stable models can be extracted by iterating a Boolean message-passing update until it reaches a fixed point, then discarding all interpretations that are not subset-minimal. Choice and disjunctive rules are handled by 'definitization': generating copies of the graph for each possible selection of disjuncts and solving them all in parallel on the GPU. The authors further claim that this approach is not only a faithful solver but a fast one: on MNIST-Addition it trains epochs up to $3.4\\times$ faster than SAME, on the ProMis UAV mission-design problem it is $137\\times$ faster than SLASH and $194\\times$ faster than ProbLog, and it can fine-tune Llama2-7B with logical constraints to overcome the Reversal Curse.","pith_inferences":["If the fixed-point equivalence is formally proved, ASN could serve as a drop-in GPU replacement for traditional solvers on tight ASP domains, enabling high-throughput query answering for robotics, planning, and constraint satisfaction.","The same graph construction may be made fully differentiable by replacing Boolean updates with soft logic, allowing end-to-end gradient flow from a loss through the solver into the neural predicates—a direction the paper lists as future work.","Choice definitization enumerates all combinations and grows combinatorially with the number of choice rules; sampling or pruning definitives would trade completeness for speed in programs with many choices.","The Reversal Curse result is tested only on family relations, so tests on other domains—geographic, scientific, or common-sense knowledge—would show whether logic-guided fine-tuning transfers beyond the paper's setting."],"forward_implications":["ASN provides a GPU-parallel path from ASP to neural learning, so neural-symbolic systems can keep the symbolic solver on the same accelerator as the neural network instead of shuttling between CPU and GPU.","The ProMis speedups (137× over SLASH, 194× over ProbLog) indicate that large-scale, legal-constraint-aware planning—such as the Paris UAV map rendered in 56 minutes—becomes practical and could extend to real-time re-planning.","Logic-guided fine-tuning with ASN reduces the Reversal Curse in LLMs, converging in 9 epochs where an unguided baseline needs 72–96 epochs, suggesting that symbolic constraints can act as a training signal for language models.","Because all choice definitives are solved in parallel batches, ASN's speed scales with GPU width, and the paper shows a clear batch-size trade-off between per-epoch time and convergence on MNIST-Addition.","The compilation covers the full ASP-Core-2 language, so any tight grounded program expressible in that standard can in principle be solved by ASN."],"supporting_citations":[{"why":"Provides the grASP graph-based ASP solving paradigm that motivates the Reasoning Graph representation.","marker":"Li 2021"},{"why":"Defines SLASH and Neural-Probabilistic Predicates, the DPPL framework into which ASN is integrated as a solver.","marker":"Skryagin et al. 2022"},{"why":"Introduces SAME and the scalable NPP semantics used as a baseline and for the MNIST-Addition and ProMis experiments.","marker":"Skryagin et al. 2023"},{"why":"Clingo is the CPU solver that SLASH uses and that ASN is compared against for speed and correctness.","marker":"Gebser et al. 2011"},{"why":"DeepProbLog provides the MNIST-Addition benchmark and a baseline NeSy system.","marker":"Manhaeve et al. 2018"},{"why":"ProMis defines the UAV mission-design task with hybrid probabilistic logic that ASN scales to cover Paris.","marker":"Kohaut et al. 2023"},{"why":"The Reversal Curse dataset and phenomenon that ASN's abductive fine-tuning targets.","marker":"Berglund et al. 2024"},{"why":"ASP-Core-2 is the standard input language that ASN's neural compilation translates into Reasoning Graphs.","marker":"Calimeri et al. 2020"}],"fun_headline_variants":["Answer Set Networks: GPU logic solver up to 194x faster","Neural compiler turns logic programs into GPU-parallel graphs","Logic-guided LLM fine-tuning meets 194x GPU speedup","Stable models on GPU: beat ProbLog by 194x","GPU-based logic solver for neural-symbolic AI, up to 194x"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the fixed point of the message-passing update, together with the subset-minimal reduction, exactly reproduces the stable-model semantics of every grounded tight answer set program; this equivalence is asserted but not proved.","fun_headline_variants_meta":{"raw":{"variants":["Answer Set Networks: GPU logic solver up to 194x faster","Neural compiler turns logic programs into GPU-parallel graphs","Logic-guided LLM fine-tuning meets 194x GPU speedup","Stable models on GPU: beat ProbLog by 194x","GPU-based logic solver for neural-symbolic AI, up to 194x"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001084,"raw_usage":{"total_tokens":4545,"prompt_tokens":972,"completion_tokens":3573,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":588,"completion_tokens_details":{"reasoning_tokens":3481}},"tokens_in":588,"tokens_out":3573,"duration_ms":19550,"temperature":1.0,"reasoning_tokens":3481,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T11:52:58.930386+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Encode a suite of grounded tight answer set programs—including aggregates and choice rules—as Reasoning Graphs, run ASN, and compare its output against a trusted solver such as clingo; any program where ASN returns a non-stable model, misses a stable model, or fails to converge would refute the claimed equivalence.","supporting_citations":[{"cited_title":"S.; and Kersting, K","cited_arxiv_id":null,"evidence_quote":"Defines SLASH and Neural-Probabilistic Predicates, the DPPL framework into which ASN is integrated as a solver."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Introduces SAME and the scalable NPP semantics used as a baseline and for the MNIST-Addition and ProMis experiments."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Clingo is the CPU solver that SLASH uses and that ASN is compared against for speed and correctness."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"DeepProbLog provides the MNIST-Addition benchmark and a baseline NeSy system."},{"cited_title":"S.; Eggert, J.; and Kersting, K","cited_arxiv_id":null,"evidence_quote":"ProMis defines the UAV mission-design task with hybrid probabilistic logic that ASN scales to cover Paris."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"ASP-Core-2 is the standard input language that ASN's neural compilation translates into Reasoning Graphs."}],"review_version":1}