{"id":"8cd34b2a-574a-4539-bf65-91e4511c7b0e","arxiv_id":"2501.03142","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"The authors apply co-activation graph analysis to state sets generated by model checking to rank neuron and feature importance in safe deep RL policies.","lead":"This paper links formal safety checks with a neuron co-activation analysis to see which parts of a trained reinforcement learning policy matter for safe behavior. It introduces a semi-global explanation tool for safety-critical reinforcement learning, though the demonstration uses small datasets and no statistical baselines.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Co-activation rankings in Sections 5.1 and 5.2 are computed from 12-state and 22-state correlation matrices; without stability checks, the claimed safety-specific neuron and feature rankings are not supported.","rationale":"The proposed combination is plausible: using policy model checking to supply externally labeled state sets is a sensible way to adapt co-activation graph analysis to RL safety, and the linked code repository is a point in the paper's favor. However, the experimental demonstration has a single load-bearing weakness: every graph statistic is estimated from very small state sets, and the paper contains no stability analysis. With 12 states, even a single added or removed state can materially change correlations, PageRank values, and Louvain communities, so the claimed differences between safety properties and between critical and non-critical states are not yet distinguishable from noise. This is the same assumption the reader flagged, so I agree with the reader's weakest-assumption analysis. The conditional verdict should remain in place until the bootstrap and permutation checks are run; if those checks show that rankings are unstable or that random labels produce similar differences, the verdict should move toward rejection or unverified. If the checks pass, the conditional could be lifted. I did not elevate the separate ambiguity in Eq. (2) about negative correlations in PageRank because the sample-size confound is already sufficient to place the current evidence in doubt.","tokens_in":13038,"tokens_out":7360,"duration_ms":75327,"concrete_test":"Stability and permutation check on the taxi environment: regenerate the 206-state dataset used in Section 5.2. (1) Draw 1000 bootstrap samples of size 12 from these 206 states, recompute the co-activation matrix, PageRank, top-50 neurons, and Louvain modularity for each sample, and report the distribution of top-50 Jaccard overlap and modularity differences. (2) Permute the critical/non-critical labels 1000 times and recompute the same statistics. If the observed 12-vs-206 differences in Section 5.1 fall within the bootstrap range of size-matched samples, or if the critical/non-critical differences are indistinguishable from the label-permutation baseline, the claimed safety-specific rankings are not supported.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim, that co-activation graph analysis \"correctly identifies significant and highly relevant neurons for the safety properties,\" depends on Pearson correlations computed over policy-model-checked state sets. Section 5.1 uses 12 states for P=1(♦ jobs=1) and 206 states for P=1(♦ jobs=2); Section 5.2 splits 206 states into 22 critical and 184 non-critical. With only 12 samples per neuron, the standard error of Pearson r is about 1/sqrt(9) ≈ 0.33, so the 2048-neuron co-activation matrix is dominated by sampling noise and many large spurious correlations will appear. PageRank and Louvain are deterministic functions of that noisy matrix, so the reported top-50 rankings, feature importance lists, modularity differences (0.29 vs 0.25, and 0.25 vs 0.23), and community overlaps can shift with one or two states. The comparison in Section 5.1 is also confounded by sample size: differences attributed to the safety property may instead reflect the 12-vs-206-state imbalance. The pruning checks show only that some selected features are safety-relevant; they do not establish that the co-activation ranking is stable or that a random feature would fail the same check. The limitations subsection states that the method supports \"labeled datasets of different sizes\" but gives no minimum-sample guidance, and no bootstrap, permutation, or random-baseline analysis is reported. Thus the current experimental evidence does not yet establish stable semi-global safety explanations.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a framework that combines probabilistic model checking of reinforcement learning (RL) policies with co-activation graph analysis. For a user-specified safety property, the framework builds the deterministic transition system induced by the trained policy, uses the Storm model checker to identify the states relevant to the property, optionally labels those states with a local explainability metric such as critical/non-critical status, and then constructs a neuron co-activation graph from activations over the resulting state set. PageRank and Louvain community detection are applied to rank neurons, identify important state features, and compare modularity and community overlap across labels. Experiments are reported on a taxi environment and a cleaning-robot environment, with two comparative settings: different safety properties (Section 5.1) and critical versus non-critical states (Section 5.2).","tokens_in":13366,"tokens_out":4373,"duration_ms":41939,"significance":"If the experimental concerns are resolved, the framework fills a legitimate gap between local and global explainable RL: it uses model checking to define semantically meaningful state subsets and transfers co-activation graph analysis from classification to sequential decision-making, with publicly available code and a coherent pipeline built on established tools. The main scientific value is the proposal of semi-global safety explanations and the demonstration that neuron-level graph analysis can be coupled with formal verification. However, the central claim that the method 'correctly identifies significant and highly relevant neurons for the safety properties' is currently supported only by small, unreplicated datasets and an external pruning reference, so the significance hinges on the robustness of the reported rankings.","major_comments":[{"comment":"The co-activation graph is computed from Pearson correlations over very small state sets: Section 5.1 reports 12 data points for P=1(♦ jobs=1) versus 206 for P=1(♦ jobs=2), and Section 5.2 reports 22 critical versus 184 non-critical states. With n=12, the standard error of a Pearson correlation is about 0.33, so the 2048-neuron correlation matrix is dominated by sampling noise and many large spurious correlations will appear. Since PageRank and Louvain are deterministic functions of that matrix, the reported top-50 rankings, feature importance lists, modularity differences (0.29 vs 0.25 and 0.25 vs 0.23), and community overlaps (97% and 93%) may shift substantially with one or two states. The paper provides no bootstrap, permutation, random-baseline, or replication analysis to establish stability, and the comparison in Section 5.1 is additionally confounded by the unequal sample sizes (12 vs 206). This directly undermines the claim in Section 5.3 that the method 'correctly identifies significant and highly relevant neurons'.","section":"Section 5.1 and Section 5.2"},{"comment":"The pruning validation used to support the feature rankings is cited from prior work (Gross and Spieker, 2024b) rather than performed and reported in this manuscript. The statements that pruning the identified feature neurons drops the reachability probability to 0.25 or 0 are presented as evidence, but no pruning experiment, ablation details, or quantitative results appear in this paper. Without reproducing the pruning check here or adding a random-feature control (e.g., pruning equally many randomly selected input features and showing they do not degrade the safety property), the conclusion that the co-activation rankings identify safety-relevant neurons is not supported by the evidence in this manuscript.","section":"Section 5.1 and Section 5.3"},{"comment":"The critical/non-critical labeling depends on a single threshold of 100 on the distance between the highest and lowest predicted Q-values, but no sensitivity analysis is provided for this threshold. Because the threshold determines the 22/184 split, the downstream neuron rankings, modularity values, and community structures could be artifacts of the chosen threshold rather than of the critical-state distinction. The paper should report results for at least two alternative thresholds or justify why the chosen threshold is not driving the conclusions.","section":"Section 5.2"},{"comment":"The limitation statement says the method 'supports labeled datasets of different sizes' without giving any guidance on minimum sample sizes or stability diagnostics. Given that the experiments use n=12 and n=22 for key subsets, this claim is too strong. The paper should either provide quantitative guidance (e.g., bootstrap confidence intervals or a minimum-correlation threshold) or explicitly downgrade the claim to describe the method as exploratory for very small state sets.","section":"Section 4.3"}],"minor_comments":[{"comment":"Equation (1) appears to have a typo: the second correlation argument should be A(j,l,S) rather than A(j,k,S), since the right-hand side currently does not depend on the layer index l.","section":"Section 3.3, Eq. (1)"},{"comment":"The heading 'Methodolodgy' is misspelled; it should be 'Methodology'.","section":"Section 4 heading"},{"comment":"The sentence 'These findings conform that our method correctly identifies...' should read 'confirm' rather than 'conform'.","section":"Section 5.3"},{"comment":"The captions of Figures 3 and 4 would be clearer if they explicitly stated which dataset label corresponds to each color, using the safety property notation from the text (e.g., P=1(♦ jobs=1) versus P=1(♦ jobs=2)).","section":"Figures 3 and 4"},{"comment":"The paper does not describe how neuron-level PageRank values are aggregated into state-feature importance rankings. Since features are attributes of states rather than neurons, the mapping from the highest-ranked neurons to the reported feature lists should be explained explicitly.","section":"Sections 5.1 and 5.2"}],"recommendation":"major_revision","confidential_remarks":"The proposed pipeline is coherent and the model-checking component is solid, but the experimental evaluation is the main blocker. The n=12 dataset and the lack of stability analyses are serious enough that the central claims are not yet supported. If the authors add bootstrap/permutation analyses, random baselines, a reproduced pruning validation, and threshold sensitivity, the paper could become publishable. The self-citations to COOL-MC and the prior pruning work are appropriate and transparent."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Co-activation graph analysis has been used on classifiers; this paper is the first to run it on RL policies using model-checked safety properties as labels. That combination is genuinely new and reasonably motivated: it fills a gap between local and global explanations. Credit where due: the pipeline is simple and coherent, Storm-based verification is established, the authors release code, and the idea of semi-global safety explanations is worth taking seriously.\n\nThe soft spots are mostly experimental. The two main analyses are built on very small state sets—12 states for one safety property, 22 critical vs 184 non-critical states for the other. Pearson correlations computed over 12 samples have huge standard errors, so PageRank and community structure can shift with one or two states. The paper reports no bootstrapping, no permutation tests, and no random baselines. The 12-vs-206 comparison also confounds 'different safety property' with 'different dataset size.' When the authors say pruning the top-ranked features violates the safety property, they are checking relevance, not stability; a random feature could fail the same check. The modularity differences (0.29 vs 0.25, 0.25 vs 0.23) are small and may be noise.\n\nNone of this kills the idea. The method is plausible, and for a demonstration paper the qualitative findings are reasonable. But the title-level claim—'correctly identifies significant and highly relevant neurons'—is not supported by the current evidence. The paper should be revised to include stability checks, larger state sets or explicit caveats about sample size, and at least one random-feature baseline. I would also like to see the pruning experiments described in more detail rather than cited from previous work.\n\nThis is a paper for the explainable-RL and safety-verification community. It is not a breakthrough, but it is a useful application with a reusable framework and an honest limitations section. I'd send it to peer review at a specialized venue, with the expectation that the authors add robustness analysis. I would not cite it in my own work yet, but I'd keep an eye on the revised version.","headline":"A plausible first step toward semi-global safety explanations for RL, but small state sets and absent stability checks leave the strong claims unbacked.","tokens_in":13823,"tokens_out":2521,"would_cite":false,"duration_ms":23986,"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":"The paper claims that co-activation graph analysis, with datasets labeled by model checking, identifies the neurons and features that determine whether a deep RL policy satisfies safety properties.","keywords":["Explainable Reinforcement Learning","Model Checking","Co-activation Graph Analysis","Safety Verification","PageRank","Louvain Community Detection","Deep Q-Learning","Semi-Global Explanations"],"falsifier":"Recompute the PageRank neuron rankings and community structures after deleting one state at a time from the 12-state one-job dataset, or after bootstrap resampling; if the top-neuron set or the claimed top features change materially, the conclusion that the method identifies safety-relevant neurons does not hold.","tokens_in":12861,"feed_emoji":"🧠","tokens_out":8272,"duration_ms":66784,"temperature":0.7,"pith_summary":"This paper proposes a framework that combines RL policy model checking with co-activation graph analysis to explain why a trained deep reinforcement learning policy is safe. Instead of explaining one state at a time or the whole policy at once, the method produces semi-global explanations: it builds a graph of which neurons tend to fire together over the states that satisfy a user-specified safety property, then ranks neurons and state features and detects functional neuron communities. The authors demonstrate on taxi and cleaning-robot environments that the top-ranked features match what actually breaks safety, since pruning those feature connections causes the verified safety probability to collapse. If the framework works as claimed, it gives safety engineers a way to turn formal verification results into interpretable maps of the network.","feed_headline":"Map neuron co-activation to expose which neurons keep RL policies safe","feed_subtitle":"Model-checked states provide the labels, so safety properties become ranked neurons and feature explanations.","key_machinery":"The central object is the co-activation graph, an undirected graph whose nodes are neurons and whose edge weights are the Pearson correlations between the neurons' activations over a labeled set of inputs. Labels come from the new step: an RL policy and an environment MDP are turned into a fully deterministic induced DTMC by querying the policy's action in each reachable state, a probabilistic model checker verifies a PCTL safety property, and the states relevant to that property become the dataset. PageRank on the weighted graph ranks neuron importance, community detection finds functional modules, and comparing graphs built under different labels (different safety properties, or critical versus non-critical states) exposes which neurons and features carry each property. This carries the argument because the ranked neurons and features are then checked by pruning their connections and re-verifying the property.","core_discovery":"The central claim is that co-activation graph analysis, when fed datasets labeled by model checking, identifies the neurons and state features that determine whether an RL policy satisfies safety properties. On the taxi domain, the most important feature neurons for completing two jobs are the passenger's destination and the number of jobs completed, and pruning those connections drops the two-job reachability probability to 0.25; the most important features for completing one job are fuel level, destination x-coordinate, and jobs completed, and pruning them drops the probability to zero. Comparing critical against non-critical states under the same safety property reveals different top neurons and different feature importances, while Louvain communities show roughly 93-97% overlap, indicating largely shared processing regions. The paper's validation is that these pruning results \"confirm that our method correctly identifies significant and highly relevant neurons for the safety properties.\"","pith_inferences":["A natural extension not pursued here is to use the PageRank rankings directly as a pruning criterion, removing low-ranked neurons while re-verifying the safety property to obtain smaller, still-safe policies.","Because the label datasets are tiny (12 states in one case, 22 critical states in another), a bootstrap or leave-one-state-out stability test would tell whether the rankings are signal or artifacts of a few states.","The semi-global explanation idea could be applied to other policy properties besides safety, such as robustness or fairness constraints, as long as a labeler over reachable states exists.","One could test whether the co-activation graphs predict safety violations in a new environment region by using the ranked features to construct counterexamples."],"forward_implications":["For the taxi policy, the top features for finishing two jobs are passenger destination and jobs completed; pruning them reduces the two-job reachability probability from 1 to 0.25.","For finishing one job, top features are fuel level, destination x-coordinate, and jobs completed; pruning them drops one-job reachability to zero.","Critical and non-critical states under the same property produce different top neurons and feature rankings, so local state importance labels can be lifted to semi-global explanations.","Community overlap of 93-97% across labels suggests most of the network is shared and only a small set of neurons and features differentiates safety-relevant behavior.","The same method transfers to a second environment (cleaning robot), where feature importance rankings were identical for two safety properties and modularities were 0.37 and 0.35."],"supporting_citations":[{"why":"Supplies the co-activation graph method: nodes are neurons, edge weights are activation correlations, and PageRank highlights important neurons.","marker":"Horta et al., 2021"},{"why":"Defines the co-activation correlation formula and the PageRank update rule used to build and rank the graphs.","marker":"Selani and Tiddi, 2021"},{"why":"Provides the model-checking pipeline that builds the induced DTMC from the RL policy and environment and generates the states satisfying each safety property.","marker":"Gross et al., 2022"},{"why":"Supplies the probabilistic model checker used to verify the PCTL safety properties on the induced DTMC.","marker":"Hensel et al., 2022"},{"why":"Provides the community detection algorithm used to identify and compare functional neuron clusters.","marker":"Blondel et al., 2023"},{"why":"Supplies the pruning-and-reverification method used as the external validation that the identified features are safety-relevant.","marker":"Gross and Spieker, 2024b"},{"why":"Supplies the explainable-RL context and the critical-state labeling idea used to split the dataset into critical and non-critical states.","marker":"Milani et al., 2024"}],"fun_headline_variants":["Prune safety-critical neurons and RL reachability drops sharply","Co-activation graphs rank neurons by RL safety importance","Model-checked RL policies: which neurons really ensure safety?","Safety-critical neurons for RL: co-activation graph analysis","Explainable RL: co-activation graphs reveal safety neurons"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The method assumes that Pearson correlations computed over the model-checked state sets—sometimes just 12 states, with a critical/non-critical split of 22 versus 184—are stable enough for PageRank and community-detection rankings to be meaningful, yet it does not test this stability.","fun_headline_variants_meta":{"raw":{"variants":["Prune safety-critical neurons and RL reachability drops sharply","Co-activation graphs rank neurons by RL safety importance","Model-checked RL policies: which neurons really ensure safety?","Safety-critical neurons for RL: co-activation graph analysis","Explainable RL: co-activation graphs reveal safety neurons"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001026,"raw_usage":{"total_tokens":4244,"prompt_tokens":785,"completion_tokens":3459,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":401,"completion_tokens_details":{"reasoning_tokens":3378}},"tokens_in":401,"tokens_out":3459,"duration_ms":26143,"temperature":1.0,"reasoning_tokens":3378,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T21:52:21.079964+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Recompute the PageRank neuron rankings and community structures after deleting one state at a time from the 12-state one-job dataset, or after bootstrap resampling; if the top-neuron set or the claimed top features change materially, the conclusion that the method identifies safety-relevant neurons does not hold.","supporting_citations":[{"cited_title":"and Tiddi, I","cited_arxiv_id":null,"evidence_quote":"Defines the co-activation correlation formula and the PageRank update rule used to build and rank the graphs."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the model-checking pipeline that builds the induced DTMC from the RL policy and environment and generates the states satisfying each safety property."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the explainable-RL context and the critical-state labeling idea used to split the dataset into critical and non-critical states."}],"review_version":1}