Paper deep dive
CDRL: Certification-Driven Reinforcement Learning for Neutrino Flavor Model Discovery
Piyush Jha, Jake Rudolph, Victoria Knapp-Pérez, Max Fieg, Aishik Ghosh, Vijay Ganesh
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 91%
Last extracted: 8/24/2026, 5:05:52 AM
Summary
The paper introduces Certification-Driven Reinforcement Learning (CDRL), a framework that enhances scientific model discovery by integrating structured feedback from symbolic reasoning tools into reinforcement learning. Unlike traditional RL that relies on scalar rewards, CDRL uses certificates generated when candidates violate domain constraints to create reusable logical constraints (conflict clauses). These constraints prune the search space via Boolean Constraint Propagation, preventing the agent from revisiting invalid regions. The method is evaluated on neutrino flavor model discovery in theoretical particle physics, demonstrating significant improvements in valid model discovery rates and efficiency compared to state-of-the-art RL approaches like AMBer. Additionally, the framework supports post-hoc extraction of interpretable rules from search trajectories, which can be reused as soft constraints to further improve performance.
Entities (10)
Relation Signals (9)
CDRL → appliedto → Neutrino Flavor Model Discovery
confidence 95% · We evaluate CDRL on neutrino flavor model discovery in theoretical particle physics
CDRL → uses → Symbolic Reasoning Tools
confidence 95% · CDRL leverages structured feedback from symbolic reasoning tools.
Certificate → convertedto → Reusable Constraints
confidence 93% · CDRL converts these certificates into reusable constraints that eliminate classes of invalid solutions
CDRL → outperforms → AMBer
confidence 92% · CDRL achieves up to 1.95× higher valid model rates and up to 6.33× higher neutrino model rates than AMBer
Piyush Jha → affiliatedwith → Georgia Institute of Technology
confidence 90% · Piyush Jha Affiliation: School of Physics, Georgia Institute of Technology, USA
Max Fieg → affiliatedwith → Fermilab
confidence 90% · Max Fieg Affiliation: Particle Theory Department, Fermilab, USA
Certificate → generatedby → Symbolic Reasoning Tools
confidence 90% · these tools produce certificates identifying the actions responsible for failure.
Reusable Constraints → enforcedby → Boolean Constraint Propagation
confidence 88% · enforced during search by Boolean Constraint Propagation (BCP)
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Many scientific discovery problems require searching combinatorial hypothesis spaces under complex domain constraints. Reinforcement learning (RL) offers a promising approach, but existing methods rely on scalar rewards that provide limited information about why candidate solutions fail, leading agents to repeatedly explore invalid regions. We introduce Certification-Driven Reinforcement Learning (CDRL), a framework that leverages structured feedback from symbolic reasoning tools. When a candidate violates domain constraints, these tools produce certificates identifying the actions responsible for failure. CDRL converts these certificates into reusable constraints that eliminate classes of invalid solutions and guide exploration toward valid regions. We evaluate CDRL on neutrino flavor model discovery in theoretical particle physics, where the hypothesis space exceeds $10^{26}$ possible models, and compare it with the state-of-the-art RL approach previously used for this task. Across three theory spaces, CDRL achieves up to 1.95$\times$ higher valid model rates and up to 6.33$\times$ higher neutrino model rates while evaluating up to 4$\times$ fewer candidates. We further extract 40 interpretable rules from search trajectories using a post-hoc decision-tree framework and show that reusing them as soft constraints yields gains of up to 2$\times$ in valid model rates and 3$\times$ in neutrino model discovery across all three theory spaces. These results suggest that CDRL uncovers reusable structure in combinatorial search spaces and provides a general framework for scientific model discovery.
Tags
Links
- Source: https://arxiv.org/abs/2608.20686v1
- Canonical: https://arxiv.org/abs/2608.20686v1
Trouble viewing inline? Open PDF directly →
Full Text
93,325 characters extracted from source content.
Expand or collapse full text
CDRL: Certification-Driven Reinforcement Learning for Neutrino Flavor Model Discovery Piyush Jha Affiliation: School of Physics, Georgia Institute of Technology, USA Jake Rudolph Affiliation: University of California, Irvine, USA Victoria Knapp-Pérez Affiliation: University of California, Irvine, USA Affiliation: Halluminate, Department of Research, USA[2pt] piyush.jha@gatech.edu, jirudolp@uci.edu, vknapppe@uci.edu, mfieg@fnal.gov, aishikghosh@physics.gatech.edu, vganesh@gatech.edu Max Fieg Affiliation: Particle Theory Department, Fermilab, USA Aishik Ghosh Affiliation: School of Physics, Georgia Institute of Technology, USA Affiliation: Lawrence Berkeley National Laboratory, USA Vijay Ganesh [4pt] School of Computer Science Georgia Institute of Technology USA Abstract Many scientific discovery problems require searching combinatorial hypothesis spaces under complex domain constraints. Reinforcement learning (RL) offers a promising approach, but existing methods rely on scalar rewards that provide limited information about why candidate solutions fail, leading agents to repeatedly explore invalid regions. We introduce Certification-Driven Reinforcement Learning (CDRL), a framework that leverages structured feedback from symbolic reasoning tools. When a candidate violates domain constraints, these tools produce certificates identifying the actions responsible for failure. CDRL converts these certificates into reusable constraints that eliminate classes of invalid solutions and guide exploration toward valid regions. We evaluate CDRL on neutrino flavor model discovery in theoretical particle physics, where the hypothesis space exceeds 102610^26 possible models, and compare it with the state-of-the-art RL approach previously used for this task. Across three theory spaces, CDRL achieves up to 1.95× higher valid model rates and up to 6.33× higher neutrino model rates while evaluating up to 4× fewer candidates. We further extract 40 interpretable rules from search trajectories using a post-hoc decision-tree framework and show that reusing them as soft constraints yields gains of up to 2× in valid model rates and 3× in neutrino model discovery across all three theory spaces. These results suggest that CDRL uncovers reusable structure in combinatorial search spaces and provides a general framework for scientific model discovery. 1 Introduction Scientific discovery often requires exploring large spaces of candidate hypotheses. Researchers propose mathematical models, derive predictions, and compare them with experimental observations. This iterative process lies at the core of many scientific disciplines, including particle physics 12; 26; 7; 21, computational biology 42, chemistry 61, and materials science 10. In many such settings, the space of candidate models is combinatorial, and small changes in model structure can lead to dramatically different predictions. Systematically exploring these large theoretical spaces therefore becomes a major computational challenge, motivating the development of AI systems that assist scientific discovery and exploration 53; 1; 49. A common approach to exploring large hypothesis spaces is reinforcement learning (RL) 65, which formulates discovery as a sequential decision-making problem. In these frameworks, an agent incrementally constructs candidate models and receives rewards based on whether they satisfy domain-specific criteria. RL has been applied successfully to automated theorem proving 46, program synthesis 71, and scientific discovery 67; 50; 31. However, these methods typically rely on scalar reward signals that provide little information about why a candidate fails 39. Consequently, agents often waste substantial effort repeatedly exploring similar invalid regions of the combinatorial search space. Figure 1: The CDRL loop. CDRL builds each model one block at a time (A) using a policy-value network and search (B, D) 62; 63. Before the search commits to a block, a symbolic referee (C) rules out moves that are already known to violate a domain constraint, so search time is spent only on moves that remain possible. Once a model is complete, it is scored by the physics pipeline (E, F; Section 4.4 defines the score and what counts as a good model). When a model fails, the certificate analyzer (G) identifies which specific block assignments caused the failure and compiles that into a reusable rule stored in the constraint database (H), so the referee (C) blocks the same failure pattern, and every equivalent model that would have made it, everywhere it recurs in future search. Separately, and only after training, search knowledge discovery (I) mines the most common decisions the search made into simple reusable rules that also feed the referee (C). Section 4.3 gives the formal, SAT-based definition of the referee and constraint database, and Table 2 works out the ways a certificate can arise. Figure 7 (Appendix A) walks through this loop step by step on a worked example. In many scientific domains, structured feedback beyond scalar rewards is available, yet traditional RL algorithms do not fully exploit it. External reasoning tools such as theorem provers, constraint solvers, computer algebra systems, program analysis tools, and simulators can analyze candidate solutions and identify the causes of failure. Because these systems operate on formally defined objects, they can often produce certificates 11 1 A certificate is a structured explanation produced by a reasoning tool that identifies the subset of decisions responsible for satisfying or violating domain constraints. See Section 3 for a formal definition and discussion. that describe the outcome of their analysis and pinpoint the components responsible for violated constraints. Such certificates provide structured information that can be leveraged to guide exploration more effectively than scalar reward signals alone. Crucially, the two signals are complementary rather than competing (Figure 2). Further, scientists have traditionally been able to distill useful heuristic rules from the problem-solving process, and these insights can accelerate future exploration of the underlying mathematical space. An RL approach that enables the extraction of such heuristic rules from the agent’s decisions would therefore be valuable, both for interpretability and for improving computational efficiency in subsequent runs. There is a growing interest in using RL to construct theories in particle physics 68; 12; 6; 29. A viable theory, or model, is subject to a number of consistency checks such as requiring that Lorentz invariance and other internal symmetries are respected, as well as demands that the theory reproduce certain observed qualities like the mass of a certain particle. When an RL agent attempts to construct a model, it will generically fail these checks. However, if the RL agent had feedback in the form of a certificate concerning the failure of a candidate model, it could be trained to build viable models more quickly. To demonstrate the potential advantages of fully incorporating such feedback, we consider models that can be constructed for neutrino masses 12, which enables rapid exploration of mathematical models where physicists have limited intuition. In our setup, an agent selects the particle content of a model and the symmetries it must satisfy. These constraints are encoded via irreducible representations of a symmetry group, yielding a Lagrangian density that defines a quantum field theory. The resulting models are evaluated using existing symbolic and numerical software for Lagrangian construction, mass-matrix extraction, and parameter fitting, followed by statistical comparison to experimental data. Exhaustive search over more than 102610^26 possible models is infeasible, as evaluating a single candidate requires non-trivial symbolic and numerical computation. Figure 2: The two feedback signals CDRL gets from each physics evaluation are complementary rather than competing. Evaluating a candidate model yields a scalar reward, a soft constraint that scores the quality of the model, and a certificate, a hard constraint that names the exact components responsible for a failure and forbids them via a clause that Boolean Constraint Propagation (BCP) then enforces everywhere that pattern would recur. The reward shapes the network through learning, while the certificate prunes the search space; together they determine the new model the search proposes next, and the cycle repeats. Section 3 gives the formal definition of a certificate. Certification-Driven Reinforcement Learning (CDRL) is a framework that leverages structured feedback from external reasoning tools to improve exploration in constrained combinatorial search spaces. When a candidate violates a domain constraint, the reasoning tool returns a certificate identifying the subset of assignments responsible for the failure. CDRL analyzes this certificate and converts the responsible assignments into a symbolic conflict clause, which is added to the global SAT constraint database 15. During search, these learned constraints are enforced by a lightweight symbolic reasoning layer that immediately eliminates partial candidates violating known domain rules, allowing the RL agent to avoid exploring impossible regions of the search space. During the MCTS rollouts that follow 62; 63, this symbolic reasoning layer is implemented via Boolean Constraint Propagation (BCP) 20; 15, which enforces the accumulated clauses as the agent builds new candidates, blocking exploration of any partial assignment that repeats a previously seen conflicting decision pattern. This differs from a negative reward in kind, not degree. A negative reward is a scalar that adjusts the network’s weights by a small gradient step; it lowers the probability of a decision but never rules it out, so the agent can, and empirically does, revisit the same dead end many times, and the penalty says nothing about which of the decisions was to blame. A conflict clause instead operates on the search space itself: it is a hard logical constraint naming the exact assignments responsible, and once added, BCP makes every partial assignment containing that pattern unreachable for all agents sharing the clause database, with no dependence on how well the network has been trained. In effect, a scalar reward changes where the agent prefers to go, whereas a certificate changes where it can go. As more certificates accumulate, the feasible search space is progressively pruned, allowing the agent to avoid rediscovering equivalent failure modes and focus expensive physics evaluations on regions more likely to contain valid theories. As a concrete example of this structured feedback in our setting, consider a candidate neutrino model whose non-Abelian A4A_4 representation assignment is invalid for any choice of ℤNZ_N charge (Figure 1). Rather than emitting only a scalar penalty for this one candidate, our system extracts a certificate identifying the representation pattern responsible and compiles it into a logical constraint that blocks that pattern across the whole charge sector, so it is masked the moment it reappears elsewhere in the search tree, before any physics evaluation is run on it (worked out in detail in Section 4). Concretely, we realize this loop with well-established tools: candidate models are encoded as a Boolean satisfiability (SAT) formula in conjunctive normal form; certificates become conflict clauses that are enforced during search by Boolean Constraint Propagation (BCP) 20; 15, the same unit-propagation mechanism used inside modern SAT solvers 15; and the search itself is an AlphaZero-style Monte Carlo Tree Search (MCTS) 62; 63 guided by a policy-value network. These three components play distinct, complementary roles at every decision: neural guidance proposes the next assignment, symbolic reasoning prunes the assignments a certificate has ruled out, and MCTS balances exploration against exploitation over what remains. We quantify the payoff of this structured feedback empirically across three neutrino theory spaces (Section 5), and further show that the constraints and decision patterns CDRL accumulates expose reusable structure in the theory space (Section 5.4). Across three theory spaces for neutrino flavor model discovery, CDRL achieves up to 1.95×1.95× higher valid model rates and up to 6.33×6.33× higher neutrino model rates than AMBer 12, while evaluating up to 4×4× fewer candidates. These gains are expected to scale with the complexity of the problem and indicate substantially more efficient navigation of the underlying combinatorial hypothesis space, similar in spirit to recent advances in algorithm discovery and search-based scientific reasoning 25; 60; 49; 1. Beyond improved search efficiency, CDRL enables search knowledge discovery from search trajectories. Using a post-hoc decision-tree analysis of high-confidence MCTS states, we extract 40 interpretable rules that capture recurring dependencies between particle assignments. Reusing these rules as soft constraints further improves performance, suggesting that they capture meaningful and reusable structure within the theory space. Our contributions are therefore: (i) CDRL, a certificate-driven RL framework that transforms symbolic failure certificates into reusable search constraints, progressively eliminating large invalid regions; (i) state-of-the-art results on neutrino flavor model discovery, achieving substantially higher discovery rates with fewer evaluations than prior RL approaches; and (i) a framework for extracting and reusing interpretable rules from search trajectories, demonstrating that knowledge acquired during exploration can improve future search. Table 1: Example neutrino flavor model discovered by CDRL in the T19×ℤ4T_19×Z_4 theory space. The table shows particle representation and charge assignments for one of the viable neutrino models discovered by CDRL. This model achieves a strong χ2χ^2 fit with a minimal number of free parameters, illustrating the ability of CDRL to discover compact and high-quality theories. Additional discovered neutrino models across all three theory spaces are provided in Section C. L E1E_1 E2E_2 E3E_3 N HuH_u HdH_d ϕ1 _1 ϕ2 _2 ϕ3 _3 ϕ4 _4 ϕ5 _5 ϕ6 _6 T19T_19 13_1 ′1 1 ′1 ¯2 3_2 ′1 1 13_1 ¯1 3_1 13_1 ¯1 3_1 23_2 23_2 ℤ4Z_4 44 22 22 22 44 22 44 22 22 33 44 44 11 2 Background and Related Work Neutrino Flavor Model Construction. The Standard Model (SM) of particle physics describes the fundamental particles and their interactions and has exquisite agreement with experiment, with some exceptions. Perhaps the most notable exception is the prediction of massless neutrinos, but experiments 27; 4; 18; 5 have determined that they have a mass, which necessitates the presence of new particles beyond the SM. Because these new particles must couple to neutrinos, and because neutrinos and charged leptons are components of the same electroweak doublets, one generally expects them to couple to charged leptons as well. For this reason, solutions to the massive neutrino problem are typically connected to the question of flavor in the SM 9; 26; 8; 45: what is the explanation for the three flavors of fermions and what is the origin for the observed levels of mixing between them? One general framework to address these shortcomings is to add right-handed neutrinos to generate small neutrino masses via the seesaw mechanism 55; 70; 30; 28, as well as a number of scalar particles, ‘flavons’, whose interactions give structure to the level of lepton mixing after they acquire a certain vacuum expectation value (VEV). Adding these new particles generally results in an even larger number of free parameters than was already present in the SM, which limits the predictivity of the model. However, the parameters in the flavor sector can be strongly constrained if the model is subject to a global flavor symmetry, which gives structure to the observed mixing; in the ideal case it explains the observed values with minimal free parameters. A given theory under this framework is thus described by: the set of particles, the irreducible representations they take under the flavor symmetry, the VEV of the flavons22 2 In a complete model, the VEV is a dynamical result of the theory, and achieving a certain VEV pattern is a problem in its own right. Here, as in Ref 12, we do not attempt to solve this problem, but assume that a certain set of VEVs can be achieved, and the remaining free parameters. The number of models that exist for a given choice of flavor symmetry grows rapidly with the number of particles, and identifying solutions that fit to experiment is highly nontrivial. Recent work 33; 34; 56; 57; 16 has demonstrated RL as a tool for searching analogous spaces of models for various areas in particle physics. In particular, the AMBer framework 12 integrates domain specific physics tools which allows the agent to evaluate candidate models using software used by physicists for conventional model-building. CDRL goes further: rather than using these tools only to evaluate candidates one at a time, it extracts structured certificates from them and converts these into reusable constraints that prune invalid regions of the search space, letting the system progressively accumulate knowledge about the structure of valid theories. This approach can be extended to several other applications of agent-guided workflows to scientific discovery. AI for scientific discovery. Artificial intelligence is increasingly used across the scientific discovery pipeline, including hypothesis generation, experimental design, and large-scale data analysis 67; 69. Recent advances highlight the ability of AI systems to explore large scientific search spaces, such as materials discovery using graph neural networks and generative models 53; 48, and biomolecular structure prediction using deep learning systems like AlphaFold 1. Machine learning is also widely used in particle physics for analyzing experimental data and identifying potential new phenomena 44. Alongside these developments, there is growing interest in incorporating domain knowledge and reasoning into AI-driven discovery processes 54; 66. In this work, we take a step in this direction by introducing CDRL, which integrates symbolic reasoning tools into the learning loop to provide structured and interpretable feedback during exploration. Reinforcement learning for algorithm and scientific discovery. Reinforcement learning (RL) has discovered algorithms and optimized complex scientific systems, including AlphaTensor for tensor decomposition 25, AlphaTensor-Quantum for fault-tolerant quantum circuits 60, and AlphaDev for faster sorting 49. It has also controlled physical systems and experiments such as tokamak plasmas 22, stratospheric balloons 14, and quantum experiment design 51. These results show RL can navigate large combinatorial search spaces, but they depend on reward signals from a simulator or environment. CDRL instead adds symbolic reasoning tools that emit structured certificates, giving the agent richer feedback to guide exploration. Neuro-symbolic AI. Neuro-symbolic AI combines neural learning with symbolic reasoning to strengthen reasoning, interpretability, and reliability 35; 2. Integration strategies range from embedding symbolic rules within neural architectures and differentiable reasoning modules to modular systems that call external reasoning tools 19. CDRL takes the modular route: a learning agent queries external symbolic systems that analyze candidate solutions and return structured feedback. In the taxonomy of 19, CDRL sits at the center of the neuro-symbolic design space, uniting learning, symbolic reasoning, and structured knowledge within a single decision loop. Oracle-augmented learning. Recent work has explored integrating external reasoning tools into AI systems. Large language models have been combined with symbolic tools during inference 43; 3; 17; 38, while other approaches incorporate external feedback during RL 32; 39. Related ideas also appear in automated reasoning and synthesis. Modern SAT solvers use conflict feedback to guide search 47, and frameworks such as CEGIS and Satisfiability Modulo Oracles refine candidates using counterexamples or constraints from external verifiers 40; 58; 41. CDRL builds on these directions by converting certificates from reasoning systems into reusable constraints, enabling RL agents to progressively prune invalid regions of large scientific search spaces. Together, these observations motivate Certification-Driven Reinforcement Learning (CDRL), a paradigm in which symbolic reasoning systems act as structured feedback generators that guide RL over large scientific search spaces. 3 Certification-Driven Reinforcement Learning (CDRL) Algorithm 1 Certification-Driven Reinforcement Learning (CDRL) 1: Notation: πθ _θ policy-value network; V verifier (the physics evaluation pipeline); A certificate analyzer; 0,K_0,K initial and accumulated constraint sets; H space of candidate hypotheses (models); h∈Hh∈ H one candidate; ℋvalidH_valid set of discovered valid hypotheses; σ a certificate returned by V on failure; c the constraint derived from σ. 2: 3: Policy πθ _θ, verifier V, certificate analyzer A, initial constraints 0K_0 4: Set of valid theories ℋvalidH_valid 5: ←0K _0 ⊳ initialize with known domain constraints 6: ℋvalid←∅H_valid← ⊳ store discovered valid solutions 7: for each training episode do 8: h∼Plan(πθ,)h Plan( _θ,K) ⊳ construct candidate while respecting accumulated constraints 9: (status,σ)←V(h)(status,σ)← V(h) ⊳ evaluate candidate and optionally return failure certificate σ 10: if status=validstatus=valid then 11: ℋvalid←ℋvalid∪hH_valid _valid∪\h\ ⊳ record valid hypothesis 12: Store trajectory and reward in replay buffer 13: else 14: c←(σ)c (σ) ⊳ convert certificate into reusable constraint 15: ←∪cK ∪\c\ ⊳ prune entire class of invalid solutions 16: Store trajectory and penalty in replay buffer 17: end if 18: Periodically update πθ _θ from replay-buffer mini-batches 19: end for Many scientific discovery tasks can be viewed as structured search problems over a large space of candidate hypotheses. An agent incrementally constructs candidate solutions while interacting with an environment that verifies whether the candidate satisfies domain constraints. Certificate-Driven Reinforcement Learning (CDRL) augments this RL loop with certificate-based constraint learning. Each time the verifier rejects a candidate, the certificate it returns is also converted into a reusable constraint that rules out the whole class of similarly invalid candidates, not just the one just tried. Formally, let H denote the space of candidate hypotheses and let 0K_0 denote a set of initial domain constraints known a priori. The agent maintains a growing set of constraints K initialized with 0K_0. During training, the agent proposes candidate hypotheses using a planning procedure Plan(πθ,) Plan( _θ,K) (such as MCTS), which incrementally constructs candidates while enforcing constraints K and using πθ _θ to guide exploration. Each candidate is verified by an external reasoning tool. If the candidate satisfies all constraints, the agent receives a positive reward. Otherwise, the verifier produces a certificate describing the failure. This certificate is analyzed to derive a new constraint, which is added to K and used to prune the search space. The overall CDRL procedure is shown in Algorithm 1. As training progresses, the learned constraints accumulate and progressively restrict exploration to regions of the hypothesis space that remain consistent with previously discovered knowledge. This allows the RL agent to avoid rediscovering similar failure modes and focus exploration on configurations that are more likely to yield valid solutions. Certificates and Constraint Learning. A certificate is a structured explanation produced by a reasoning tool when a candidate hypothesis violates domain constraints. It identifies the subset of decisions responsible for the failure. Let h∈Hh∈ H denote a candidate hypothesis. When h is invalid or redundant with an already-covered equivalent hypothesis, the verifier returns a certificate σ, which is analyzed to derive a constraint c that prevents similar configurations. This constraint is added to K and enforced during future exploration, progressively pruning the search space. This mechanism is conceptually related to conflict-driven learning in SAT solvers, where conflicts yield clauses that eliminate inconsistent assignments. In CDRL, certificates play an analogous role by enabling reusable constraint learning. 4 Application: Neutrino Flavor Model Discovery We evaluate CDRL on the discovery of viable neutrino flavor models, a central problem in particle physics. The task involves constructing models that explain neutrino masses and mixing while satisfying domain constraints. We follow a common flavor symmetry model building framework, where candidate models are defined by non-Abelian symmetry choices, particle irreducible representation assignments, Abelian charges, and vacuum expectation values. This results in a large combinatorial search space, making efficient exploration critical. Figure 1 shows how the components below fit together; further background is provided in Section 2. 4.1 Matrix Representation of Candidate Models Following the AMBer framework 12, we encode a candidate theory as a matrix representation that captures the assignment of particles to symmetry representations and charges. Rows correspond to particles in the model, while columns correspond to irreducible representation and charge assignments under the symmetry groups. For example, rows include the three charged lepton doublets (L1,L2,L3)(L_1,L_2,L_3), charged lepton singlets (E1,E2,E3)(E_1,E_2,E_3), right-handed neutrinos (N1,N2,N3)(N_1,N_2,N_3), Higgs fields (Hu,Hd)(H_u,H_d), and several flavon fields. Columns represent discrete non-Abelian representations (e.g., A4A_4 irreducible representations), Abelian ℤNZ_N charges, and VEV configurations for flavon fields. Columns are encoded using one-hot vectors. Unassigned entries are represented by −1-1, allowing the state to represent partially constructed models. This matrix therefore forms the state representation for the learning agent. 4.2 Sequential Construction of Models Model construction is formulated as a sequential decision process. Instead of assigning every matrix entry independently, decisions are organized into blocks corresponding to logical modeling choices. The agent starts by assigning the active ℤNZ_N symmetry as one block, then for each particle in turn assigns its representation and then its Abelian charge as two separate blocks, and finally assigns each flavon’s VEV configuration as its own block. At each step, the next unassigned block is selected, and the agent chooses from a small alphabet consisting of either an all-zero vector (inactive block) or a one-hot vector indicating the assignment. This structured action space reduces the branching factor and enables incremental construction of candidate theories until completion. 4.3 SAT-Based Constraint Layer Rather than allowing the RL agent to freely construct candidate models, discovering only at the end that they violate domain rules, we incorporate a symbolic constraint layer that continuously enforces known scientific constraints during search. This layer immediately rejects partial assignments that cannot be extended into a valid theory, allowing the agent to focus its exploration on feasible regions of the combinatorial search space. We encode the domain knowledge as a set of Boolean constraints, including exactly one representation per particle, a single active ℤNZ_N symmetry (a modeling choice that reduces the search space), exactly one charge per particle for that active ℤNZ_N symmetry, structural constraints for triplet representations, and exactly one vacuum expectation value (VEV) assignment per flavon. These constraints are compiled once into conjunctive normal form (CNF). During the MCTS search, we use Boolean Constraint Propagation (BCP) 20; 15 at every node to maintain consistency between the current partial assignment and the encoded constraints. Whenever the agent makes a new assignment, BCP efficiently detects whether the partial model already violates a constraint and automatically infers any assignments that are logically forced. As a result, invalid branches are pruned immediately, while the state presented to the neural network always satisfies all currently known hard constraints. We therefore use BCP as a lightweight symbolic reasoning layer that filters illegal actions without requiring a full SAT solve after every decision. 4.4 RL environment and reward We use the same particle physics evaluation pipeline as AMBer 12 for direct comparison. A terminal state corresponds to a fully specified model matrix, which is passed to the physics tools. Using Model2Mass, the particle assignment matrix is compiled into a Lagrangian and the resulting Dirac and Majorana mass matrices are constructed, from which the light-neutrino mass matrix is obtained through the seesaw mechanism. Using flavorpy, the model’s free parameters are then fit to neutrino observables from NuFit 5.3 24 and scored by a chi-squared goodness of fit χ2χ^2. A model is invalid if it fails a structural check (a rank-deficient mass matrix, so no physical spectrum exists) or is inelegant (more than 5050 free parameters); such models receive a strong penalty. Valid models are scored by a reward that combines (i) the chi-squared fit quality and (i) the number of free parameters npn_p, normalized and clipped to a bounded range so that better fits with fewer parameters score higher (an equal weighting of the two terms by default). We designate a valid model a neutrino model when it additionally satisfies χ2≤10χ^2≤ 10 and np≤7n_p≤ 7. Because each evaluation requires expensive numerical optimization and dominates runtime (approx. 98%; Section 5), avoiding invalid and redundant regions of the search space before evaluation is critical. Full experimental and compute details are given in Appendix B. 4.5 Certificate Extraction and Conflict Clauses Beyond scalar rewards, CDRL extracts structured certificates from invalid candidate models and converts them into reusable conflict clauses added to the global constraint set K. We implement this with a dedicated certificate-analysis routine that runs on every terminal model. It inspects the completed model matrix, tests it against the criteria below, and, when a criterion fires, identifies the exact subset of assignments responsible and emits their negation as a clause. Because a clause names the responsible assignments rather than the single candidate, one certificate prunes an entire class of models and lets the agent avoid revisiting similar configurations. We consider two main classes: (i) insufficient-rank representation certificates, which arise when a candidate’s non-Abelian representations and VEV choice yield a rank-deficient mass matrix for every choice of Abelian charge, and eliminate that specific representation-and-VEV combination independent of the charges; and (i) ℤNZ_N symmetry certificates, which depend only on the Abelian charges and capture two group-theoretic equivalences: charge assignments reducible to a smaller symmetry group by a shared divisor d (checked in both directions between the smaller and larger group), and charge assignments related by negation q↦−qmodNq -q N, an automorphism of order 2, both of which preserve the theory’s selection rule. Table 2 demonstrates how each type of certificate works on a common ℤ6Z_6 candidate. Together, these certificates encode reusable symbolic knowledge that progressively removes invalid and redundant regions from the search space. Table 2: The three certificate types, each worked through on a common ℤ6Z_6 candidate; the full derivation follows below. Certificates 2 and 3 depend only on the ℤNZ_N charges, independent of representations or VEVs. Every clause is ¬(the equivalent or excluded pattern) (the equivalent or excluded pattern); once added to the shared constraint database, it is enforced across all parallel searches with no physics evaluation spent on models it already rules out. Description Example Clause Insufficient-rank representation Model already rank-deficient without ℤNZ_N symmetry Reps and VEVs with ℤ6Z_6 charges wildcarded already rank-deficient ¬ (reps & VEV, any charges) Abelian symmetry reducibility ℤN[qi]≅ℤN/d[qi/d]Z_N[q_i] _N/d[q_i/d] ℤ6[2,4,6]↦ℤ3[1,2,3]Z_6\,[2,4,6] _3\,[1,2,3] ¬ (other representative) Charge negation ℤN[qi]≅ℤN[−qi mod N]Z_N[q_i] _N[-q_i mod N] ℤ6[2,4,6]↦ℤ6[4,2,6]Z_6\,[2,4,6] _6\,[4,2,6] ¬ (negated charges) We now give the full construction of each certificate type. The first class arises when a candidate model’s non-Abelian representations and VEV choice cannot support a full-rank mass matrix under any Abelian charge assignment. After constructing a candidate matrix, the system evaluates the model using the physics validity checker. If the model fails, the algorithm performs a reduced analysis in which the Abelian charge sector is temporarily wildcarded and only the non-Abelian representation and VEV assignments are retained. This has the effect of removing the Abelian symmetry entirely. When the representation-and-VEV-only model is already rank-deficient, no Abelian charge assignment layered on top of it can restore full rank, so the failure must be attributed solely to the non-Abelian representations and VEV choice. The system extracts the corresponding representation and VEV assignments and generates a conflict clause blocking this combination; other VEV choices for the same representations remain unaffected and available for exploration. This allows the solver to prune large classes of models that share the same insufficient-rank structure. The second class arises from symmetry relations in the Abelian ℤNZ_N charge sector, independent of the non-Abelian representations or VEV choice, and captures two group-theoretic equivalences between charge assignments that describe the same physics. The first is reducibility. If all charges in a ℤNZ_N model share a common divisor d, then the model is reducible to a ℤN/dZ_N/d model. Formally, if qi=dai,N=dM,q_i=da_i, N=dM, then the selection rule q1+q2+q3=0(modN)q_1+q_2+q_3=0 N is equivalent to a1+a2+a3=0(modM).a_1+a_2+a_3=0 M. This implies that the larger symmetry provides no additional structure beyond the reduced group ℤMZ_M. Whichever model is evaluated first, the certificate blocks the other, and the relation is checked in both directions (a smaller model also blocks the larger models it embeds into). The system generates a conflict clause by reconstructing the equivalent model in matrix form and negating the literals corresponding to that assignment. The second equivalence is relation by an automorphism, specifically the order-2 automorphism of negation. Replacing every charge with its additive inverse, q↦−qmodNq -q N, preserves the selection rule ∑iqi≡0(modN) _iq_i≡ 0 N (negating every term preserves a sum of zero), so the negated charge assignment describes the same physics and need not be explored separately. Higher order automorphisms could also be included in future applications. 4.6 Learned Clause Injection The conflict clauses generated during evaluation are accumulated globally and injected into the SAT solver before each new search episode, requiring no recompilation since each clause is already in CNF. Detection then falls out of BCP itself: at every MCTS node the current partial assignment is fed to the solver, and to score a candidate block assignment we tentatively add its literals and propagate. If propagation drives any learned clause to a conflict, that block assignment is removed from the legal-action mask before the policy network ever ranks it (Section 4.3). Instead, a forced literal implied by the clauses is propagated into the state. Figure 1 traces this loop end to end: a conflict at a completed model is analyzed into a clause, appended to the shared database, and the clause then masks the same failing pattern the moment it recurs elsewhere in the tree, before any physics evaluation is spent on it. This is precisely where the neuro-symbolic design pays off over a purely neural agent: the learned clause makes the whole equivalence class logically unreachable for every worker (Figure 2), so large regions of the search space are pruned permanently rather than merely down-weighted. 4.7 MCTS, Neural Guidance, and Portfolio Parallelization We search the space of partial model matrices using MCTS 62; 63. Each node corresponds to a partially constructed candidate. At each step, a policy-value network proposes the next assignment and estimates the state’s value. The policy is masked by BCP’s legal-action vector (Section 4.3), ensuring only constraint-consistent actions are explored, and the masked priors guide tree traversal via PUCT 59. At terminal states, the physics evaluation pipeline computes a reward that is backpropagated through the tree and used to retrain the network via self-play. This tightly couples all three components at every decision: neural guidance proposes, symbolic reasoning prunes, and MCTS balances exploration against exploitation. Removing any one causes substantial degradation and neutrino discovery collapses to near zero without either the network or MCTS (Table 5). To scale search, we employ portfolio-style parallelization inspired by parallel SAT solvers 11; 52 and distributed RL 36. Multiple workers independently perform MCTS self-play while sharing (i) a replay buffer for network retraining and (i) a global conflict clause database. Any certificate discovered by one worker is immediately enforced via BCP in all others, a direct analogue of clause sharing in portfolio SAT solving. Terminal evaluations are also cached globally to avoid redundant physics computation. Removing this sharing increases variance and reduces neutrino discovery by up to 2×2× (Table 5). Additional details are in Appendices B.5 and B.6. Table 3: Comparison with Baselines across Theory Spaces. Valid (%) denotes structurally valid models, Neutrino (%) denotes discovered neutrino flavor models, and Min Params denotes the minimum number of free parameters found (lower is better). DNN: deep neural network (the policy-value network, Section 4.3); PPO: Proximal Policy Optimization, the RL algorithm AMBer uses in place of CDRL’s MCTS. Parenthetical multipliers under CDRL’s Valid (%) and Neutrino (%) entries show improvement relative to AMBer, the prior state of the art; all other baselines (Random, ChatGPT, and the DNN/MCTS/symbolic ablations below AMBer) are shown for context and are not the basis for these multipliers. Each ablated or hybrid baseline (MCTS only, DNN only, Symbolic only, AlphaZero) is CDRL itself with the corresponding component removed, evaluated on the same physics pipeline described in Appendix B.3; this isolates that component’s contribution rather than testing an independent reimplementation. Method Category A4×ℤ4A_4×Z_4 A4×ℤNA_4×Z_N T19×ℤ4T_19×Z_4 Valid (%) Neutrino (%) Min Params Valid (%) Neutrino (%) Min Params Valid (%) Neutrino (%) Min Params Uninformed and LLM baselines Random Random search 0.1 0.00 12 0.1 0.00 14 0.1 0.00 16 ChatGPT (GPT-5.3) 64 Few-shot prompting 0.2 0.00 13 0.2 0.00 18 0.1 0.00 15 Search and learning hybrids AlphaZero 62 DNN + MCTS 14.9 0.01 7 16.2 0.03 7 5.4 0.04 5 MCTS only Tree search only 10.2 0.00 9 9.8 0.00 10 1.1 0.00 7 DNN only Policy/value network 5.1 0.00 13 4.5 0.00 9 2.2 0.01 7 Symbolic only 47 CDCL SAT solver 0.2 0.00 12 0.2 0.00 12 0.1 0.00 10 State-of-the-art AMBer 12 DNN + PPO 19.53 0.02 5 13.79 0.03 5 11.02 0.03 4 CDRL (Ours) DNN + MCTS + certificates 28.1 ± 3.3 (1.44×) 0.10 ± 0.01 (5.00×) 5 26.9 ± 3.7 (1.95×) 0.19 ± 0.05 (6.33×) 5 18.2 ± 2.1 (1.65×) 0.09 ± 0.02 (3.00×) 4 4.8 Benchmark Theory Spaces We evaluate CDRL on neutrino flavor model discovery using the same theory spaces as AMBer 12 to ensure direct comparability. The search space consists of discrete flavor symmetry models defined by non-Abelian representations, Abelian ℤNZ_N charge assignments, and flavon VEV configurations. We consider three theory spaces used in prior work, defined by their symmetry structure and the number of flavons nϕn_φ: (i) A4×ℤ4A_4×Z_4 with nϕ≤5n_φ≤ 5 flavons, (i) A4×ℤNA_4×Z_N where N∈[2,10]N∈[2,10] and nϕ≤5n_φ≤ 5, and (i) T19×ℤ4T_19×Z_4 with nϕ≤6n_φ≤ 6. These spaces increase in symmetry richness and combinatorial complexity, providing progressively harder benchmarks. 5 Experimental Results 5.1 Evaluation Metrics We adopt the same evaluation protocol as AMBer to ensure consistency. Each candidate model is evaluated using the physics pipeline, which produces a χ2χ^2 fit to experimental observables and the number of free parameters npn_p. A model is considered valid if it satisfies structural constraints, and is considered a neutrino model if it achieves both a good fit and low complexity, defined as χ2≤10χ^2≤ 10 and np≤7n_p≤ 7. We report the percentage of valid physics models (Valid %), the percentage of viable neutrino models (Neutrino %), and the minimum number of parameters discovered. 5.2 Main Results CDRL achieves the highest Valid (%) and Neutrino (%) of any method in every theory space, matching on AMBer’s Min Params. As shown in Table 3, on A4×ℤNA_4×Z_N, CDRL achieves 26.9%26.9\% valid models compared to 13.79%13.79\% for AMBer (a 1.95×1.95× improvement), and 0.19%0.19\% neutrino models compared to 0.03%0.03\% (a 6.33×6.33× improvement). Similar gains are observed in other theory spaces, including up to 1.65×1.65× improvements in valid model rates and up to 3×3× improvements in neutrino discovery. These gains are achieved with substantially higher sample efficiency. As shown in Table 4, CDRL discovers more neutrino models while evaluating up to 4×4× fewer candidates. In combinatorial spaces exceeding 102610^26 possible models, these reductions correspond to substantially more efficient exploration. The mechanism behind these gains is concrete: Figure 1 traces how a single certificate blocks an entire class of candidates before any physics is run, and Figure 5 shows an example rule recovered from the search itself (full analysis in Section 5.4). Table 4: Search Efficiency Comparison. CDRL discovers more neutrino models while evaluating significantly fewer candidates (up to 4×4× fewer) across all theory spaces, demonstrating substantially improved sample efficiency over AMBer and random search. Space Method Models evaluated Neutrino models found A4×ℤ4A_4×Z_4 Random 4,000,000 28 AMBer 4,000,000 683 CDRL 1,000,000 1090 A4×ℤNA_4×Z_N Random 4,000,000 21 AMBer 4,000,000 1394 CDRL 1,000,000 2343 T19×ℤ4T_19×Z_4 Random 24,000,000 409 AMBer 24,000,000 6439 CDRL 6,000,000 7019 Importance of certificate-driven pruning. The additional baselines (implementation details in Appendix B.3) are CDRL itself with one component removed, and highlight the importance of combining learning, planning, and symbolic reasoning. Few-shot prompting with GPT-5.3 performs near-random search, indicating that current large language models offer little advantage in these underexplored theory spaces: the relevant structure is largely absent from pretraining data, so the model cannot substitute for guided search with symbolic feedback. Pure symbolic search, DNN-only policies, MCTS-only search, and AlphaZero-style baselines all substantially underperform CDRL. On A4×ℤNA_4×Z_N the AlphaZero-style baseline (MCTS and the policy-value network, without certificates) already exceeds AMBer’s valid model rate (16.2%16.2\% vs. 13.79%13.79\%), so planning and neural guidance alone recover part of AMBer’s gap to CDRL. Certificate-driven pruning (Table 5) accounts for the remainder and for most of the gain in neutrino discovery. Future work may study the additional performance metrics for such rule-guided search, beyond raw number of neutrino models found. Qualitative trends. Aggregate rates measure how often a search succeeds, but for model building the diversity of what is found matters just as much: physicists want a broad set of distinct candidate theories to study, not many copies of the same one, and coverage across different symmetry groups indicates that the search is not confined to a narrow corner of the space. We therefore also examine the distribution of discovered models, not only their counts. Figure 3 shows the clearest evidence of this: CDRL discovers viable models spread across a substantially broader range of ℤNZ_N symmetry groups than AMBer, which concentrates around a few specific values of N. This indicates that CDRL explores different regions of the theory space rather than only different instances within the same region. Models are binned by the ℤNZ_N they were constructed under rather than any reduced or canonical form, so this spread is not an artifact of the same underlying model being counted under multiple symmetry groups; the reducibility certificate (Table 2) instead prevents a redundant representative from being explored and counted a second time under a different N. Figure 4 shows where CDRL’s models concentrate in (χ2,np)(χ^2,n_p) space in the right column compared to AMBer in the left column. We also present a strong example model discovered by CDRL in the T19×ℤ4T_19×Z_4 space (Table 1). The neutrino models discovered by CDRL do not exactly match any of those found by AMBer. Combined with the broader ℤNZ_N coverage in Figure 3, this is consistent with CDRL exploring complementary regions of the theory space rather than merely finding different individual models within the same region AMBer already covers. Following the analysis protocol of AMBer 12, we can look more closely at why these distributions differ. For the distribution of models shown in Figure 4, CDRL reaches neutrino models with the smallest parameter counts observed for either method (Table 3 reports this as Min Params) while maintaining competitive or lower χ2χ^2 values. For the ℤNZ_N distribution of Figure 3, AMBer concentrates its discoveries around specific symmetry groups (e.g., N=5N=5), whereas CDRL spreads more uniformly across the available ℤNZ_N choices. This trend is consistent with progressively stronger symbolic pruning during search. As the learned clause database grows, the legal-action mask becomes increasingly selective, allowing Boolean constraint propagation to eliminate larger regions of invalid or redundant search trajectories before expensive physics evaluation is performed. This mechanism both concentrates evaluation on predictive low-parameter models and, because whole redundant equivalence classes are removed rather than merely down-weighted, pushes the search into ℤNZ_N regions AMBer rarely reaches. CDRL’s reward contains no term that rewards higher-order ℤNZ_N symmetries (Section 4.4 gives the full reward, which depends only on χ2χ^2 fit quality and the number of free parameters); AMBer’s scalar reward includes such a term to steer search toward the more complex, higher-order groups 12. CDRL reaches broader coverage without an equivalent incentive. Certificates prune redundant equivalence classes uniformly across the theory space, so exploration spreads more evenly as a byproduct of pruning rather than of reward shaping. This difference in reward design does not affect the evaluation protocol itself (Section 5), which scores both methods identically. Figure 3: Distribution of successfully discovered neutrino models across ℤNZ_N symmetry groups for AMBer and CDRL. CDRL discovers viable models more uniformly across different symmetry choices, while AMBer concentrates more heavily around specific values of N. Figure 4: Distribution of discovered models over χ2χ^2 (fit quality) and npn_p (number of parameters). Each bin shows model density, with the bottom-left region corresponding to well-fitting, low-complexity models. CDRL places more mass in the low-npn_p areas. Within that region, χ2χ^2 differences at very low values do not indicate meaningfully different fit quality, so Table 3 and Table 5 remain the primary quantitative comparison, with this figure illustrating where in (χ2,np)(χ^2,n_p) space that advantage is concentrated. Although CDRL introduces slight additional overhead from MCTS, certificate analysis, and symbolic propagation, the dominant computational cost (approx. 98%) arises from the physics evaluation pipeline, which is the same as AMBer. Since experiments use different parallelization settings and compute configurations (CDRL uses 32 CPU cores, while AMBer uses 250 parallel environments), we report candidate evaluations as the primary normalized measure of search efficiency. 5.3 Ablation Study An ablation study measures each component’s importance by removing it from the full system and observing the resulting drop in performance, so a larger drop indicates a more important component. Table 5 isolates the contribution of each component this way. Error bars are the standard deviation across 4 runs with different random seeds. Every ablation degrades performance, confirming that the gains come from integrating learning, planning, and symbolic reasoning rather than from any single part. Removing either the neural network or MCTS collapses neutrino discovery to near zero, showing that guided exploration is necessary at all in a space this large. Removing symbolic certificates instead leaves a functioning search, with valid model rates falling from 26.9%26.9\% to 16.2%16.2\% and neutrino discovery from 0.19%0.19\% to 0.03%0.03\% on A4×ℤNA_4×Z_N, so certificates contribute a substantial improvement on top of the neural and planning components. Removing portfolio sharing lowers performance and raises variance, indicating that shared constraints and experience are critical for scaling. In short, each component contributes measurably, and the full system is required for strong performance. Table 5: Ablation Study of CDRL Components. Valid (%) denotes the percentage of structurally valid models, Neutrino (%) denotes the percentage of discovered neutrino flavor models, and Min Params denotes the minimum number of free parameters found. Method / Ablation Description A4×ℤ4A_4×Z_4 A4×ℤNA_4×Z_N T19×ℤ4T_19×Z_4 Valid (%) Neutrino (%) Min Params Valid (%) Neutrino (%) Min Params Valid (%) Neutrino (%) Min Params CDRL (Full) DNN + MCTS + symbolic certificates + portfolio 28.1 ± 3.3 0.10 ± 0.01 5 26.9 ± 3.7 0.19 ± 0.05 5 18.2 ± 2.1 0.09 ± 0.02 4 No DNN No policy/value network 10.2 ± 5.1 0.00 ± 0.00 9 9.8 ± 4.6 0.00 ± 0.00 10 1.1 ± 1.0 0.00 ± 0.00 7 No MCTS No planning 5.1 ± 8.4 0.00 ± 0.00 13 4.5 ± 9.0 0.00 ± 0.00 9 2.2 ± 3.6 0.01 ± 0.00 7 No symbolic No certificate 14.9 ± 3.1 0.01 ± 0.02 7 16.2 ± 2.1 0.03 ± 0.01 7 5.4 ± 4.9 0.04 ± 0.02 5 No portfolio No clause/replay shared 26.9 ± 6.5 0.04 ± 0.02 6 25.1 ± 7.2 0.10 ± 0.09 5 12.1 ± 7.8 0.06 ± 0.04 5 5.4 Search Knowledge Discovery E2.Z4 E1.Z4 = 3?3E1.Z4 = 1?12YesNoYesNo Hu.A4 E3.rep = 1”?1’E3.rep = 1?1’1”YesNoYesNo Figure 5: Example decision trees. Left: Determination of the E2E_2’s ℤ4Z_4 charge in A4×ℤ4A_4×Z_4. Among high-confidence states, this decision tree predicts the E2E_2’s ℤ4Z_4 charge from E1E_1’s ℤ4Z_4 charge. This demonstrates how CDRL has learned to match the ℤ4Z_4 charges of the charged lepton singlets, a reasonable result in order to construct physically realizable mass matrices. This observation also shows how some rules exclude possible choices (in this case the ℤ4Z_4 charge value of 4). Right: Determination of the HuH_u’s A4A_4 representation in A4×ℤNA_4×Z_N. This decision tree is harder to interpret physically. The up-flavor Higgs is not directly correlated with the charged lepton sector, so there is either some non-trivial relationship, or this is a spurious correlation within the CDRL search. The full set of such observations for all three theory spaces is in Appendix C. A by-product of the search is a record of the decisions CDRL makes on its way to good models. We examine this record post-hoc to recover common decision patterns from the MCTS trajectories and cast them into human-readable decision trees. These decision patterns both illuminate how the agent is exploring, and with sufficient interpretation by a human physicist can provide insight on common modes of viable models in the theory space. Our approach is related to prior work on extracting interpretable policies from RL systems 13. However, in addition to using extracted rules purely for explanation or verification, we inject these rules as soft symbolic constraints in fresh, smaller-scale, “rule-guided” CDRL runs to test their utility in deepening exploration of fruitful regions of the theory space. Effectively, these soft constraints encourage the agent towards known viable regions of the theory space while still permitting exploration of the entire space. As shown in Figure 6, incorporating these rules consistently increases the number of discovered models in all three theory spaces. In A4×ℤ4A_4×Z_4 and T19×ℤ4T_19×Z_4, rule-guided runs achieve ∼2× \!2× higher valid model rates and 22–3×3× higher neutrino model discovery, while in A4×ℤNA_4×Z_N we observe ∼1.5× \!1.5× improvements in validity and up to 3×3× in neutrino discovery. We describe the procedure used to extract soft constraints from MCTS trajectories in Algorithm 2 and incorporate them into the search process. We retain high-confidence decision points from MCTS trajectories, i.e. states where the dominant action receives more than 95%95\% of visits and has a positive value estimate, and group these states by construction progress, defined as the number of assigned entries in the state before the first unassigned position. For each progress bucket with enough samples, we train one shallow decision tree that predicts the dominant action from the partial model’s earlier assignments; hyperparameters are given in Appendix B. Because blocks are assigned in a fixed top-down order (Section 4), only blocks assigned earlier in that order are available as features. We extract these high-confidence root-to-leaf paths as rules of the form conditions→aconditions→ a, where the conditions are conjunctions over binary state features, and retain only rules expressible as binary conditions for compatibility with the symbolic representation. These rules can then be injected into a new CDRL run as soft constraints. At inference time, we identify all rules whose conditions are satisfied by the current state, let each activated rule vote for its preferred action to form a bias vector r(s)r(s), and reweight the neural policy as P~(a∣s)∝P(a∣s)(1+βra(s)) P(a s) P(a s)\,(1+β\,r_a(s)), where β=0.5β=0.5 in all experiments. The reweighted policy is then masked by the legality constraints and renormalized before being used in MCTS, so soft constraints guide the search without overriding hard constraints or eliminating exploration. Algorithm 2 Soft Constraint Extraction and Policy Reweighting 1: MCTS traces D, progress buckets ℬB 2: Minimum samples m, tree hyperparameters (d,s,ℓ)(d,s, ) 3: Soft bias strength β 4: Collect state-action samples (xi,ai)(x_i,a_i) from MCTS 5: Retain high-confidence samples based on visit concentration and value estimates 6: Group samples into buckets bb∈ℬ\D_b\_b based on progress 7: for each bucket b∈ℬb do 8: if |b|<m|D_b|<m then 9: continue 10: end if 11: Train decision tree TbT_b with depth d, split s, leaf size ℓ 12: Extract leaf paths corresponding to high-confidence predictions 13: Convert each path into a rule (conditions→a)(conditions→ a) 14: Store rules with support and purity 15: end for 16: Build rule table indexed by progress and decision block 17: 18: Policy Reweighting during MCTS: 19: Given state s, compute neural policy P(⋅∣s)P(· s) 20: Identify rules satisfied by s and compute bias vector r(s)r(s) 21: Reweight policy: P~(a∣s)∝P(a∣s)(1+βra(s)) P(a s) P(a s)\,(1+β\,r_a(s)) 22: Apply legality mask and renormalize P~ P Figure 6: Impact of search knowledge discovery (KD) across theory spaces. Each panel is titled by metric and theory space. We compare CDRL with and without rule-based soft constraints on A4×ℤ4A_4×Z_4, A4×ℤNA_4×Z_N, and T19×ℤ4T_19×Z_4. Incorporating rules extracted from high-confidence search trajectories consistently improves both valid model rates and neutrino model discovery. Rule-guided runs achieve higher final performance and faster convergence, with gains of roughly 1.51.5–2×2× in valid models and 22–3×3× in neutrino models across the three spaces, demonstrating that the extracted rules provide useful and generalizable guidance for exploration. These experiments are performed using smaller-scale KD evaluation runs, so absolute values are not directly comparable to the full-scale results reported in Table 3. The extracted rules are simple if-else conditions over particle assignments that reveal recurring structure in successful models. For example, assignments of charged lepton singlets often follow consistent patterns (e.g., E1E_1 influencing E2,E3E_2,E_3 through identical or systematically shifted ℤ4Z_4 charges). We also observe coordinated triplet assignments across L, N, and ϕφ, mirroring common design patterns used by human model builders 23. Although extracted post-hoc, these rules provide reusable and generalizable structure. The full set of 40 rules is listed in Section C. Crucially, interpreting each rule within the model building process requires additional context not always captured within the decision tree, and many rules are more representative of the agent’s search process than of correlations between parameters of the model. For example, several of the observed rules for the ℤNZ_N charges of the charged lepton singlets (E1,E2,E3E_1,E_2,E_3) show them favoring identical or closely related charges. This is a reasonable pattern for correctly producing their masses if other particles have already been given appropriate representation assignments. However, some rules restrict themselves to only a subset of the charge values the symmetry allows. This demonstrates the limitation of interpreting these rules physically. Each tree is fit only to the high-confidence trajectories within a single progress bucket, a small, selective sample. Therefore, a tree can look like a high-confidence rule simply because the values outside it were rare in that particular sample, not because the wider search avoids them. While we introduce a tool for search knowledge discovery, further work in this direction may enable more robust interpretation of these discovered correlations in terms of useful model-building rules. Surfacing this kind of observation is still useful. It either flags a rule that will not hold up once tested on more data, or, when a pattern holds up under closer inspection, a regularity of the theory space a human model builder had not already anticipated. 6 Conclusion, Limitation, and Future Work We introduced CDRL, a framework for scientific discovery in large constrained hypothesis spaces. Unlike standard RL methods that rely primarily on scalar rewards, CDRL uses structured certificates from symbolic domain-specific reasoning tools to identify why candidates fail and convert these failures into reusable constraints. On neutrino flavor model discovery, CDRL consistently improves search efficiency across all theory spaces. Per candidate evaluated, it achieves up to 1.95× higher valid model rates and 6.33× higher neutrino model discovery than AMBer. Separately, reaching a comparable number of neutrino models requires up to 4× fewer physics evaluations (Table 4). CDRL also improves coverage of the theory space, matches AMBer’s best model complexity while discovering far more of them, and enables post-hoc search knowledge discovery through interpretable rules extracted from search trajectories. The core idea of CDRL is not specific to neutrino physics, nor to particle physics. Many scientific domains pair a large discrete design space with an expensive verifier and an external tool that can explain failures, including chemistry, materials science, and automated theorem proving. In each, the dominant cost is the verification step, so the same computational bottleneck we address here applies: a scalar reward wastes that expensive budget by letting the agent revisit equivalent failures, whereas a certificate removes the whole failing class once and for all. Wherever a reasoning tool can name the assignments responsible for a violation, CDRL can turn that explanation into a constraint that is reused across the search. Finally, the rules recovered through search knowledge discovery are useful beyond efficiency, as they compress what the agent learned into human-readable structure, which both accelerates future runs and gives scientists a first look at the regularities of a mathematical space they are only beginning to explore. We have not yet independently validated these rules as physically meaningful. At this stage, they describe regularities in how the search itself explores the space, which are themselves shaped by our design choices, and confirming which of them reflect genuine physical structure is left to future work with domain experts. The main limitation of CDRL is that it depends on the availability of useful certificate-generating tools and is currently best suited to structured, discrete search spaces where constraints can be represented and reused effectively. The framework could also introduce overhead in larger search spaces from certificate analysis and clause management. Future work will extend CDRL to broader scientific domains such as chemistry and materials science, where external verifiers can provide rich feedback. Another promising direction is to learn when and how to generalize certificates into reusable constraints, and to combine CDRL with foundation models so that neural priors, symbolic pruning, and scientific verification can work together in a unified discovery loop. Acknowledgments PJ was supported by a seed grant from the AI4Science Center in the College of Sciences at Georgia Tech. MF is supported by Fermilab which is administered by Fermi Forward Discovery Group, LLC under Contract No. 89243024CSC000002 with the U.S. Department of Energy, Office of Science, Office of High Energy Physics. JR is supported by a fellowship from the WATCHEP training grant from the U.S. Department of Energy, Office of Science. The work of VKP was supported in part by the U.S. National Science Foundation under Grant PHY-221028. References Abramson et al. (2024) J. Abramson, J. Adler, J. Dunger, R. Evans, T. Green, A. Pritzel, O. Ronneberger, L. Willmore, A. J. Ballard, J. Bambrick, et al. Accurate structure prediction of biomolecular interactions with AlphaFold 3. Nature 630 (8016), p. 493–500. Cited by: §1, §1, §2. Acharya et al. (2023) K. Acharya, W. Raza, C. Dourado, A. Velasquez, and H. H. Song Neurosymbolic reinforcement learning and planning: a survey. IEEE Transactions on Artificial Intelligence. Cited by: §2. Agrawal et al. (2024) L. A. Agrawal, A. Kanade, N. Goyal, S. Lahiri, and S. Rajamani Monitor-guided decoding of code LMs with static analysis of repository context. Advances in Neural Information Processing Systems 36. Cited by: §2. Ahmad et al. (2002) Q. R. Ahmad et al. Direct evidence for neutrino flavor transformation from neutral current interactions in the Sudbury Neutrino Observatory. Phys. Rev. Lett. 89, p. 011301. External Links: nucl-ex/0204008, Document Cited by: §2. Ahn et al. (2003) M. H. Ahn et al. Indications of neutrino oscillation in a 250 km long baseline experiment. Phys. Rev. Lett. 90, p. 041801. External Links: hep-ex/0212007, Document Cited by: §2. Alexander et al. (2026) S. Alexander, B. Bradley, L. Gouskos, and C. Niu Autonomous Discovery of Particle Physics Theories from Experimental Data. External Links: 2603.28935 Cited by: §1. Almumin et al. (2023) Y. Almumin, M. Chen, M. Cheng, V. Knapp-Perez, Y. Li, A. Mondol, S. Ramos-Sanchez, M. Ratz, and S. Shukla Neutrino Flavor Model Building and the Origins of Flavor and CP Violation. Universe 9 (12), p. 512. External Links: 2204.08668, Document Cited by: §1. Altmannshofer and Greljo (2025) W. Altmannshofer and A. Greljo Recent Progress in Flavor Model Building. Ann. Rev. Nucl. Part. Sci. 75 (1), p. 201–322. External Links: 2412.04549, Document Cited by: §2. Babu (2010) K. S. Babu TASI Lectures on Flavor Physics. In Theoretical Advanced Study Institute in Elementary Particle Physics: The Dawn of the LHC Era, p. 49–123. External Links: 0910.2948, Document Cited by: §2. Bai and Zhang (2025) X. Bai and X. Zhang Artificial intelligence-powered materials science. Nano-micro letters 17 (1), p. 135. Cited by: §1. Balyo et al. (2015) T. Balyo, P. Sanders, and C. Sinz Hordesat: a massively parallel portfolio sat solver. In International Conference on Theory and Applications of Satisfiability Testing, p. 156–172. Cited by: §4.7. Baretz et al. (2025) J. B. Baretz, M. Fieg, V. Ganesh, A. Ghosh, V. Knapp-Perez, J. Rudolph, and D. Whiteson Towards ai-assisted neutrino flavor theory design. arXiv preprint arXiv:2506.08080. Cited by: §B.3, §1, §1, §1, §2, §4.1, §4.4, §4.8, Table 3, §5.2, footnote 2. Bastani et al. (2018) O. Bastani, Y. Pu, and A. Solar-Lezama Verifiable reinforcement learning via policy extraction. Advances in neural information processing systems 31. Cited by: §5.4. Bellemare et al. (2020) M. G. Bellemare, S. Candido, P. S. Castro, J. Gong, M. C. Machado, S. Moitra, S. S. Ponda, and Z. Wang Autonomous navigation of stratospheric balloons using reinforcement learning. Nature 588 (7836), p. 77–82. Cited by: §2. Biere et al. (2009) A. Biere, H. van Maaren, and T. Walsh Handbook of satisfiability. SAGE Publications Limited. Cited by: §1, §1, §1, §4.3. Carta et al. (2025) F. Carta, A. Gauntlett, F. Griffin, and Y. He BPS spectroscopy with reinforcement learning. . External Links: 2501.14863 Cited by: §2. Chen et al. (2020) Y. Chen, C. Wang, O. Bastani, I. Dillig, and Y. Feng Program synthesis using deduction-guided reinforcement learning. In International Conference on Computer Aided Verification, p. 587–610. Cited by: §2. Cleveland et al. (1998) B. T. Cleveland, T. Daily, R. Davis, J. R. Distel, K. Lande, C. K. Lee, P. S. Wildenhain, and J. Ullman Measurement of the solar electron neutrino flux with the Homestake chlorine detector. Astrophys. J. 496, p. 505–526. External Links: Document Cited by: §2. Colelough and Regli (2025) B. C. Colelough and W. Regli Neuro-symbolic ai in 2024: a systematic review. arXiv preprint arXiv:2501.05435. Cited by: §2. Davis et al. (1962) M. Davis, G. Logemann, and D. Loveland A machine program for theorem-proving. Communications of the ACM 5 (7), p. 394–397. Cited by: §1, §1, §4.3. de Gouvêa et al. (2022) A. de Gouvêa, I. Mocioiu, S. Pastore, L. E. Strigari, L. Alvarez-Ruso, A. M. Ankowski, A. B. Balantekin, V. Brdar, M. Cadeddu, S. Carey, J. Carlson, M. -C. Chen, V. Cirigliano, W. Dekens, P. B. Denton, R. Dharmapalan, L. Everett, H. Gallagher, S. Gardiner, J. Gehrlein, L. Graf, W. C. Haxton, O. Hen, H. Hergert, S. Horiuchi, P. Q. Hung, J. Isaacson, N. Jachowicz, L. Jin, A. N. Khan, A. Lovato, P. A. N. Machado, K. Mahn, D. Marfatia, C. Mariani, E. Mereghetti, J. G. Morfín, A. Nicholson, G. Paz, R. Plestid, N. Rocco, I. Sarcevic, R. Schiavilla, A. Sousa, J. Tena-Vidal, M. L. Wagman, and A. Walker-Loud Theory of neutrino physics – snowmass tf11 (aka nf08) topical group report. External Links: 2209.07983, Link Cited by: §1. Degrave et al. (2022) J. Degrave, F. Felici, J. Buchli, M. Neunert, B. Tracey, F. Carpanese, T. Ewalds, R. Hafner, A. Abdolmaleki, D. de Las Casas, et al. Magnetic control of tokamak plasmas through deep reinforcement learning. Nature 602 (7897), p. 414–419. Cited by: §2. Ding and Meloni (2012) G. Ding and D. Meloni A Model for Tri-bimaximal Mixing from a Completely Broken A4A_4. Nucl. Phys. B 855, p. 21–45. External Links: 1108.2733, Document Cited by: §5.4. Esteban et al. (2020) I. Esteban, M. C. Gonzalez-Garcia, M. Maltoni, T. Schwetz, and A. Zhou The fate of hints: updated global analysis of three-flavor neutrino oscillations. JHEP 09, p. 178. External Links: 2007.14792, Document Cited by: §4.4. Fawzi et al. (2022) A. Fawzi, M. Balog, A. Huang, T. Hubert, B. Romera-Paredes, M. Barekatain, A. Novikov, F. J. R. Ruiz, J. Schrittwieser, G. Swirszcz, et al. Discovering faster matrix multiplication algorithms with reinforcement learning. Nature 610 (7930), p. 47–53. Cited by: §1, §2. Feruglio and Romanino (2021) F. Feruglio and A. Romanino Lepton flavour symmetries. External Links: 1912.06028, Link Cited by: §1, §2. Fukuda et al. (1998) Y. Fukuda et al. Evidence for oscillation of atmospheric neutrinos. Phys. Rev. Lett. 81, p. 1562–1567. External Links: hep-ex/9807003, Document Cited by: §2. Gell-Mann et al. (1979) M. Gell-Mann, P. Ramond, and R. Slansky Complex Spinors and Unified Theories. Conf. Proc. C 790927, p. 315–321. External Links: 1306.4669 Cited by: §2. Giarnetti and Meloni (2026) A. Giarnetti and D. Meloni Reinforcement Learning Techniques for the Flavor Problem in Particle Physics. Symmetry 18 (1), p. 131. External Links: 2510.25495, Document Cited by: §1. Glashow (1980) S. L. Glashow The Future of Elementary Particle Physics. NATO Sci. Ser. B 61, p. 687. External Links: Document Cited by: §2. Gow et al. (2022) S. Gow, M. Niranjan, S. Kanza, and J. G. Frey A review of reinforcement learning in chemistry. Digital Discovery 1 (5), p. 551–567. Cited by: §1. Guo et al. (2025) D. Guo, D. Yang, H. Zhang, J. Song, P. Wang, Q. Zhu, R. Xu, R. Zhang, S. Ma, X. Bi, et al. Deepseek-r1: incentivizing reasoning capability in LLMs via reinforcement learning. arXiv preprint arXiv:2501.12948. Cited by: §2. Halverson et al. (2019) J. Halverson, B. Nelson, and F. Ruehle Branes with brains: exploring string vacua with deep reinforcement learning. Journal of High Energy Physics 2019 (6). External Links: ISSN 1029-8479, Link, Document Cited by: §2. Harvey and Lukas (2021) T. R. Harvey and A. Lukas Quark Mass Models and Reinforcement Learning. JHEP 08, p. 161. External Links: 2103.04759, Document Cited by: §2. Hitzler et al. (2023) P. Hitzler, M. K. Sarker, and A. Eberhart Compendium of neurosymbolic artificial intelligence. Vol. 369, IOS Press. Cited by: §2. Horgan et al. (2018) D. Horgan, J. Quan, D. Budden, G. Barth-Maron, M. Hessel, H. van Hasselt, and D. Silver Distributed prioritized experience replay. corr abs/1803.00933 (2018). arXiv preprint arXiv:1803.00933. Cited by: §4.7. Ignatiev et al. (2018) A. Ignatiev, A. Morgado, and J. Marques-Silva PySAT: A Python toolkit for prototyping with SAT oracles. In SAT, p. 428–437. External Links: Link, Document Cited by: §B.2. Jana et al. (2023) P. Jana, P. Jha, H. Ju, G. Kishore, A. Mahajan, and V. Ganesh CoTran: an llm-based code translator using reinforcement learning with feedback from compiler and symbolic execution. arXiv preprint arXiv:2306.06755. Cited by: §2. Jha et al. (2025) P. Jha, P. Jana, P. Suresh, A. Arora, and V. Ganesh RLSF: fine-tuning LLMs via symbolic feedback. 28th European Conference on Artificial Intelligence. Cited by: §1, §2. Jha et al. (2010) S. Jha, S. Gulwani, S. A. Seshia, and A. Tiwari Oracle-guided component-based program synthesis. In Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering-Volume 1, p. 215–224. Cited by: §2. Jha and Seshia (2017) S. Jha and S. A. Seshia A theory of formal synthesis via inductive learning. Acta Informatica 54 (7), p. 693–726. Cited by: §2. Jumper et al. (2021) J. Jumper, R. Evans, A. Pritzel, T. Green, M. Figurnov, O. Ronneberger, K. Tunyasuvunakool, R. Bates, A. Žídek, A. Potapenko, et al. Highly accurate protein structure prediction with AlphaFold. nature 596 (7873), p. 583–589. Cited by: §1. Kambhampati et al. (2024) S. Kambhampati, K. Valmeekam, L. Guan, K. Stechly, M. Verma, S. Bhambri, L. Saldyt, and A. Murthy LLMs can’t plan, but can help planning in llm-modulo frameworks. arXiv preprint arXiv:2402.01817. Cited by: §2. Karagiorgi et al. (2022) G. Karagiorgi, G. Kasieczka, S. Kravitz, B. Nachman, and D. Shih Machine learning in the search for new fundamental physics. Nature Reviews Physics 4 (6), p. 399–412. Cited by: §2. King (2015) S. F. King Models of Neutrino Mass, Mixing and CP Violation. J. Phys. G 42, p. 123001. External Links: 1510.02091, Document Cited by: §2. Li et al. (2024) Z. Li, J. Sun, L. Murphy, Q. Su, Z. Li, X. Zhang, K. Yang, and X. Si A survey on deep learning for theorem proving. arXiv preprint arXiv:2404.09939. Cited by: §1. Liang et al. (2016) J. H. Liang, V. Ganesh, P. Poupart, and K. Czarnecki Learning rate based branching heuristic for sat solvers. In Theory and Applications of Satisfiability Testing–SAT 2016: 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings 19, p. 123–140. Cited by: §B.3, §2, Table 3. Liu et al. (2023) Y. Liu, Z. Yang, Z. Yu, Z. Liu, D. Liu, H. Lin, M. Li, S. Ma, M. Avdeev, and S. Shi Generative artificial intelligence and its applications in materials science: current situation and future perspectives. Journal of Materiomics 9 (4), p. 798–816. Cited by: §2. Mankowitz et al. (2023) D. J. Mankowitz, A. Michi, A. Zhernov, M. Gelmi, M. Selvi, C. Paduraru, E. Leurent, S. Iqbal, J. Lespiau, A. Ahern, et al. Faster sorting algorithms discovered using deep reinforcement learning. Nature 618 (7964), p. 257–263. Cited by: §1, §1, §2. Martín-Guerrero and Lamata (2021) J. D. Martín-Guerrero and L. Lamata Reinforcement learning and physics. Applied Sciences 11 (18), p. 8589. Cited by: §1. Melnikov et al. (2018) A. A. Melnikov, H. Poulsen Nautrup, M. Krenn, V. Dunjko, M. Tiersch, A. Zeilinger, and H. J. Briegel Active learning machine learns to create new quantum experiments. Proceedings of the National Academy of Sciences 115 (6), p. 1221–1226. Cited by: §2. Menouer and Baarir (2017) T. Menouer and S. Baarir Parallel learning portfolio-based solvers. Procedia Computer Science 108, p. 335–344. Cited by: §4.7. Merchant et al. (2023) A. Merchant, S. Batzner, S. S. Schoenholz, M. Aykol, G. Cheon, and E. D. Cubuk Scaling deep learning for materials discovery. Nature 624 (7990), p. 80–85. Cited by: §1, §2. Messeri and Crockett (2024) L. Messeri and M. J. Crockett Artificial intelligence and illusions of understanding in scientific research. Nature 627 (8002), p. 49–58. Cited by: §2. Minkowski (1977) P. Minkowski μ→eγμ→ eγ at a Rate of One Out of 10910^9 Muon Decays?. Phys. Lett. B 67, p. 421–428. External Links: Document Cited by: §2. Nishimura et al. (2020) S. Nishimura, C. Miyao, and H. Otsuka Exploring the flavor structure of quarks and leptons with reinforcement learning. JHEP 23, p. 021. External Links: 2304.14176, Document Cited by: §2. Nishimura et al. (2024) S. Nishimura, C. Miyao, and H. Otsuka Reinforcement learning-based statistical search strategy for an axion model from flavor. . External Links: 2409.10023 Cited by: §2. Polgreen et al. (2022) E. Polgreen, A. Reynolds, and S. A. Seshia Satisfiability and synthesis modulo oracles. In International Conference on Verification, Model Checking, and Abstract Interpretation, p. 263–284. Cited by: §2. Rosin (2011) C. D. Rosin Multi-armed bandits with episode context. Annals of Mathematics and Artificial Intelligence 61 (3), p. 203–230. Cited by: §4.7. Ruiz et al. (2025) F. J. Ruiz, T. Laakkonen, J. Bausch, M. Balog, M. Barekatain, F. J. Heras, A. Novikov, N. Fitzpatrick, B. Romera-Paredes, J. Van De Wetering, et al. Quantum circuit optimization with AlphaTensor. Nature Machine Intelligence 7 (3), p. 374–385. Cited by: §1, §2. Segler et al. (2018) M. H. Segler, M. Preuss, and M. P. Waller Planning chemical syntheses with deep neural networks and symbolic ai. Nature 555 (7698), p. 604–610. Cited by: §1. Silver et al. (2016) D. Silver, A. Huang, C. J. Maddison, A. Guez, L. Sifre, G. Van Den Driessche, J. Schrittwieser, I. Antonoglou, V. Panneershelvam, M. Lanctot, et al. Mastering the game of Go with deep neural networks and tree search. Nature 529 (7587), p. 484–489. Cited by: §B.3, Figure 1, Figure 1, §1, §1, §4.7, Table 3. Silver et al. (2017) D. Silver, J. Schrittwieser, K. Simonyan, I. Antonoglou, A. Huang, A. Guez, T. Hubert, L. Baker, M. Lai, A. Bolton, Y. Chen, T. Lillicrap, F. Hui, L. Sifre, G. van den Driessche, T. Graepel, and D. Hassabis Mastering the game of Go without human knowledge. Nature 550 (7676), p. 354–359. External Links: ISSN 1476-4687, Document, Link Cited by: Figure 1, Figure 1, §1, §1, §4.7. Singh et al. (2025) A. Singh, A. Fry, A. Perelman, A. Tart, A. Ganesh, A. El-Kishky, A. McLaughlin, A. Low, A. Ostrow, A. Ananthram, et al. Openai gpt-5 system card. arXiv preprint arXiv:2601.03267. Cited by: §B.3.1, Table 3. Sutton and Barto (2018) R. S. Sutton and A. G. Barto Reinforcement learning: an introduction. A Bradford Book, Cambridge, MA, USA. External Links: ISBN 0262039249 Cited by: §1. Van Noorden and Perkel (2023) R. Van Noorden and J. M. Perkel AI and science: what 1,600 researchers think. Nature 621 (7980), p. 672–675. Cited by: §2. Wang et al. (2023) H. Wang, T. Fu, Y. Du, W. Gao, K. Huang, Z. Liu, P. Chandak, S. Liu, P. Van Katwyk, A. Deac, et al. Scientific discovery in the age of artificial intelligence. Nature 620 (7972), p. 47–60. Cited by: §1, §2. Wojcik et al. (2025) G. N. Wojcik, S. T. Eu, and L. L. Everett Graph reinforcement learning for exploring model spaces beyond the standard model. Phys. Rev. D 111 (3), p. 035007. External Links: 2407.07203, Document Cited by: §1. Xu et al. (2021) Y. Xu, X. Liu, X. Cao, C. Huang, E. Liu, S. Qian, X. Liu, Y. Wu, F. Dong, C. Qiu, et al. Artificial intelligence: a powerful paradigm for scientific research. The innovation 2 (4). Cited by: §2. Yanagida (1979) T. Yanagida Horizontal gauge symmetry and masses of neutrinos. Conf. Proc. C 7902131, p. 95–99. Cited by: §2. Zhang and Gu (2025) J. Zhang and B. Gu Advances in reinforcement learning for intelligent program synthesis. In 2025 5th International Conference on Neural Networks, Information and Communication Engineering (NNICE), p. 1734–1739. Cited by: §1. The CDRL loop, step by step one MCTS tree, shown as it is built Figure 7: The CDRL mechanism, shown as four snapshots of the same tree. (1) Start: the empty model; three of the nine allowed ℤNZ_N choices are shown at the root. (2) Propose, mask, descend: at the root, and again at every node MCTS visits, the BCP referee masks the illegal children first and the policy-value network then ranks what remains; MCTS commits to ℤN=6Z_N=6 and descends, and the same red × masking recurs at each node along the way. Continued below. Figure 8: (continued) (3) Two signals from one evaluation: the branch completes and the candidate fails, rank-deficient for every ℤNZ_N charge; this single evaluation produces a scalar reward that retrains the network and, separately, a certificate that the analyzer converts into a clause added to the shared database. (4) Same pattern, different branch: MCTS next explores the sibling ℤN=4Z_N=4 branch, and the clause learned in step 3 masks the same representation-and-VEV pattern as soon as it recurs, before the branch is built out further or any physics evaluation is spent on it. Appendix A The CDRL Loop: A Step-by-Step Walkthrough Figure 7 below walks through a worked example as four snapshots of the same tree, taken as it is actually built, covering the same components as Figure 1 (the policy-value network, the BCP referee, MCTS, physics evaluation, the certificate analyzer, and the clause database) except search knowledge discovery, which operates offline after training and is not part of this per-candidate loop. Showing the same tree across panels also makes the key claim concrete rather than only described: a clause learned from one branch permanently prunes a matching pattern anywhere else in the tree. At every node, not only the root, the BCP referee first masks any child that would violate an already-learned clause, and the policy-value network then ranks the remaining legal children; this repeats at each subsequent decision (the ℤNZ_N choice, then each particle’s representation, then its charge, and so on). What Figure 7 shows as a single selected path is itself the outcome of many such simulations from the current state, each one descending through already-expanded nodes by upper-confidence bound and expanding one new leaf; the move actually played is the one visited most often across these simulations, not simply the network’s top-ranked action. As in Algorithm 1, the network is updated periodically from replay-buffer mini-batches rather than immediately after every single evaluation, and the certificate path in Step 3 only triggers when the completed candidate fails; a valid candidate produces a reward alone. The three ℤNZ_N choices at the root are an illustrative subset of the nine allowed in this theory space (N∈2,…,10N∈\2,…,10\). Appendix B Additional Experimental Details B.1 Compute Infrastructure All experiments are conducted on a machine with Intel Xeon Gold 6448Y CPUs (32 cores, 2.10 GHz), 32 GB RAM, and an NVIDIA H100 GPU (80GB, MIG 20GB partition). Parallel self-play is executed across CPU workers, while neural network training is performed on the GPU. The dominant computational cost in our setting arises from the physics evaluation pipeline, which involves symbolic model construction, numerical optimization, and parameter fitting for candidate theories. MCTS traversal and SAT-based propagation introduce additional overhead, but are comparatively lightweight relative to terminal model evaluation. Since different methods use different parallelization settings and compute configurations (CDRL uses 32 CPU cores, while AMBer uses 250 parallel environments), we report candidate evaluations as the primary normalized efficiency metric. B.2 Additional Implementation Details Our framework is implemented in PyTorch. We integrate symbolic constraint reasoning using a SAT solver backend, leveraging MiniSAT-style Boolean Constraint Propagation (BCP) via the PySAT library 37. Domain constraints are compiled into conjunctive normal form (CNF) and enforced during search. After each action, the solver applies BCP to propagate implied assignments, ensuring that all intermediate states remain consistent with hard constraints. For search knowledge discovery rule extraction (Section 5.4), we treat an MCTS decision as high-confidence when the dominant action receives more than 95%95\% of visits and has a positive value estimate. Progress buckets require at least 1010 such samples; each decision tree has maximum depth 33, requires at least 1010 samples to split a node and 55 samples per leaf, and is fit with an 80/20 train-test split when enough data is available. B.3 Baselines We compare against AMBer (Autonomous Model Builder) 12, an RL framework for neutrino flavor model discovery. AMBer performs iterative model refinement using scalar rewards derived from the physics evaluation pipeline, including χ2χ^2 fit quality, the number of free parameters, and a bonus for exploring higher-order ℤNZ_N symmetry groups. Unlike CDRL, AMBer does not use certificate-driven symbolic pruning or reusable constraint learning. We additionally compare against several ablated and hybrid baselines, including pure MCTS search, DNN-only policies, symbolic-only SAT-based search 47, and a DNN+MCTS framework 62. These baselines isolate the contributions of planning, neural guidance, and symbolic reasoning. B.3.1 LLM Baseline Details We evaluate a prompting-based baseline using GPT-5.3 64. The model is prompted to directly generate candidate neutrino flavor model matrices satisfying the required representation, charge, and VEV assignment format used throughout the paper. The prompt contains: (i) a task description explaining the flavor model construction problem, (i) formatting instructions specifying the matrix structure and allowed assignments, and (i) 3 few-shot examples of valid candidate model matrices drawn from the corresponding theory space. The model is then asked to generate new candidate matrices autoregressively. Generated outputs are parsed into matrix form and evaluated using the same symbolic constraints and physics evaluation pipeline used for all other methods. Invalid, incomplete, or unparsable outputs are counted as failed candidates. We use temperature 0.8 and top-p 0.95 decoding for generation. The baseline does not use search, SAT-based propagation, iterative refinement, or certificate-driven feedback, and therefore serves as a reference point for pure prompting-based generation without structured exploration. B.4 Neural Network Architecture The policy-value network operates on a flattened matrix representation of the state. The architecture consists of: • Fully connected layer: 512 units with BatchNorm and ReLU • Fully connected layer: 256 units with BatchNorm and ReLU • Policy head: linear layer to action dimension followed by log-softmax • Value head: linear layer followed by tanh B.5 Additional Training Details We provide the concrete hyperparameters for the MCTS and network training described in Section 4. We use: • Max iterations: 30 • Episodes per iteration: 100 • MCTS simulations per move: 150 • MCTS cpuctc_puct: 0.5 • Batch size: 512 • Training epochs per iteration: 20 • Optimizer: Adam The policy head is trained using cross-entropy loss against MCTS visit counts, while the value head is trained using mean squared error against normalized terminal rewards. After each training iteration, the updated model is evaluated against the previous checkpoint in a single-agent self-play evaluation setting. Both models independently generate candidate solutions using the same environment and evaluation pipeline, and we compare their cumulative terminal rewards across a fixed number of evaluation episodes. The checkpoint is updated only if the new model achieves higher cumulative reward than the previous model. Unlike standard AlphaZero pit-play, this comparison does not involve a competitive two-player game, since neutrino model discovery is a single-agent environment. B.6 Parallelization We employ a portfolio-style parallelization strategy inspired by parallel SAT solvers. Multiple workers independently perform MCTS-guided self-play while sharing: • neural network replay buffers • a global database of learned conflict clauses Conflict clauses discovered by any worker are synchronized globally and reused by all workers. Additionally, expensive terminal evaluations are cached to avoid redundant computation. This combination of parallel search and clause sharing significantly improves exploration efficiency and sample efficiency. In our current implementation, learned clauses are accumulated monotonically and shared across workers, and we do not employ CDCL-style clause deletion. In practice, this remains computationally manageable because SAT propagation constitutes only a small fraction of the total runtime, while the dominant cost arises from the physics evaluation pipeline. Although the number of learned certificates grows over training, we did not observe clause management becoming a bottleneck in the theory spaces considered in this work. For larger domains, clause forgetting or activity-based clause management would be a natural extension. Appendix C Search Knowledge Discovery Rule Galleries Below we list the full set of observations extracted from the high-confidence MCTS trajectories in each theory space, using the procedure described in Section 5.4. Each observation is a shallow decision tree that predicts one block assignment (a representation or a ℤNZ_N charge) from earlier assignments in the same partial model; an observation that collapses to a single leaf is a constant assignment, always taking the same value in the high-confidence set. For every tree we report the train and test accuracy of the predicted assignment. In the two-way trees, the left branch is the Yes outcome of the condition and the right branch is No. These rules are extracted post-hoc and reused as the soft policy bias of Algorithm 2; the aggregate effect of reusing them is reported in Figure 6. C.1 A4×ℤ4A_4×Z_4 Constant assignments L1.rep = 3E1.rep = 1”E1.Z4 = 4E2.rep = 1E3.rep = 1’N1.rep = 3phi1.rep = 3phi2.rep = 3 E2.Z4_charge Train: 0.917 Test: 0.917 E1.Z4 = 3?3E1.Z4 = 1?12YesNoYesNo E3.Z4_charge Train: 0.972 Test: 0.944 E2.Z4 = 1?1E1.Z4 = 4?42YesNoYesNo N1.Z4_charge Train: 0.911 Test: 1.000 L2.Z4 = 3?2E3.Z4 = 1?24YesNoYesNo Hd.rep Train: 0.615 Test: NA E3.rep = 1’?11’YesNo phi1.Z4_charge Train: 0.654 Test: 0.429 Hu.Z4 = 2?3Hu.Z4 = 4?3E1.Z4 = 1?43YesNoYesNoYesNo phi2.Z4_charge Train: 0.719 Test: 0.444 Hu.Z4 = 1?42YesNo C.2 A4×ℤNA_4×Z_N Constant assignments L1.rep = 3E2.rep = 1’N1.rep = 3phi1.rep = 3phi2.rep = 3phi3.rep = 3phi4.rep = 3 E2.Z5_charge Train: 0.938 Test: 0.882 E1.Z5 = 2?2E1.Z5 = 1?14YesNoYesNo E3.rep Train: 0.707 Test: 0.727 E2.rep = 1’?1”1YesNo E3.Z5_charge Train: 0.926 Test: 0.968 E2.Z5 = 4?4E1.Z5 = 2?2E2.Z5 = 1?15YesNoYesNoYesNo N1.Z5_charge Train: 0.861 Test: 0.900 E2.Z5 = 3?3E1.Z5 = 2?2L3.Z5 = 5?42YesNoYesNoYesNo Hu.rep Train: 0.889 Test: 0.600 E3.rep = 1”?1’E3.rep = 1?1’1”YesNoYesNo C.3 T19×ℤ4T_19×Z_4 Left edge: Yes Right edge: No L1.Z4_charge Train: 0.792 Test: 0.714 4 E1.Z4_charge Train: 0.611 Test: 0.600 L2.Z4 = 4?1L1.Z4 = 1?21 E2.rep Train: 0.950 Test: 0.905 E1.rep = 1?1’1 E2.Z4_charge Train: 0.938 Test: 0.857 E1.Z4 = 2?2E1.Z4 = 1?13 E3.rep Train: 0.685 Test: 0.694 E1.rep = 1”?E2.rep = 1”?1’1”1 E3.Z4_charge Train: 0.924 Test: 0.926 E1.Z4 = 2?2E2.Z4 = 4?4E2.Z4 = 3?31 N1.rep Train: 0.960 Test: 0.932 L2.rep = 3_3b?3_33_3b Hu.rep Train: 0.522 Test: 0.667 E3.rep = 1?1”N3.rep = 3_2b?1’N1.rep = 3_3?1’1 Hu.Z4_charge Train: 0.978 Test: 0.833 4 Hd.rep Train: 0.821 Test: 0.875 N3.rep = 3_2?1”E2.rep = 1?1”1 phi1.rep Train: 0.859 Test: 0.941 L3.rep = 3_3b?3_2bE1.rep = 1?3_33_3b phi2.rep Train: 0.750 Test: 0.625 N2.rep = 3_3?3_2bE1.rep = 1”?3_2N3.rep = 3_2?3_13_3 phi3.rep Train: 0.741 Test: 0.714 N1.rep = 3_3?3_2b3_1 phi5.rep Train: 0.857 Test: 0.750 3_2b