{"id":"ee263657-9682-41ae-8b22-52fcecb4976a","arxiv_id":"2608.10755","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"PPProbe extracts minimal unsatisfiable subsets from probabilistic Datalog derivation graphs to identify and filter mutually inconsistent analysis alarms.","lead":"Probabilistic Datalog can emit alarms that each look plausible but can never occur together in a single possible world. PPProbe finds these impossible alarm combinations using minimal unsatisfiable subsets, reporting large speedups over generic MUS tools and a big reduction in the alarms developers must inspect.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Algorithm 6's exclusive-dependency replacement ignores dependency polarity: for n :- ¬v, n true entails ¬v, so the 'guaranteed UNSAT' candidate (M\\{v})∪{n} can be SAT, and MineMUS's unguarded Shrink would emit a non-conflict as an MUS.","rationale":"The reader's weakest assumption concerns the Boolean abstraction not enforcing least-fixpoint semantics, with positive recursion admitting cyclic models. That is a real gap in the paper's proof, but it primarily threatens completeness rather than soundness: the least fixpoint of the intended semantics is itself a model of the Φ equations, so any set UNSAT under Φ is also unsatisfiable in every actual possible world. The more load-bearing defect is in the bottom-up MUS inference of Algorithm 6. There, the paper asserts a 'guaranteed UNSAT' replacement without restricting the dependency to a positive body literal. Under Definition 4, a relation n with sole derivation n :- ¬v satisfies Γ[n] = S_n ∧ ¬Γ[v], so n true implies v false, not v true. The replacement candidate can therefore be SAT even when the original MUS is UNSAT. Since MineMUS calls Shrink directly on the candidate without a SAT check, this can manufacture spurious MUSes, directly contradicting the paper's central soundness claim. The paper's empirical comparison and domain framing are useful, but this correctness risk is concrete and localized; a small fix (checking SAT before Shrink, or restricting exclusive dependencies to positive literals and proving the guarantee) would resolve it. The verdict should remain conditional pending this check or a formal proof, so UNCHANGED is appropriate.","tokens_in":20836,"tokens_out":22180,"duration_ms":261964,"concrete_test":"Build the four-rule micro-benchmark exactly as described: 1.0::b. v :- b. a :- ¬v. n :- ¬v, with queries v, a, n. Confirm with Definition 5 and Φ that {v,a} is an MUS (UNSAT, both singletons SAT). Then run PPProbe's InferMUS on M={v,a} and inspect the candidate produced at Algorithm 6 line 4 for v. Independently check C={a,n} with CVC5 against Φ: it is SAT (v=false, a=true, n=true, S_a=S_n=true, S_v=false). If PPProbe emits {a,n} or any subset of it as an MUS, the exclusive-dependency guarantee is unsound; if it does not, determine whether the implementation restricts N to positive body literals or adds a SAT check before Shrink, and require that restriction or proof in the paper.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 6 and Algorithm 6 claim that if n depends solely on v, then C=(M\\{v})∪{n} is guaranteed UNSAT (line 4), and MineMUS (Algorithm 7) applies Shrink(C) without re-running CheckSat. Under the paper's own Boolean encoding (Definition 4), this guarantee holds only for positive dependencies: if n's sole rule is n :- ¬v, then Γ[n] = S_n ∧ ¬Γ[v], so Γ[n]=true forces Γ[v]=false. Replacing v by n can therefore turn an UNSAT set into a SAT set. Example: input b; v :- b; a :- ¬v; n :- ¬v. M={v,a} is an MUS: v true requires b, and a true requires ¬v. But C={a,n} is SAT by setting v=false, a=true, n=true. If N in line 2 includes negative body dependencies (the text does not exclude them), InferMUS passes SAT candidates to Shrink; a deletion-based shrink on a SAT formula cannot return a valid MUS, so the reported 'MUS' need not be a genuine conflict. This is a direct threat to the central soundness claim, independent of the least-fixpoint issue. The fixpoint concern is less decisive: least-fixpoint worlds are models of Φ, so Φ-UNSAT is still sound; the unproven direction risks completeness, not soundness.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces PPProbe, a tool for extracting minimal unsatisfiable subsets (MUSes) from probabilistic Datalog analyses. The authors formalize mutual inconsistency among output facts as MUSes over a Boolean encoding Φ of the derivation graph, and propose two optimizations: derivative sampling, which uses negative structural and statistical dependencies to prioritize candidate combinations, and bottom-up MUS inference, which derives new conflicts via logical replacement over the derivation graph. The tool is evaluated on 70 benchmarks from side-channel analysis, data race analysis, semantic diffing, and Bayesian networks, reporting higher MUS throughput than MARCO, ReMUS, and TOME, as well as substantial reductions in false alarms when MUSes are used as constraints in a MaxSAT filtering step.","tokens_in":21148,"tokens_out":8536,"duration_ms":89346,"significance":"If the reported results and the soundness claims hold, PPProbe would be a useful domain-specific MUS enumeration method for an emerging class of probabilistic program analyses. The paper has several strengths: it identifies a genuinely new problem (mutual inconsistency of probabilistic Datalog outputs), the implementation is artifact-backed, the evaluation covers multiple real-world domains, the ablations isolate the contribution of each optimization, and the stability analysis speaks to the randomness of the sampler. The claimed throughput gains over generic MUS enumerators are plausible in spirit, since the tool exploits derivation-graph structure that generic tools ignore. However, the paper's central soundness claim is currently not established: the bottom-up inference step contains a concrete unsoundness under negative dependencies, and the Boolean encoding's relation to least-fixpoint possible-world semantics is asserted rather than proven. These issues are local and fixable in principle, but they must be addressed before the contributions can be accepted.","major_comments":[{"comment":"The 'exclusive dependency' replacement is not sound when the dependency is negative. The paper does not restrict 'depends solely on v' to positive dependencies. Under the Boolean encoding of Definition 4, if n's only derivation is n :- ¬v, then Γ[n] = S_n ∧ ¬Γ[v], so Γ[n]=true forces Γ[v]=false. Replacing v by n can therefore turn an UNSAT set into a SAT set. Concretely, take input b and rules v :- b, a :- ¬v, n :- ¬v. Then M={v,a} is an MUS: v requires b, and a requires ¬v. But C=(M\\{v})∪{n}={a,n} is SAT by setting S_a=S_n=true, Γ[v]=false, and Γ[b]=true. Algorithm 7 then calls Shrink(C) without a prior CheckSat, since Algorithm 1 only calls Shrink after the UNSAT check in line 8. Running a deletion-based shrink on a SAT formula can return a set that is not an MUS of Φ, directly invalidating the soundness claim in Section 4 unless 'depends solely' is defined to exclude negative dependencies and the algorithm is modified accordingly.","section":"Section 6, Algorithm 6 (lines 3–5) and Algorithm 7"},{"comment":"The encoding Φ is asserted to characterize possible worlds but does not enforce least-fixpoint semantics. Section 3.1 defines the solution as the least fixpoint over the Herbrand universe, and only negation is required to be stratified; positive recursion is allowed. For a rule p :- p, the equation Γ[p] ↔ (S[p] ∧ Γ[p]) admits the spurious model Γ[p]=true with S[p]=true even when p has no derivation from input facts. Thus Φ-models can be a strict superset of possible worlds. This does not affect the UNSAT direction used for conflict detection—if Φ is unsatisfiable, no possible world exists—but it means the claim in Section 3.3 that joint satisfiability under Φ captures co-occurrence in a possible world is unproven, and the minimality guarantee of Definition 6 may not hold for actual conflicts: a proper subset can be Φ-SAT via a spurious model while being unsatisfiable in every possible world. The authors should either prove that every model of Φ extends to a least-fixpoint model (which is false for the p :- p example) or explicitly separate the soundness claim from the completeness/minimality claim.","section":"Section 3.2, Definition 4 and Section 3.3, Definition 5"},{"comment":"The paper asserts that replacing v by n in a known MUS yields a set 'guaranteed to be UNSAT' (Algorithm 6, line 4), and that blocking an alternative derivation d2 with a positive literal v' by adding the other members of an existing MUS M_alt is sound (lines 15–17). The second assertion relies on the fact that any model of Φ with M_alt\\{v'} true must have v' false, which is true only because M_alt is an MUS under Φ; this dependence should be stated explicitly. More importantly, the first assertion has no proof and, as shown in the previous comment, is false without a polarity condition. The section should include a formal invariant stating exactly which syntactic conditions make logical replacement preserve unsatisfiability, together with a proof, or the algorithmic claim should be weakened.","section":"Section 6, 'Logical Replacement' paragraph"}],"minor_comments":[{"comment":"The runtime entries are typeset without separators (e.g., '0.40.5 0.4 2.40.00.0 0.0 0.01.93.0 2.4 17.9'), which makes the values unreadable; please reformat the table so that each column is distinct.","section":"Table 2"},{"comment":"The caption of Figure 6 says 'Normalized MUS count', while the text describes normalized throughput relative to the best baseline. These terms should be reconciled, and the normalization base (per-domain best baseline) should be stated in the caption.","section":"Section 7.2 and Figure 6"},{"comment":"Algorithm 4 returns Root' as a set (S+∪S− minus Visited), but Algorithm 2 uses it as a single root; if the set is empty or contains multiple elements, the behavior is underspecified. Please clarify the intended selection rule or return type.","section":"Section 5.2, Algorithm 4"},{"comment":"The phrase 'Eightside-channel analysis benchmarks' is missing a space, and the table of benchmark statistics would benefit from a Total row so that the reader can verify the claimed count of 70 benchmarks directly.","section":"Section 7.1"},{"comment":"The proof of Theorem 1 is informal: it does not rigorously justify that satisfying assignments for v1 and v2 can always be combined when the dependencies on shared input facts have the same polarity, especially in the presence of intermediate derived facts and multiple derivations. Either a complete proof should be supplied, or the statement should be marked as a heuristic that guides sampling rather than as a theorem.","section":"Section 5.2, Theorem 1"}],"recommendation":"major_revision","confidential_remarks":"The paper addresses a timely problem and the experimental setup is substantial, but the central soundness claim is not currently supported because of the negative-dependency issue in Algorithm 6 and the unproven relationship between Φ-models and least-fixpoint possible worlds. These are technical, fixable issues rather than signs of methodological dishonesty; the artifact and benchmark evaluation are valuable. I would encourage the editor to request a revision that fixes the logical-replacement guarantee, proves or weakens the encoding claim, and re-runs the evaluation after the fix. The current form should not be accepted as-is."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Here's the short version: the paper identifies a genuine gap—probabilistic Datalog analyses can emit alarms that no single possible world realizes—and it's sensible to treat that as an MUS enumeration problem over the derivation graph. The derivation-aware sampling and bottom-up inference are new relative to the domain-agnostic MUS literature, and the evaluation spans four domains with reasonable baselines. But the central soundness claim does not survive close reading of Algorithm 6.\n\nThe concrete problem: in InferMUS (Algorithm 6), for any relation n that depends 'solely' on v, the paper replaces v by n in a known MUS M and claims (M\\{v})∪{n} is guaranteed UNSAT. That is only true when the dependency is positive. If n's only derivation is n :- ¬v, then Γ[n] = S_n ∧ ¬Γ[v]. Replacing v with n flips the polarity, so the candidate can become SAT. A minimal example: input b; v :- b; a :- ¬v; n :- ¬v. M={v,a} is an MUS, but {a,n} is SAT. MineMUS then runs Shrink on a SAT formula without a CheckSat guard, so it can emit a non-conflict as an MUS. Nothing in the text excludes negative body literals from N. This directly violates the definition of soundness in Section 4, and it also undermines the false-positive reduction numbers: if the MUS constraints aren't genuine conflicts, the Δ% figures are not a conservative lower bound on real false positives.\n\nThe least-fixpoint issue is real but less damaging. Definition 4 permits self-supported cyclic models, so Φ-SAT can over-approximate possible worlds. That threatens completeness (missed conflicts), not the UNSAT-direction soundness. Worth fixing with a proof or a tightened encoding, but not a load-bearing flaw.\n\nThe paper is otherwise honestly written. It doesn't fit parameters or assume conclusions; the benchmark suite is substantial and the throughput gains are large. The artifact is promised but no link is provided, which is a problem for a systems paper.\n\nBottom line: the problem formulation and sampling idea deserve referee time, and the flaw is fixable—add a polarity check to the replacement rule and re-run the evaluation. As it stands, though, the soundness guarantee and the headline reduction numbers are not established. I'd send it to review conditional on fixing that bug, and I'd be skeptical of the reported reductions until then.","headline":"The problem is real and the derivation-aware sampling idea is worth building on, but Algorithm 6's replacement rule is unsound under negative dependencies, so the central soundness claim needs repair before the results can be trusted.","tokens_in":21622,"tokens_out":3295,"would_cite":false,"duration_ms":33766,"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":"This paper claims that conflicting alarms in probabilistic Datalog analyses can be identified exactly as minimal unsatisfiable subsets of a Boolean encoding of the derivation graph, and that PPProbe enumerates these subsets soundly and…","keywords":["probabilistic Datalog","minimal unsatisfiable subsets","conflict extraction","derivation graph","MUS enumeration","static analysis","false alarm reduction"],"falsifier":"Run PPProbe on the program containing only the rule `0.5::p :- p.` (a positive recursive cycle with no base fact). The intended least-model semantics says p is false in every possible world, so the set `{p}` should be reported as unsatisfiable; if PPProbe reports `{p}` as satisfiable, the Boolean encoding has admitted a self-supported model and the claimed soundness of the abstraction is violated.","tokens_in":20640,"feed_emoji":"🧩","tokens_out":9028,"duration_ms":83255,"temperature":0.7,"pith_summary":"Probabilistic Datalog analyses return alarms with marginal probabilities, and a developer can easily be presented with two alarms that are each plausible in some possible world but that no single world contains together. This paper argues that those mutually exclusive output combinations are exactly the minimal unsatisfiable subsets (MUSes) of the Boolean encoding of the program's derivation graph, and that a specialized MUS enumerator called PPProbe can find them soundly and efficiently. PPProbe prioritizes candidate sets by exploiting negative structural and statistical dependencies in the derivation graph, then prunes the search by deriving new conflicts from old ones through logical replacement. If the claim is right, developers can automatically filter out alarm combinations that can never co-occur, and the paper reports an average 47.7% reduction in mutually inconsistent alarms across 70 benchmarks.","feed_headline":"New tool filters 47.7% of mutually inconsistent Datalog alarms","feed_subtitle":"PPProbe turns derivation graphs into Boolean constraints and enumerates the minimal conflict sets that generic MUS tools miss.","key_machinery":"The load-bearing object is the Boolean interpretation of the grounded derivation graph (Definition 4): each rule instance becomes an independent Bernoulli event variable $S[r]$, each fact becomes a Boolean variable $\\Gamma[v]$, and each derived fact is defined by $D_v = \\bigvee_{r \\in \\mathrm{Derv}(v)} (S[r] \\wedge \\bigwedge_{b^+ \\in B^+} \\Gamma[b^+] \\wedge \\bigwedge_{b^- \\in B^-} \\neg \\Gamma[b^-])$. This reduces the question 'can these output facts co-occur?' to a SAT problem over $\\Phi$, and a minimal unsatisfiable subset of output facts under $\\Phi$ is exactly a minimal conflict. The supporting mechanisms are the derivation graph itself: negative edges $h \\to b$ for each negated body literal $b$ drive derivative sampling, and recursive dependency sets $\\mathrm{Dep}^+$ and $\\mathrm{Dep}^-$ (input facts that support or oppose a relation) steer the sampler toward statistically negatively dependent pairs; logical replacement over the graph then generates new MUSes bottom-up.","core_discovery":"The central claim is that conflicts among output facts of a probabilistic Datalog program are exactly the minimal unsatisfiable subsets (MUSes) under the Boolean encoding $\\Phi$ of the grounded derivation graph, and that PPProbe enumerates these MUSes soundly. Soundness is defined as every produced MUS corresponding to a genuine conflict: the facts in the MUS cannot hold together in any valid interpretation, independent of the numeric probabilities. The two mechanisms that make enumeration efficient are derivative sampling, which targets combinations whose derivation trees share input facts with opposite polarity, and bottom-up MUS inference, which replaces facts in a known MUS by their derivation ancestors (or blocks alternate derivations) to synthesize new conflicts without extra solver calls. On 70 benchmarks from side-channel analysis, data race detection, semantic diffing, and Bayesian networks, PPProbe reports higher throughput than MARCO, ReMUS, and TOME, and the conflicts it finds yield a conservative false-positive reduction, averaging 47.7%.","pith_inferences":["The pipeline is insensitive to probability values, so the same conflict extractor would work for any probabilistic Datalog program regardless of how its rule probabilities were learned; the four-domain evaluation already suggests this portability, but the paper does not claim it as a general theorem.","The dependency polarity sets could double as an explanation mechanism: when PPProbe reports a conflict, the shared input fact appearing in Dep+ of one fact and Dep- of the other identifies the root cause, a feature the paper does not implement.","The reported reductions understate the benefit for individual alarms: they are computed on combinations, so a developer who simply drops alarms participating in any detected MUS would likely remove more than 47.7% of the alarm volume; this per-alarm metric is not reported.","If the least-fixpoint faithfulness gap in Definition 4 is real, then on programs with positive recursive cycles PPProbe could miss genuine conflicts (because the encoding over-approximates the possible worlds); testing this on synthetic recursion-only programs would separate the abstraction question from the tool's practical value."],"forward_implications":["If PPProbe is sound, any alarm set that is a superset of a detected MUS can be discarded without inspecting it, because no possible world realizes it.","The reduction percentages (69% for side-channel queries, 61% for data-race queries) are conservative lower bounds on the fraction of alarm combinations a developer can prune.","Because the encoding and enumeration ignore the concrete probability values, the same pipeline applies to any probabilistic Datalog program whose rule probabilities are learned or estimated differently.","The technique changes the workflow of probabilistic program analysis: instead of triaging every alarm, a developer first runs conflict extraction and only inspects alarms that survive the MUS-based filter.","Generic MUS enumerators that ignore derivation-graph structure time out on the same benchmarks, indicating that the structural guidance, not the SAT encoding alone, is responsible for the scalability."],"supporting_citations":[{"why":"Provides the seed-shrink MUS enumeration approach (MARCO) that PPProbe uses for the Shrink routine and as a primary baseline for throughput comparison.","marker":"[26]"},{"why":"ReMUS baseline enumerator against which PPProbe's MUS discovery throughput is measured.","marker":"[9]"},{"why":"TOME baseline enumerator, the strongest baseline on semantic diffing benchmarks, used for comparison.","marker":"[6]"},{"why":"ProbLog solver used to ground the probabilistic Datalog program and produce the queried output facts and derivation graph.","marker":"[13]"},{"why":"Soufflé Datalog engine whose resolution procedure is instrumented to extract the complete derivation graph for the encoding.","marker":"[21]"},{"why":"CVC5 SMT solver used for the satisfiability checks and MaxSAT queries that drive MUS enumeration and filtering.","marker":"[3]"},{"why":"Introduces the probabilistic Datalog rules used in the data-race benchmarks and motivates the need for handling uncertainty in program analysis.","marker":"[36]"},{"why":"Provides the probabilistic Datalog framework and side-channel benchmarks with correlated inputs that PPProbe is applied to.","marker":"[54]"},{"why":"Supplies the semantic diffing benchmarks and the Datalog formulation of synchronization differences that PPProbe analyzes.","marker":"[45]"}],"fun_headline_variants":["PPProbe exposes impossible alarm combos in probabilistic Datalog","MUS-based conflict extraction cuts false alarms by 47.7%","PPProbe finds minimal conflicts 24x faster than generic MUS tools","Eliminate mutually inconsistent alarms with PPProbe","Conflict extraction for probabilistic Datalog: 47.7% fewer false alarms"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The Boolean encoding of Definition 4 assumes that every satisfiable assignment to rule-event and fact variables corresponds to a genuine possible world, without enforcing Datalog's least-fixpoint semantics, so positive recursive derivations might create self-supported 'worlds' that the intended semantics rejects.","fun_headline_variants_meta":{"raw":{"variants":["PPProbe exposes impossible alarm combos in probabilistic Datalog","MUS-based conflict extraction cuts false alarms by 47.7%","PPProbe finds minimal conflicts 24x faster than generic MUS tools","Eliminate mutually inconsistent alarms with PPProbe","Conflict extraction for probabilistic Datalog: 47.7% fewer false alarms"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000514,"raw_usage":{"total_tokens":2505,"prompt_tokens":959,"completion_tokens":1546,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":575,"completion_tokens_details":{"reasoning_tokens":1455}},"tokens_in":575,"tokens_out":1546,"duration_ms":9181,"temperature":1.0,"reasoning_tokens":1455,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T18:00:12.210031+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run PPProbe on the program containing only the rule `0.5::p :- p.` (a positive recursive cycle with no base fact). The intended least-model semantics says p is false in every possible world, so the set `{p}` should be reported as unsatisfiable; if PPProbe reports `{p}` as satisfiable, the Boolean encoding has admitted a self-supported model and the claimed soundness of the abstraction is violated.","supporting_citations":[{"cited_title":"Liffiton, Alessandro Previti, Ammar Malik, and Joao Marques-Silva","cited_arxiv_id":null,"evidence_quote":"Provides the seed-shrink MUS enumeration approach (MARCO) that PPProbe uses for the Shrink routine and as a primary baseline for throughput comparison."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"ReMUS baseline enumerator against which PPProbe's MUS discovery throughput is measured."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"TOME baseline enumerator, the strongest baseline on semantic diffing benchmarks, used for comparison."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"ProbLog solver used to ground the probabilistic Datalog program and produce the queried output facts and derivation graph."}],"review_version":1}