CDRL: Certification-Driven Reinforcement Learning for Neutrino Flavor Model Discovery

# CDRL: Certification-Driven Reinforcement Learning for Neutrino Flavor Model Discovery
Source: [https://arxiv.org/html/2608.20686](https://arxiv.org/html/2608.20686)
Jake RudolphAffiliation:University of California, Irvine, USAVictoria Knapp\-PérezAffiliation:University of California, Irvine, USAAffiliation: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\.eduMax FiegAffiliation:Particle Theory Department, Fermilab, USAAishik GhoshAffiliation:School of Physics, Georgia Institute of Technology, USAAffiliation:Lawrence Berkeley National Laboratory, USAVijay Ganesh\[4pt\] School of Computer ScienceGeorgia Institute of TechnologyUSA

###### 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 theactionsresponsible 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 exceeds102610^\{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×\\timeshigher valid model rates and up to 6\.33×\\timeshigher neutrino model rates while evaluating up to 4×\\timesfewer 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×\\timesin valid model rates and 3×\\timesin 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\.

## 1Introduction

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](https://arxiv.org/html/2608.20686#bib.bib37);[26](https://arxiv.org/html/2608.20686#bib.bib43);[7](https://arxiv.org/html/2608.20686#bib.bib45);[21](https://arxiv.org/html/2608.20686#bib.bib44), computational biology[42](https://arxiv.org/html/2608.20686#bib.bib38), chemistry[61](https://arxiv.org/html/2608.20686#bib.bib35), and materials science[10](https://arxiv.org/html/2608.20686#bib.bib36)\. 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](https://arxiv.org/html/2608.20686#bib.bib20);[1](https://arxiv.org/html/2608.20686#bib.bib26);[49](https://arxiv.org/html/2608.20686#bib.bib21)\.

A common approach to exploring large hypothesis spaces is reinforcement learning \(RL\)[65](https://arxiv.org/html/2608.20686#bib.bib58), 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](https://arxiv.org/html/2608.20686#bib.bib29), program synthesis[71](https://arxiv.org/html/2608.20686#bib.bib28), and scientific discovery[67](https://arxiv.org/html/2608.20686#bib.bib34);[50](https://arxiv.org/html/2608.20686#bib.bib33);[31](https://arxiv.org/html/2608.20686#bib.bib32)\. However, these methods typically rely on scalar reward signals that provide little information about why a candidate fails[39](https://arxiv.org/html/2608.20686#bib.bib27)\. 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](https://arxiv.org/html/2608.20686#bib.bib9);[63](https://arxiv.org/html/2608.20686#bib.bib57)\. 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](https://arxiv.org/html/2608.20686#S4.SS4)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](https://arxiv.org/html/2608.20686#S4.SS3)gives the formal, SAT\-based definition of the referee and constraint database, and Table[2](https://arxiv.org/html/2608.20686#S4.T2)works out the ways a certificate can arise\. Figure[7](https://arxiv.org/html/2608.20686#A0.F7)\(Appendix[A](https://arxiv.org/html/2608.20686#A1)\) 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 producecertificates111A 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](https://arxiv.org/html/2608.20686#S3)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](https://arxiv.org/html/2608.20686#S1.F2)\)\.

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](https://arxiv.org/html/2608.20686#bib.bib70);[12](https://arxiv.org/html/2608.20686#bib.bib37);[6](https://arxiv.org/html/2608.20686#bib.bib69);[29](https://arxiv.org/html/2608.20686#bib.bib71)\. 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](https://arxiv.org/html/2608.20686#bib.bib37), 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 than102610^\{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](https://arxiv.org/html/2608.20686#S3)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](https://arxiv.org/html/2608.20686#bib.bib4)\. 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](https://arxiv.org/html/2608.20686#bib.bib9);[63](https://arxiv.org/html/2608.20686#bib.bib57), this symbolic reasoning layer is implemented via Boolean Constraint Propagation \(BCP\)[20](https://arxiv.org/html/2608.20686#bib.bib10);[15](https://arxiv.org/html/2608.20686#bib.bib4), 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\-AbelianA4A\_\{4\}representation assignment is invalid for*any*choice ofℤN\\mathbb\{Z\}\_\{N\}charge \(Figure[1](https://arxiv.org/html/2608.20686#S1.F1)\)\. 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](https://arxiv.org/html/2608.20686#S4)\)\. 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](https://arxiv.org/html/2608.20686#bib.bib10);[15](https://arxiv.org/html/2608.20686#bib.bib4), the same unit\-propagation mechanism used inside modern SAT solvers[15](https://arxiv.org/html/2608.20686#bib.bib4); and the search itself is an AlphaZero\-style Monte Carlo Tree Search \(MCTS\)[62](https://arxiv.org/html/2608.20686#bib.bib9);[63](https://arxiv.org/html/2608.20686#bib.bib57)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](https://arxiv.org/html/2608.20686#S5)\), and further show that the constraints and decision patterns CDRL accumulates expose reusable structure in the theory space \(Section[5\.4](https://arxiv.org/html/2608.20686#S5.SS4)\)\.

Across three theory spaces for neutrino flavor model discovery, CDRL achieves up to1\.95×1\.95\\timeshigher valid model rates and up to6\.33×6\.33\\timeshigher neutrino model rates than AMBer[12](https://arxiv.org/html/2608.20686#bib.bib37), while evaluating up to4×4\\timesfewer 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](https://arxiv.org/html/2608.20686#bib.bib30);[60](https://arxiv.org/html/2608.20686#bib.bib19);[49](https://arxiv.org/html/2608.20686#bib.bib21);[1](https://arxiv.org/html/2608.20686#bib.bib26)\.

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 contributionsare therefore: \(i\) CDRL, a certificate\-driven RL framework that transforms symbolic failure certificates into reusable search constraints, progressively eliminating large invalid regions; \(ii\) state\-of\-the\-art results on neutrino flavor model discovery, achieving substantially higher discovery rates with fewer evaluations than prior RL approaches; and \(iii\) 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 theT19×ℤ4T\_\{19\}\\times\\mathbb\{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\\chi^\{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](https://arxiv.org/html/2608.20686#A3)\.LLE1E\_\{1\}E2E\_\{2\}E3E\_\{3\}NNHuH\_\{u\}HdH\_\{d\}ϕ1\\phi\_\{1\}ϕ2\\phi\_\{2\}ϕ3\\phi\_\{3\}ϕ4\\phi\_\{4\}ϕ5\\phi\_\{5\}ϕ6\\phi\_\{6\}T19T\_\{19\}𝟑1\\mathbf\{3\}\_\{1\}𝟏′′\\mathbf\{1\}^\{\\prime\\prime\}𝟏\\mathbf\{1\}𝟏′\\mathbf\{1\}^\{\\prime\}𝟑¯2\\bar\{\\mathbf\{3\}\}\_\{2\}𝟏′\\mathbf\{1\}^\{\\prime\}𝟏\\mathbf\{1\}𝟑1\\mathbf\{3\}\_\{1\}𝟑¯1\\bar\{\\mathbf\{3\}\}\_\{1\}𝟑1\\mathbf\{3\}\_\{1\}𝟑¯1\\bar\{\\mathbf\{3\}\}\_\{1\}𝟑2\\mathbf\{3\}\_\{2\}𝟑2\\mathbf\{3\}\_\{2\}ℤ4\\mathbb\{Z\}\_\{4\}44222222442244222233444411
## 2Background 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](https://arxiv.org/html/2608.20686#bib.bib39);[4](https://arxiv.org/html/2608.20686#bib.bib42);[18](https://arxiv.org/html/2608.20686#bib.bib41);[5](https://arxiv.org/html/2608.20686#bib.bib40)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](https://arxiv.org/html/2608.20686#bib.bib3);[26](https://arxiv.org/html/2608.20686#bib.bib43);[8](https://arxiv.org/html/2608.20686#bib.bib2);[45](https://arxiv.org/html/2608.20686#bib.bib1): 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](https://arxiv.org/html/2608.20686#bib.bib49);[70](https://arxiv.org/html/2608.20686#bib.bib48);[30](https://arxiv.org/html/2608.20686#bib.bib47);[28](https://arxiv.org/html/2608.20686#bib.bib46), 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 flavons222In 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](https://arxiv.org/html/2608.20686#bib.bib37), 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](https://arxiv.org/html/2608.20686#bib.bib52);[34](https://arxiv.org/html/2608.20686#bib.bib53);[56](https://arxiv.org/html/2608.20686#bib.bib54);[57](https://arxiv.org/html/2608.20686#bib.bib55);[16](https://arxiv.org/html/2608.20686#bib.bib56)has demonstrated RL as a tool for searching analogous spaces of models for various areas in particle physics\. In particular, the AMBer framework[12](https://arxiv.org/html/2608.20686#bib.bib37)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](https://arxiv.org/html/2608.20686#bib.bib34);[69](https://arxiv.org/html/2608.20686#bib.bib14)\. 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](https://arxiv.org/html/2608.20686#bib.bib20);[48](https://arxiv.org/html/2608.20686#bib.bib17), and biomolecular structure prediction using deep learning systems like AlphaFold[1](https://arxiv.org/html/2608.20686#bib.bib26)\. Machine learning is also widely used in particle physics for analyzing experimental data and identifying potential new phenomena[44](https://arxiv.org/html/2608.20686#bib.bib18)\. Alongside these developments, there is growing interest in incorporating domain knowledge and reasoning into AI\-driven discovery processes[54](https://arxiv.org/html/2608.20686#bib.bib15);[66](https://arxiv.org/html/2608.20686#bib.bib16)\. 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](https://arxiv.org/html/2608.20686#bib.bib30), AlphaTensor\-Quantum for fault\-tolerant quantum circuits[60](https://arxiv.org/html/2608.20686#bib.bib19), and AlphaDev for faster sorting[49](https://arxiv.org/html/2608.20686#bib.bib21)\. It has also controlled physical systems and experiments such as tokamak plasmas[22](https://arxiv.org/html/2608.20686#bib.bib24), stratospheric balloons[14](https://arxiv.org/html/2608.20686#bib.bib25), and quantum experiment design[51](https://arxiv.org/html/2608.20686#bib.bib23)\. 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](https://arxiv.org/html/2608.20686#bib.bib64);[2](https://arxiv.org/html/2608.20686#bib.bib61)\. Integration strategies range from embedding symbolic rules within neural architectures and differentiable reasoning modules to modular systems that call external reasoning tools[19](https://arxiv.org/html/2608.20686#bib.bib22)\. 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](https://arxiv.org/html/2608.20686#bib.bib22), 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](https://arxiv.org/html/2608.20686#bib.bib63);[3](https://arxiv.org/html/2608.20686#bib.bib62);[17](https://arxiv.org/html/2608.20686#bib.bib60);[38](https://arxiv.org/html/2608.20686#bib.bib59), while other approaches incorporate external feedback during RL[32](https://arxiv.org/html/2608.20686#bib.bib11);[39](https://arxiv.org/html/2608.20686#bib.bib27)\. Related ideas also appear in automated reasoning and synthesis\. Modern SAT solvers use conflict feedback to guide search[47](https://arxiv.org/html/2608.20686#bib.bib65), and frameworks such as CEGIS and Satisfiability Modulo Oracles refine candidates using counterexamples or constraints from external verifiers[40](https://arxiv.org/html/2608.20686#bib.bib31);[58](https://arxiv.org/html/2608.20686#bib.bib12);[41](https://arxiv.org/html/2608.20686#bib.bib13)\. 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\.

## 3Certification\-Driven Reinforcement Learning \(CDRL\)

Algorithm 1Certification\-Driven Reinforcement Learning \(CDRL\)1:Notation:

πθ\\pi\_\{\\theta\}policy\-value network;

VVverifier \(the physics evaluation pipeline\);

𝒜\\mathcal\{A\}certificate analyzer;

𝒦0,𝒦\\mathcal\{K\}\_\{0\},\\mathcal\{K\}initial and accumulated constraint sets;

HHspace of candidate hypotheses \(models\);

h∈Hh\\in Hone candidate;

ℋvalid\\mathcal\{H\}\_\{\\text\{valid\}\}set of discovered valid hypotheses;

σ\\sigmaa certificate returned by

VVon failure;

ccthe constraint derived from

σ\\sigma\.

2:

3:Policy

πθ\\pi\_\{\\theta\}, verifier

VV, certificate analyzer

𝒜\\mathcal\{A\}, initial constraints

𝒦0\\mathcal\{K\}\_\{0\}
4:Set of valid theories

ℋvalid\\mathcal\{H\}\_\{\\text\{valid\}\}
5:

𝒦←𝒦0\\mathcal\{K\}\\leftarrow\\mathcal\{K\}\_\{0\}⊳\\trianglerightinitialize with known domain constraints

6:

ℋvalid←∅\\mathcal\{H\}\_\{\\text\{valid\}\}\\leftarrow\\emptyset⊳\\trianglerightstore discovered valid solutions

7:foreach training episodedo

8:

h∼Plan​\(πθ,𝒦\)h\\sim\\textsc\{Plan\}\(\\pi\_\{\\theta\},\\mathcal\{K\}\)⊳\\trianglerightconstruct candidate while respecting accumulated constraints

9:

\(s​t​a​t​u​s,σ\)←V⁡\(h\)\(status,\\sigma\)\\leftarrow V\(h\)⊳\\trianglerightevaluate candidate and optionally return failure certificateσ\\sigma

10:if

s​t​a​t​u​s=validstatus=\\text\{valid\}then

11:

ℋvalid←ℋvalid∪\{h\}\\mathcal\{H\}\_\{\\text\{valid\}\}\\leftarrow\\mathcal\{H\}\_\{\\text\{valid\}\}\\cup\\\{h\\\}⊳\\trianglerightrecord valid hypothesis

12:Store trajectory and reward in replay buffer

13:else

14:

c←𝒜⁡\(σ\)c\\leftarrow\\mathcal\{A\}\(\\sigma\)⊳\\trianglerightconvert certificate into reusable constraint

15:

𝒦←𝒦∪\{c\}\\mathcal\{K\}\\leftarrow\\mathcal\{K\}\\cup\\\{c\\\}⊳\\trianglerightprune entire class of invalid solutions

16:Store trajectory and penalty in replay buffer

17:endif

18:Periodically update

πθ\\pi\_\{\\theta\}from replay\-buffer mini\-batches

19:endfor

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, letHHdenote the space of candidate hypotheses and let𝒦0\\mathcal\{K\}\_\{0\}denote a set of initial domain constraints known a priori\. The agent maintains a growing set of constraints𝒦\\mathcal\{K\}initialized with𝒦0\\mathcal\{K\}\_\{0\}\. During training, the agent proposes candidate hypotheses using a planning procedurePlan​\(πθ,𝒦\)\\textsc\{Plan\}\(\\pi\_\{\\theta\},\\mathcal\{K\}\)\(such as MCTS\), which incrementally constructs candidates while enforcing constraints𝒦\\mathcal\{K\}and usingπθ\\pi\_\{\\theta\}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𝒦\\mathcal\{K\}and used to prune the search space\.

The overall CDRL procedure is shown in Algorithm[1](https://arxiv.org/html/2608.20686#alg1)\. 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\. Leth∈Hh\\in Hdenote a candidate hypothesis\. Whenhhis invalid or redundant with an already\-covered equivalent hypothesis, the verifier returns a certificateσ\\sigma, which is analyzed to derive a constraintccthat prevents similar configurations\. This constraint is added to𝒦\\mathcal\{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\.

## 4Application: 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](https://arxiv.org/html/2608.20686#S1.F1)shows how the components below fit together; further background is provided in Section[2](https://arxiv.org/html/2608.20686#S2)\.

### 4\.1Matrix Representation of Candidate Models

Following the AMBer framework[12](https://arxiv.org/html/2608.20686#bib.bib37), 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ℤN\\mathbb\{Z\}\_\{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\.2Sequential 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ℤN\\mathbb\{Z\}\_\{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\.3SAT\-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ℤN\\mathbb\{Z\}\_\{N\}symmetry \(a modeling choice that reduces the search space\), exactly one charge per particle for that activeℤN\\mathbb\{Z\}\_\{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](https://arxiv.org/html/2608.20686#bib.bib10);[15](https://arxiv.org/html/2608.20686#bib.bib4)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\.4RL environment and reward

We use the same particle physics evaluation pipeline as AMBer[12](https://arxiv.org/html/2608.20686#bib.bib37)for direct comparison\. A terminal state corresponds to a fully specified model matrix, which is passed to the physics tools\. UsingModel2Mass, 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\. Usingflavorpy, the model’s free parameters are then fit to neutrino observables from NuFit 5\.3[24](https://arxiv.org/html/2608.20686#bib.bib51)and scored by a chi\-squared goodness of fitχ2\\chi^\{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 than5050free parameters\); such models receive a strong penalty\. Valid models are scored by a reward that combines \(i\) the chi\-squared fit quality and \(ii\) the number of free parametersnpn\_\{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\\chi^\{2\}\\leq 10andnp≤7n\_\{p\}\\leq 7\. Because each evaluation requires expensive numerical optimization and dominates runtime \(approx\. 98%; Section[5](https://arxiv.org/html/2608.20686#S5)\), avoiding invalid and redundant regions of the search space before evaluation is critical\. Full experimental and compute details are given in Appendix[B](https://arxiv.org/html/2608.20686#A2)\.

### 4\.5Certificate Extraction and Conflict Clauses

Beyond scalar rewards, CDRL extracts structured certificates from invalid candidate models and converts them into reusableconflict clausesadded to the global constraint set𝒦\\mathcal\{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 \(ii\)*ℤN\\mathbb\{Z\}\_\{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 divisordd\(checked in both directions between the smaller and larger group\), and charge assignments related by negationq↦−qmodNq\\mapsto\-q\\bmod N, an automorphism of order 2, both of which preserve the theory’s selection rule\. Table[2](https://arxiv.org/html/2608.20686#S4.T2)demonstrates how each type of certificate works on a commonℤ6\\mathbb\{Z\}\_\{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ℤ6\\mathbb\{Z\}\_\{6\}candidate; the full derivation follows below\. Certificates 2 and 3 depend only on theℤN\\mathbb\{Z\}\_\{N\}charges, independent of representations or VEVs\. Every clause is¬\(the equivalent or excluded pattern\)\\neg\(\\text\{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\.DescriptionExampleClauseInsufficient\-rank representationModel already rank\-deficient withoutℤN\\mathbb\{Z\}\_\{N\}symmetryReps and VEVs withℤ6\\mathbb\{Z\}\_\{6\}charges wildcarded already rank\-deficient¬\\neg\(reps & VEV, any charges\)Abelian symmetry reducibilityℤN​\[qi\]≅ℤN/d​\[qi/d\]\\mathbb\{Z\}\_\{N\}\[q\_\{i\}\]\\cong\\mathbb\{Z\}\_\{N/d\}\[q\_\{i\}/d\]ℤ6​\[2,4,6\]↦ℤ3​\[1,2,3\]\\mathbb\{Z\}\_\{6\}\\,\[2,4,6\]\\mapsto\\mathbb\{Z\}\_\{3\}\\,\[1,2,3\]¬\\neg\(other representative\)Charge negationℤN​\[qi\]≅ℤN​\[−qi​mod N\]\\mathbb\{Z\}\_\{N\}\[q\_\{i\}\]\\cong\\mathbb\{Z\}\_\{N\}\[\-q\_\{i\}\\text\{ mod N\}\]ℤ6​\[2,4,6\]↦ℤ6​\[4,2,6\]\\mathbb\{Z\}\_\{6\}\\,\[2,4,6\]\\mapsto\\mathbb\{Z\}\_\{6\}\\,\[4,2,6\]¬\\neg\(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ℤN\\mathbb\{Z\}\_\{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ℤN\\mathbb\{Z\}\_\{N\}model share a common divisordd, then the model is reducible to aℤN/d\\mathbb\{Z\}\_\{N/d\}model\. Formally, if

qi=d​ai,N=d​M,q\_\{i\}=da\_\{i\},\\qquad N=dM,then the selection rule

q1\+q2\+q3=0\(modN\)q\_\{1\}\+q\_\{2\}\+q\_\{3\}=0\\pmod\{N\}is equivalent to

a1\+a2\+a3=0\(modM\)\.a\_\{1\}\+a\_\{2\}\+a\_\{3\}=0\\pmod\{M\}\.This implies that the larger symmetry provides no additional structure beyond the reduced groupℤM\\mathbb\{Z\}\_\{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\\mapsto\-q\\bmod N, preserves the selection rule∑iqi≡0\(modN\)\\sum\_\{i\}q\_\{i\}\\equiv 0\\pmod\{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\.6Learned 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](https://arxiv.org/html/2608.20686#S4.SS3)\)\. Instead, a forced literal implied by the clauses is propagated into the state\. Figure[1](https://arxiv.org/html/2608.20686#S1.F1)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](https://arxiv.org/html/2608.20686#S1.F2)\), so large regions of the search space are pruned permanently rather than merely down\-weighted\.

### 4\.7MCTS, Neural Guidance, and Portfolio Parallelization

We search the space of partial model matrices using MCTS[62](https://arxiv.org/html/2608.20686#bib.bib9);[63](https://arxiv.org/html/2608.20686#bib.bib57)\. 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](https://arxiv.org/html/2608.20686#S4.SS3)\), ensuring only constraint\-consistent actions are explored, and the masked priors guide tree traversal via PUCT[59](https://arxiv.org/html/2608.20686#bib.bib6)\. 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](https://arxiv.org/html/2608.20686#S5.T5)\)\.

To scale search, we employ portfolio\-style parallelization inspired by parallel SAT solvers[11](https://arxiv.org/html/2608.20686#bib.bib8);[52](https://arxiv.org/html/2608.20686#bib.bib7)and distributed RL[36](https://arxiv.org/html/2608.20686#bib.bib67)\. Multiple workers independently perform MCTS self\-play while sharing \(i\) a replay buffer for network retraining and \(ii\) 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 to2×2\\times\(Table[5](https://arxiv.org/html/2608.20686#S5.T5)\)\. Additional details are in Appendices[B\.5](https://arxiv.org/html/2608.20686#A2.SS5)and[B\.6](https://arxiv.org/html/2608.20686#A2.SS6)\.

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](https://arxiv.org/html/2608.20686#S4.SS3)\); 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](https://arxiv.org/html/2608.20686#A2.SS3); this isolates that component’s contribution rather than testing an independent reimplementation\.MethodCategoryA4×ℤ4A\_\{4\}\\times\\mathbb\{Z\}\_\{4\}A4×ℤNA\_\{4\}\\times\\mathbb\{Z\}\_\{N\}T19×ℤ4T\_\{19\}\\times\\mathbb\{Z\}\_\{4\}Valid \(%\)Neutrino \(%\)Min ParamsValid \(%\)Neutrino \(%\)Min ParamsValid \(%\)Neutrino \(%\)Min ParamsUninformed and LLM baselinesRandomRandom search0\.10\.00120\.10\.00140\.10\.0016ChatGPT \(GPT\-5\.3\)[64](https://arxiv.org/html/2608.20686#bib.bib68)Few\-shot prompting0\.20\.00130\.20\.00180\.10\.0015Search and learning hybridsAlphaZero[62](https://arxiv.org/html/2608.20686#bib.bib9)DNN \+ MCTS14\.90\.01716\.20\.0375\.40\.045MCTS onlyTree search only10\.20\.0099\.80\.00101\.10\.007DNN onlyPolicy/value network5\.10\.00134\.50\.0092\.20\.017Symbolic only[47](https://arxiv.org/html/2608.20686#bib.bib65)CDCL SAT solver0\.20\.00120\.20\.00120\.10\.0010State\-of\-the\-artAMBer[12](https://arxiv.org/html/2608.20686#bib.bib37)DNN \+ PPO19\.530\.02513\.790\.03511\.020\.034CDRL \(Ours\)DNN \+ MCTS \+ certificates28\.1±\\pm3\.3\(1\.44×\\times\)0\.10±\\pm0\.01\(5\.00×\\times\)526\.9±\\pm3\.7\(1\.95×\\times\)0\.19±\\pm0\.05\(6\.33×\\times\)518\.2±\\pm2\.1\(1\.65×\\times\)0\.09±\\pm0\.02\(3\.00×\\times\)4

### 4\.8Benchmark Theory Spaces

We evaluate CDRL on neutrino flavor model discovery using the same theory spaces as AMBer[12](https://arxiv.org/html/2608.20686#bib.bib37)to ensure direct comparability\. The search space consists of discrete flavor symmetry models defined by non\-Abelian representations, AbelianℤN\\mathbb\{Z\}\_\{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 flavonsnϕn\_\{\\phi\}: \(i\)A4×ℤ4A\_\{4\}\\times\\mathbb\{Z\}\_\{4\}withnϕ≤5n\_\{\\phi\}\\leq 5flavons, \(ii\)A4×ℤNA\_\{4\}\\times\\mathbb\{Z\}\_\{N\}whereN∈\[2,10\]N\\in\[2,10\]andnϕ≤5n\_\{\\phi\}\\leq 5, and \(iii\)T19×ℤ4T\_\{19\}\\times\\mathbb\{Z\}\_\{4\}withnϕ≤6n\_\{\\phi\}\\leq 6\. These spaces increase in symmetry richness and combinatorial complexity, providing progressively harder benchmarks\.

## 5Experimental Results

### 5\.1Evaluation 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\\chi^\{2\}fit to experimental observables and the number of free parametersnpn\_\{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\\chi^\{2\}\\leq 10andnp≤7n\_\{p\}\\leq 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\.2Main 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](https://arxiv.org/html/2608.20686#S4.T3), onA4×ℤNA\_\{4\}\\times\\mathbb\{Z\}\_\{N\}, CDRL achieves26\.9%26\.9\\%valid models compared to13\.79%13\.79\\%for AMBer \(a1\.95×1\.95\\timesimprovement\), and0\.19%0\.19\\%neutrino models compared to0\.03%0\.03\\%\(a6\.33×6\.33\\timesimprovement\)\. Similar gains are observed in other theory spaces, including up to1\.65×1\.65\\timesimprovements in valid model rates and up to3×3\\timesimprovements in neutrino discovery\. These gains are achieved with substantially higher sample efficiency\. As shown in Table[4](https://arxiv.org/html/2608.20686#S5.T4), CDRL discovers more neutrino models while evaluating up to4×4\\timesfewer candidates\. In combinatorial spaces exceeding102610^\{26\}possible models, these reductions correspond to substantially more efficient exploration\. The mechanism behind these gains is concrete: Figure[1](https://arxiv.org/html/2608.20686#S1.F1)traces how a single certificate blocks an entire class of candidates before any physics is run, and Figure[5](https://arxiv.org/html/2608.20686#S5.F5)shows an example rule recovered from the search itself \(full analysis in Section[5\.4](https://arxiv.org/html/2608.20686#S5.SS4)\)\.

Table 4:Search Efficiency Comparison\.CDRL discovers more neutrino models while evaluating significantly fewer candidates \(up to4×4\\timesfewer\) across all theory spaces, demonstrating substantially improved sample efficiency over AMBer and random search\.SpaceMethodModels evaluatedNeutrino models foundA4×ℤ4A\_\{4\}\\times\\mathbb\{Z\}\_\{4\}Random4,000,00028AMBer4,000,000683CDRL1,000,0001090A4×ℤNA\_\{4\}\\times\\mathbb\{Z\}\_\{N\}Random4,000,00021AMBer4,000,0001394CDRL1,000,0002343T19×ℤ4T\_\{19\}\\times\\mathbb\{Z\}\_\{4\}Random24,000,000409AMBer24,000,0006439CDRL6,000,0007019##### Importance of certificate\-driven pruning\.

The additional baselines \(implementation details in Appendix[B\.3](https://arxiv.org/html/2608.20686#A2.SS3)\) 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\. OnA4×ℤNA\_\{4\}\\times\\mathbb\{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](https://arxiv.org/html/2608.20686#S5.T5)\) 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](https://arxiv.org/html/2608.20686#S5.F3)shows the clearest evidence of this: CDRL discovers viable models spread across a substantially broader range ofℤN\\mathbb\{Z\}\_\{N\}symmetry groups than AMBer, which concentrates around a few specific values ofNN\. 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ℤN\\mathbb\{Z\}\_\{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](https://arxiv.org/html/2608.20686#S4.T2)\) instead prevents a redundant representative from being explored and counted a second time under a differentNN\. Figure[4](https://arxiv.org/html/2608.20686#S5.F4)shows where CDRL’s models concentrate in\(χ2,np\)\(\\chi^\{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 theT19×ℤ4T\_\{19\}\\times\\mathbb\{Z\}\_\{4\}space \(Table[1](https://arxiv.org/html/2608.20686#S1.T1)\)\. The neutrino models discovered by CDRL do not exactly match any of those found by AMBer\. Combined with the broaderℤN\\mathbb\{Z\}\_\{N\}coverage in Figure[3](https://arxiv.org/html/2608.20686#S5.F3), 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](https://arxiv.org/html/2608.20686#bib.bib37), we can look more closely at why these distributions differ\. For the distribution of models shown in Figure[4](https://arxiv.org/html/2608.20686#S5.F4), CDRL reaches neutrino models with the smallest parameter counts observed for either method \(Table[3](https://arxiv.org/html/2608.20686#S4.T3)reports this as Min Params\) while maintaining competitive or lowerχ2\\chi^\{2\}values\. For theℤN\\mathbb\{Z\}\_\{N\}distribution of Figure[3](https://arxiv.org/html/2608.20686#S5.F3), AMBer concentrates its discoveries around specific symmetry groups \(e\.g\.,N=5N=5\), whereas CDRL spreads more uniformly across the availableℤN\\mathbb\{Z\}\_\{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ℤN\\mathbb\{Z\}\_\{N\}regions AMBer rarely reaches\. CDRL’s reward contains no term that rewards higher\-orderℤN\\mathbb\{Z\}\_\{N\}symmetries \(Section[4\.4](https://arxiv.org/html/2608.20686#S4.SS4)gives the full reward, which depends only onχ2\\chi^\{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](https://arxiv.org/html/2608.20686#bib.bib37)\. 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](https://arxiv.org/html/2608.20686#S5)\), which scores both methods identically\.

![Refer to caption](https://arxiv.org/html/2608.20686v1/ZN_diversity.png)Figure 3:Distribution of successfully discovered neutrino models acrossℤN\\mathbb\{Z\}\_\{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 ofNN\.![Refer to caption](https://arxiv.org/html/2608.20686v1/Heatplot.png)Figure 4:Distribution of discovered models overχ2\\chi^\{2\}\(fit quality\) andnpn\_\{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\\chi^\{2\}differences at very low values do not indicate meaningfully different fit quality, so Table[3](https://arxiv.org/html/2608.20686#S4.T3)and Table[5](https://arxiv.org/html/2608.20686#S5.T5)remain the primary quantitative comparison, with this figure illustrating where in\(χ2,np\)\(\\chi^\{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\.3Ablation 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](https://arxiv.org/html/2608.20686#S5.T5)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 from26\.9%26\.9\\%to16\.2%16\.2\\%and neutrino discovery from0\.19%0\.19\\%to0\.03%0\.03\\%onA4×ℤNA\_\{4\}\\times\\mathbb\{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 / AblationDescriptionA4×ℤ4A\_\{4\}\\times\\mathbb\{Z\}\_\{4\}A4×ℤNA\_\{4\}\\times\\mathbb\{Z\}\_\{N\}T19×ℤ4T\_\{19\}\\times\\mathbb\{Z\}\_\{4\}Valid \(%\)Neutrino \(%\)Min ParamsValid \(%\)Neutrino \(%\)Min ParamsValid \(%\)Neutrino \(%\)Min ParamsCDRL \(Full\)DNN \+ MCTS \+ symbolic certificates \+ portfolio28\.1±\\pm3\.30\.10±\\pm0\.01526\.9±\\pm3\.70\.19±\\pm0\.05518\.2±\\pm2\.10\.09±\\pm0\.024No DNNNo policy/value network10\.2±\\pm5\.10\.00±\\pm0\.0099\.8±\\pm4\.60\.00±\\pm0\.00101\.1±\\pm1\.00\.00±\\pm0\.007No MCTSNo planning5\.1±\\pm8\.40\.00±\\pm0\.00134\.5±\\pm9\.00\.00±\\pm0\.0092\.2±\\pm3\.60\.01±\\pm0\.007No symbolicNo certificate14\.9±\\pm3\.10\.01±\\pm0\.02716\.2±\\pm2\.10\.03±\\pm0\.0175\.4±\\pm4\.90\.04±\\pm0\.025No portfolioNo clause/replay shared26\.9±\\pm6\.50\.04±\\pm0\.02625\.1±\\pm7\.20\.10±\\pm0\.09512\.1±\\pm7\.80\.06±\\pm0\.045

### 5\.4Search 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 theE2E\_\{2\}’sℤ4\\mathbb\{Z\}\_\{4\}charge inA4×ℤ4A\_\{4\}\\times\\mathbb\{Z\}\_\{4\}\. Among high\-confidence states, this decision tree predicts theE2E\_\{2\}’sℤ4\\mathbb\{Z\}\_\{4\}charge fromE1E\_\{1\}’sℤ4\\mathbb\{Z\}\_\{4\}charge\. This demonstrates how CDRL has learned to match theℤ4\\mathbb\{Z\}\_\{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ℤ4\\mathbb\{Z\}\_\{4\}charge value of 4\)\.Right:Determination of theHuH\_\{u\}’sA4A\_\{4\}representation inA4×ℤNA\_\{4\}\\times\\mathbb\{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](https://arxiv.org/html/2608.20686#A3)\.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](https://arxiv.org/html/2608.20686#bib.bib66)\. 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](https://arxiv.org/html/2608.20686#S5.F6), incorporating these rules consistently increases the number of discovered models in all three theory spaces\. InA4×ℤ4A\_\{4\}\\times\\mathbb\{Z\}\_\{4\}andT19×ℤ4T\_\{19\}\\times\\mathbb\{Z\}\_\{4\}, rule\-guided runs achieve∼2×\\sim\\\!2\\timeshigher valid model rates and22–3×3\\timeshigher neutrino model discovery, while inA4×ℤNA\_\{4\}\\times\\mathbb\{Z\}\_\{N\}we observe∼1\.5×\\sim\\\!1\.5\\timesimprovements in validity and up to3×3\\timesin neutrino discovery\.

We describe the procedure used to extract soft constraints from MCTS trajectories in Algorithm[2](https://arxiv.org/html/2608.20686#alg2)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 than95%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](https://arxiv.org/html/2608.20686#A2)\. Because blocks are assigned in a fixed top\-down order \(Section[4](https://arxiv.org/html/2608.20686#S4)\), only blocks assigned earlier in that order are available as features\. We extract these high\-confidence root\-to\-leaf paths as rules of the formconditions→a\\text\{conditions\}\\rightarrow 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 vectorr⁡\(s\)r\(s\), and reweight the neural policy asP~​\(a∣s\)∝P⁡\(a∣s\)​\(1\+β​ra​\(s\)\)\\tilde\{P\}\(a\\mid s\)\\propto P\(a\\mid s\)\\,\(1\+\\beta\\,r\_\{a\}\(s\)\), whereβ=0\.5\\beta=0\.5in 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 2Soft Constraint Extraction and Policy Reweighting1:MCTS traces

𝒟\\mathcal\{D\}, progress buckets

ℬ\\mathcal\{B\}
2:Minimum samples

mm, tree hyperparameters

\(d,s,ℓ\)\(d,s,\\ell\)
3:Soft bias strength

β\\beta
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

\{𝒟b\}b∈ℬ\\\{\\mathcal\{D\}\_\{b\}\\\}\_\{b\\in\\mathcal\{B\}\}based on progress

7:foreach bucket

b∈ℬb\\in\\mathcal\{B\}do

8:if

\|𝒟b\|<m\|\\mathcal\{D\}\_\{b\}\|<mthen

9:continue

10:endif

11:Train decision tree

TbT\_\{b\}with depth

dd, split

ss, leaf size

ℓ\\ell
12:Extract leaf paths corresponding to high\-confidence predictions

13:Convert each path into a rule

\(conditions→a\)\(\\text\{conditions\}\\rightarrow a\)
14:Store rules with support and purity

15:endfor

16:Build rule table indexed by progress and decision block

17:

18:Policy Reweighting during MCTS:

19:Given state

ss, compute neural policy

P\(⋅∣s\)P\(\\cdot\\mid s\)
20:Identify rules satisfied by

ssand compute bias vector

r⁡\(s\)r\(s\)
21:Reweight policy:

P~​\(a∣s\)∝P⁡\(a∣s\)​\(1\+β​ra​\(s\)\)\\tilde\{P\}\(a\\mid s\)\\propto P\(a\\mid s\)\\,\(1\+\\beta\\,r\_\{a\}\(s\)\)
22:Apply legality mask and renormalize

P~\\tilde\{P\}

![Refer to caption](https://arxiv.org/html/2608.20686v1/KD.png)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 onA4×ℤ4A\_\{4\}\\times\\mathbb\{Z\}\_\{4\},A4×ℤNA\_\{4\}\\times\\mathbb\{Z\}\_\{N\}, andT19×ℤ4T\_\{19\}\\times\\mathbb\{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 roughly1\.51\.5–2×2\\timesin valid models and22–3×3\\timesin 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](https://arxiv.org/html/2608.20686#S4.T3)\.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\}influencingE2,E3E\_\{2\},E\_\{3\}through identical or systematically shiftedℤ4\\mathbb\{Z\}\_\{4\}charges\)\. We also observe coordinated triplet assignments acrossLL,NN, andϕ\\phi, mirroring common design patterns used by human model builders[23](https://arxiv.org/html/2608.20686#bib.bib50)\. Although extracted post\-hoc, these rules provide reusable and generalizable structure\. The full set of 40 rules is listed in Section[C](https://arxiv.org/html/2608.20686#A3)\.

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ℤN\\mathbb\{Z\}\_\{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\.

## 6Conclusion, 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×\\timeshigher valid model rates and 6\.33×\\timeshigher neutrino model discovery than AMBer\. Separately, reaching a comparable number of neutrino models requires up to 4×\\timesfewer physics evaluations \(Table[4](https://arxiv.org/html/2608.20686#S5.T4)\)\. 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

- Abramsonet 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\.Nature630\(8016\),pp\. 493–500\.Cited by:[§1](https://arxiv.org/html/2608.20686#S1.p1.1),[§1](https://arxiv.org/html/2608.20686#S1.p10.1),[§2](https://arxiv.org/html/2608.20686#S2.p4.1)\.
- Acharyaet al\.\(2023\)K\. Acharya, W\. Raza, C\. Dourado, A\. Velasquez, and H\. H\. SongNeurosymbolic reinforcement learning and planning: a survey\.IEEE Transactions on Artificial Intelligence\.Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p6.1)\.
- Agrawalet al\.\(2024\)L\. A\. Agrawal, A\. Kanade, N\. Goyal, S\. Lahiri, and S\. RajamaniMonitor\-guided decoding of code LMs with static analysis of repository context\.Advances in Neural Information Processing Systems36\.Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p7.1)\.
- Ahmadet al\.\(2002\)Q\. R\. Ahmadet al\.Direct evidence for neutrino flavor transformation from neutral current interactions in the Sudbury Neutrino Observatory\.Phys\. Rev\. Lett\.89,pp\. 011301\.External Links:nucl\-ex/0204008,[Document](https://dx.doi.org/10.1103/PhysRevLett.89.011301)Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p1.1)\.
- Ahnet al\.\(2003\)M\. H\. Ahnet al\.Indications of neutrino oscillation in a 250 km long baseline experiment\.Phys\. Rev\. Lett\.90,pp\. 041801\.External Links:hep\-ex/0212007,[Document](https://dx.doi.org/10.1103/PhysRevLett.90.041801)Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p1.1)\.
- Alexanderet al\.\(2026\)S\. Alexander, B\. Bradley, L\. Gouskos, and C\. NiuAutonomous Discovery of Particle Physics Theories from Experimental Data\.External Links:2603\.28935Cited by:[§1](https://arxiv.org/html/2608.20686#S1.p5.1)\.
- Almuminet al\.\(2023\)Y\. Almumin, M\. Chen, M\. Cheng, V\. Knapp\-Perez, Y\. Li, A\. Mondol, S\. Ramos\-Sanchez, M\. Ratz, and S\. ShuklaNeutrino Flavor Model Building and the Origins of Flavor and CP Violation\.Universe9\(12\),pp\. 512\.External Links:2204\.08668,[Document](https://dx.doi.org/10.3390/universe9120512)Cited by:[§1](https://arxiv.org/html/2608.20686#S1.p1.1)\.
- Altmannshofer and Greljo \(2025\)W\. Altmannshofer and A\. GreljoRecent Progress in Flavor Model Building\.Ann\. Rev\. Nucl\. Part\. Sci\.75\(1\),pp\. 201–322\.External Links:2412\.04549,[Document](https://dx.doi.org/10.1146/annurev-nucl-121423-100950)Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p1.1)\.
- Babu \(2010\)K\. S\. BabuTASI Lectures on Flavor Physics\.InTheoretical Advanced Study Institute in Elementary Particle Physics: The Dawn of the LHC Era,pp\. 49–123\.External Links:0910\.2948,[Document](https://dx.doi.org/10.1142/9789812838360%5F0002)Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p1.1)\.
- Bai and Zhang \(2025\)X\. Bai and X\. ZhangArtificial intelligence\-powered materials science\.Nano\-micro letters17\(1\),pp\. 135\.Cited by:[§1](https://arxiv.org/html/2608.20686#S1.p1.1)\.
- Balyoet al\.\(2015\)T\. Balyo, P\. Sanders, and C\. SinzHordesat: a massively parallel portfolio sat solver\.InInternational Conference on Theory and Applications of Satisfiability Testing,pp\. 156–172\.Cited by:[§4\.7](https://arxiv.org/html/2608.20686#S4.SS7.p2.1)\.
- Baretzet al\.\(2025\)J\. B\. Baretz, M\. Fieg, V\. Ganesh, A\. Ghosh, V\. Knapp\-Perez, J\. Rudolph, and D\. WhitesonTowards ai\-assisted neutrino flavor theory design\.arXiv preprint arXiv:2506\.08080\.Cited by:[§B\.3](https://arxiv.org/html/2608.20686#A2.SS3.p1.1),[§1](https://arxiv.org/html/2608.20686#S1.p1.1),[§1](https://arxiv.org/html/2608.20686#S1.p10.1),[§1](https://arxiv.org/html/2608.20686#S1.p5.1),[§2](https://arxiv.org/html/2608.20686#S2.p3.1),[§4\.1](https://arxiv.org/html/2608.20686#S4.SS1.p1.1),[§4\.4](https://arxiv.org/html/2608.20686#S4.SS4.p1.1),[§4\.8](https://arxiv.org/html/2608.20686#S4.SS8.p1.1),[Table 3](https://arxiv.org/html/2608.20686#S4.T3.6.1.1.1.1.1.1.12.1),[§5\.2](https://arxiv.org/html/2608.20686#S5.SS2.SSS0.Px2.p2.1),[footnote 2](https://arxiv.org/html/2608.20686#footnote2)\.
- Bastaniet al\.\(2018\)O\. Bastani, Y\. Pu, and A\. Solar\-LezamaVerifiable reinforcement learning via policy extraction\.Advances in neural information processing systems31\.Cited by:[§5\.4](https://arxiv.org/html/2608.20686#S5.SS4.p1.1)\.
- Bellemareet al\.\(2020\)M\. G\. Bellemare, S\. Candido, P\. S\. Castro, J\. Gong, M\. C\. Machado, S\. Moitra, S\. S\. Ponda, and Z\. WangAutonomous navigation of stratospheric balloons using reinforcement learning\.Nature588\(7836\),pp\. 77–82\.Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p5.1)\.
- Biereet al\.\(2009\)A\. Biere, H\. van Maaren, and T\. WalshHandbook of satisfiability\.SAGE Publications Limited\.Cited by:[§1](https://arxiv.org/html/2608.20686#S1.p7.1),[§1](https://arxiv.org/html/2608.20686#S1.p8.1),[§1](https://arxiv.org/html/2608.20686#S1.p9.1),[§4\.3](https://arxiv.org/html/2608.20686#S4.SS3.p3.1)\.
- Cartaet al\.\(2025\)F\. Carta, A\. Gauntlett, F\. Griffin, and Y\. HeBPS spectroscopy with reinforcement learning\.\.External Links:2501\.14863Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p3.1)\.
- Chenet al\.\(2020\)Y\. Chen, C\. Wang, O\. Bastani, I\. Dillig, and Y\. FengProgram synthesis using deduction\-guided reinforcement learning\.InInternational Conference on Computer Aided Verification,pp\. 587–610\.Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p7.1)\.
- Clevelandet al\.\(1998\)B\. T\. Cleveland, T\. Daily, R\. Davis, J\. R\. Distel, K\. Lande, C\. K\. Lee, P\. S\. Wildenhain, and J\. UllmanMeasurement of the solar electron neutrino flux with the Homestake chlorine detector\.Astrophys\. J\.496,pp\. 505–526\.External Links:[Document](https://dx.doi.org/10.1086/305343)Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p1.1)\.
- Colelough and Regli \(2025\)B\. C\. Colelough and W\. RegliNeuro\-symbolic ai in 2024: a systematic review\.arXiv preprint arXiv:2501\.05435\.Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p6.1)\.
- Daviset al\.\(1962\)M\. Davis, G\. Logemann, and D\. LovelandA machine program for theorem\-proving\.Communications of the ACM5\(7\),pp\. 394–397\.Cited by:[§1](https://arxiv.org/html/2608.20686#S1.p8.1),[§1](https://arxiv.org/html/2608.20686#S1.p9.1),[§4\.3](https://arxiv.org/html/2608.20686#S4.SS3.p3.1)\.
- de Gouvêaet 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\-LoudTheory of neutrino physics – snowmass tf11 \(aka nf08\) topical group report\.External Links:2209\.07983,[Link](https://arxiv.org/abs/2209.07983)Cited by:[§1](https://arxiv.org/html/2608.20686#S1.p1.1)\.
- Degraveet 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\.Nature602\(7897\),pp\. 414–419\.Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p5.1)\.
- Ding and Meloni \(2012\)G\. Ding and D\. MeloniA Model for Tri\-bimaximal Mixing from a Completely BrokenA4A\_\{4\}\.Nucl\. Phys\. B855,pp\. 21–45\.External Links:1108\.2733,[Document](https://dx.doi.org/10.1016/j.nuclphysb.2011.10.001)Cited by:[§5\.4](https://arxiv.org/html/2608.20686#S5.SS4.p3.1)\.
- Estebanet al\.\(2020\)I\. Esteban, M\. C\. Gonzalez\-Garcia, M\. Maltoni, T\. Schwetz, and A\. ZhouThe fate of hints: updated global analysis of three\-flavor neutrino oscillations\.JHEP09,pp\. 178\.External Links:2007\.14792,[Document](https://dx.doi.org/10.1007/JHEP09%282020%29178)Cited by:[§4\.4](https://arxiv.org/html/2608.20686#S4.SS4.p1.1)\.
- Fawziet 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\.Nature610\(7930\),pp\. 47–53\.Cited by:[§1](https://arxiv.org/html/2608.20686#S1.p10.1),[§2](https://arxiv.org/html/2608.20686#S2.p5.1)\.
- Feruglio and Romanino \(2021\)F\. Feruglio and A\. RomaninoLepton flavour symmetries\.External Links:1912\.06028,[Link](https://arxiv.org/abs/1912.06028)Cited by:[§1](https://arxiv.org/html/2608.20686#S1.p1.1),[§2](https://arxiv.org/html/2608.20686#S2.p1.1)\.
- Fukudaet al\.\(1998\)Y\. Fukudaet al\.Evidence for oscillation of atmospheric neutrinos\.Phys\. Rev\. Lett\.81,pp\. 1562–1567\.External Links:hep\-ex/9807003,[Document](https://dx.doi.org/10.1103/PhysRevLett.81.1562)Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p1.1)\.
- Gell\-Mannet al\.\(1979\)M\. Gell\-Mann, P\. Ramond, and R\. SlanskyComplex Spinors and Unified Theories\.Conf\. Proc\. C790927,pp\. 315–321\.External Links:1306\.4669Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p2.1)\.
- Giarnetti and Meloni \(2026\)A\. Giarnetti and D\. MeloniReinforcement Learning Techniques for the Flavor Problem in Particle Physics\.Symmetry18\(1\),pp\. 131\.External Links:2510\.25495,[Document](https://dx.doi.org/10.3390/sym18010131)Cited by:[§1](https://arxiv.org/html/2608.20686#S1.p5.1)\.
- Glashow \(1980\)S\. L\. GlashowThe Future of Elementary Particle Physics\.NATO Sci\. Ser\. B61,pp\. 687\.External Links:[Document](https://dx.doi.org/10.1007/978-1-4684-7197-7%5F15)Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p2.1)\.
- Gowet al\.\(2022\)S\. Gow, M\. Niranjan, S\. Kanza, and J\. G\. FreyA review of reinforcement learning in chemistry\.Digital Discovery1\(5\),pp\. 551–567\.Cited by:[§1](https://arxiv.org/html/2608.20686#S1.p2.1)\.
- Guoet 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](https://arxiv.org/html/2608.20686#S2.p7.1)\.
- Halversonet al\.\(2019\)J\. Halverson, B\. Nelson, and F\. RuehleBranes with brains: exploring string vacua with deep reinforcement learning\.Journal of High Energy Physics2019\(6\)\.External Links:ISSN 1029\-8479,[Link](http://dx.doi.org/10.1007/JHEP06(2019)003),[Document](https://dx.doi.org/10.1007/jhep06%282019%29003)Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p3.1)\.
- Harvey and Lukas \(2021\)T\. R\. Harvey and A\. LukasQuark Mass Models and Reinforcement Learning\.JHEP08,pp\. 161\.External Links:2103\.04759,[Document](https://dx.doi.org/10.1007/JHEP08%282021%29161)Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p3.1)\.
- Hitzleret al\.\(2023\)P\. Hitzler, M\. K\. Sarker, and A\. EberhartCompendium of neurosymbolic artificial intelligence\.Vol\.369,IOS Press\.Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p6.1)\.
- Horganet al\.\(2018\)D\. Horgan, J\. Quan, D\. Budden, G\. Barth\-Maron, M\. Hessel, H\. van Hasselt, and D\. SilverDistributed prioritized experience replay\. corr abs/1803\.00933 \(2018\)\.arXiv preprint arXiv:1803\.00933\.Cited by:[§4\.7](https://arxiv.org/html/2608.20686#S4.SS7.p2.1)\.
- Ignatievet al\.\(2018\)A\. Ignatiev, A\. Morgado, and J\. Marques\-SilvaPySAT: A Python toolkit for prototyping with SAT oracles\.InSAT,pp\. 428–437\.External Links:[Link](https://doi.org/10.1007/978-3-319-94144-8_26),[Document](https://dx.doi.org/10.1007/978-3-319-94144-8%5F26)Cited by:[§B\.2](https://arxiv.org/html/2608.20686#A2.SS2.p1.1)\.
- Janaet al\.\(2023\)P\. Jana, P\. Jha, H\. Ju, G\. Kishore, A\. Mahajan, and V\. GaneshCoTran: an llm\-based code translator using reinforcement learning with feedback from compiler and symbolic execution\.arXiv preprint arXiv:2306\.06755\.Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p7.1)\.
- Jhaet al\.\(2025\)P\. Jha, P\. Jana, P\. Suresh, A\. Arora, and V\. GaneshRLSF: fine\-tuning LLMs via symbolic feedback\.28th European Conference on Artificial Intelligence\.Cited by:[§1](https://arxiv.org/html/2608.20686#S1.p2.1),[§2](https://arxiv.org/html/2608.20686#S2.p7.1)\.
- Jhaet al\.\(2010\)S\. Jha, S\. Gulwani, S\. A\. Seshia, and A\. TiwariOracle\-guided component\-based program synthesis\.InProceedings of the 32nd ACM/IEEE International Conference on Software Engineering\-Volume 1,pp\. 215–224\.Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p7.1)\.
- Jha and Seshia \(2017\)S\. Jha and S\. A\. SeshiaA theory of formal synthesis via inductive learning\.Acta Informatica54\(7\),pp\. 693–726\.Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p7.1)\.
- Jumperet 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\.nature596\(7873\),pp\. 583–589\.Cited by:[§1](https://arxiv.org/html/2608.20686#S1.p1.1)\.
- Kambhampatiet al\.\(2024\)S\. Kambhampati, K\. Valmeekam, L\. Guan, K\. Stechly, M\. Verma, S\. Bhambri, L\. Saldyt, and A\. MurthyLLMs can’t plan, but can help planning in llm\-modulo frameworks\.arXiv preprint arXiv:2402\.01817\.Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p7.1)\.
- Karagiorgiet al\.\(2022\)G\. Karagiorgi, G\. Kasieczka, S\. Kravitz, B\. Nachman, and D\. ShihMachine learning in the search for new fundamental physics\.Nature Reviews Physics4\(6\),pp\. 399–412\.Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p4.1)\.
- King \(2015\)S\. F\. KingModels of Neutrino Mass, Mixing and CP Violation\.J\. Phys\. G42,pp\. 123001\.External Links:1510\.02091,[Document](https://dx.doi.org/10.1088/0954-3899/42/12/123001)Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p1.1)\.
- Liet al\.\(2024\)Z\. Li, J\. Sun, L\. Murphy, Q\. Su, Z\. Li, X\. Zhang, K\. Yang, and X\. SiA survey on deep learning for theorem proving\.arXiv preprint arXiv:2404\.09939\.Cited by:[§1](https://arxiv.org/html/2608.20686#S1.p2.1)\.
- Lianget al\.\(2016\)J\. H\. Liang, V\. Ganesh, P\. Poupart, and K\. CzarneckiLearning rate based branching heuristic for sat solvers\.InTheory and Applications of Satisfiability Testing–SAT 2016: 19th International Conference, Bordeaux, France, July 5\-8, 2016, Proceedings 19,pp\. 123–140\.Cited by:[§B\.3](https://arxiv.org/html/2608.20686#A2.SS3.p2.1),[§2](https://arxiv.org/html/2608.20686#S2.p7.1),[Table 3](https://arxiv.org/html/2608.20686#S4.T3.6.1.1.1.1.1.1.10.1)\.
- Liuet al\.\(2023\)Y\. Liu, Z\. Yang, Z\. Yu, Z\. Liu, D\. Liu, H\. Lin, M\. Li, S\. Ma, M\. Avdeev, and S\. ShiGenerative artificial intelligence and its applications in materials science: current situation and future perspectives\.Journal of Materiomics9\(4\),pp\. 798–816\.Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p4.1)\.
- Mankowitzet 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\.Nature618\(7964\),pp\. 257–263\.Cited by:[§1](https://arxiv.org/html/2608.20686#S1.p1.1),[§1](https://arxiv.org/html/2608.20686#S1.p10.1),[§2](https://arxiv.org/html/2608.20686#S2.p5.1)\.
- Martín\-Guerrero and Lamata \(2021\)J\. D\. Martín\-Guerrero and L\. LamataReinforcement learning and physics\.Applied Sciences11\(18\),pp\. 8589\.Cited by:[§1](https://arxiv.org/html/2608.20686#S1.p2.1)\.
- Melnikovet al\.\(2018\)A\. A\. Melnikov, H\. Poulsen Nautrup, M\. Krenn, V\. Dunjko, M\. Tiersch, A\. Zeilinger, and H\. J\. BriegelActive learning machine learns to create new quantum experiments\.Proceedings of the National Academy of Sciences115\(6\),pp\. 1221–1226\.Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p5.1)\.
- Menouer and Baarir \(2017\)T\. Menouer and S\. BaarirParallel learning portfolio\-based solvers\.Procedia Computer Science108,pp\. 335–344\.Cited by:[§4\.7](https://arxiv.org/html/2608.20686#S4.SS7.p2.1)\.
- Merchantet al\.\(2023\)A\. Merchant, S\. Batzner, S\. S\. Schoenholz, M\. Aykol, G\. Cheon, and E\. D\. CubukScaling deep learning for materials discovery\.Nature624\(7990\),pp\. 80–85\.Cited by:[§1](https://arxiv.org/html/2608.20686#S1.p1.1),[§2](https://arxiv.org/html/2608.20686#S2.p4.1)\.
- Messeri and Crockett \(2024\)L\. Messeri and M\. J\. CrockettArtificial intelligence and illusions of understanding in scientific research\.Nature627\(8002\),pp\. 49–58\.Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p4.1)\.
- Minkowski \(1977\)P\. Minkowskiμ→e​γ\\mu\\to e\\gammaat a Rate of One Out of10910^\{9\}Muon Decays?\.Phys\. Lett\. B67,pp\. 421–428\.External Links:[Document](https://dx.doi.org/10.1016/0370-2693%2877%2990435-X)Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p2.1)\.
- Nishimuraet al\.\(2020\)S\. Nishimura, C\. Miyao, and H\. OtsukaExploring the flavor structure of quarks and leptons with reinforcement learning\.JHEP23,pp\. 021\.External Links:2304\.14176,[Document](https://dx.doi.org/10.1007/JHEP12%282023%29021)Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p3.1)\.
- Nishimuraet al\.\(2024\)S\. Nishimura, C\. Miyao, and H\. OtsukaReinforcement learning\-based statistical search strategy for an axion model from flavor\.\.External Links:2409\.10023Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p3.1)\.
- Polgreenet al\.\(2022\)E\. Polgreen, A\. Reynolds, and S\. A\. SeshiaSatisfiability and synthesis modulo oracles\.InInternational Conference on Verification, Model Checking, and Abstract Interpretation,pp\. 263–284\.Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p7.1)\.
- Rosin \(2011\)C\. D\. RosinMulti\-armed bandits with episode context\.Annals of Mathematics and Artificial Intelligence61\(3\),pp\. 203–230\.Cited by:[§4\.7](https://arxiv.org/html/2608.20686#S4.SS7.p1.1)\.
- Ruizet 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 Intelligence7\(3\),pp\. 374–385\.Cited by:[§1](https://arxiv.org/html/2608.20686#S1.p10.1),[§2](https://arxiv.org/html/2608.20686#S2.p5.1)\.
- Segleret al\.\(2018\)M\. H\. Segler, M\. Preuss, and M\. P\. WallerPlanning chemical syntheses with deep neural networks and symbolic ai\.Nature555\(7698\),pp\. 604–610\.Cited by:[§1](https://arxiv.org/html/2608.20686#S1.p1.1)\.
- Silveret 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\.Nature529\(7587\),pp\. 484–489\.Cited by:[§B\.3](https://arxiv.org/html/2608.20686#A2.SS3.p2.1),[Figure 1](https://arxiv.org/html/2608.20686#S1.F1),[Figure 1](https://arxiv.org/html/2608.20686#S1.F1.5.1),[§1](https://arxiv.org/html/2608.20686#S1.p8.1),[§1](https://arxiv.org/html/2608.20686#S1.p9.1),[§4\.7](https://arxiv.org/html/2608.20686#S4.SS7.p1.1),[Table 3](https://arxiv.org/html/2608.20686#S4.T3.6.1.1.1.1.1.1.7.1)\.
- Silveret 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\. HassabisMastering the game of Go without human knowledge\.Nature550\(7676\),pp\. 354–359\.External Links:ISSN 1476\-4687,[Document](https://dx.doi.org/10.1038/nature24270),[Link](https://doi.org/10.1038/nature24270)Cited by:[Figure 1](https://arxiv.org/html/2608.20686#S1.F1),[Figure 1](https://arxiv.org/html/2608.20686#S1.F1.5.1),[§1](https://arxiv.org/html/2608.20686#S1.p8.1),[§1](https://arxiv.org/html/2608.20686#S1.p9.1),[§4\.7](https://arxiv.org/html/2608.20686#S4.SS7.p1.1)\.
- Singhet 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](https://arxiv.org/html/2608.20686#A2.SS3.SSS1.p1.1),[Table 3](https://arxiv.org/html/2608.20686#S4.T3.6.1.1.1.1.1.1.5.1)\.
- Sutton and Barto \(2018\)R\. S\. Sutton and A\. G\. BartoReinforcement learning: an introduction\.A Bradford Book,Cambridge, MA, USA\.External Links:ISBN 0262039249Cited by:[§1](https://arxiv.org/html/2608.20686#S1.p2.1)\.
- Van Noorden and Perkel \(2023\)R\. Van Noorden and J\. M\. PerkelAI and science: what 1,600 researchers think\.Nature621\(7980\),pp\. 672–675\.Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p4.1)\.
- Wanget 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\.Nature620\(7972\),pp\. 47–60\.Cited by:[§1](https://arxiv.org/html/2608.20686#S1.p2.1),[§2](https://arxiv.org/html/2608.20686#S2.p4.1)\.
- Wojciket al\.\(2025\)G\. N\. Wojcik, S\. T\. Eu, and L\. L\. EverettGraph reinforcement learning for exploring model spaces beyond the standard model\.Phys\. Rev\. D111\(3\),pp\. 035007\.External Links:2407\.07203,[Document](https://dx.doi.org/10.1103/PhysRevD.111.035007)Cited by:[§1](https://arxiv.org/html/2608.20686#S1.p5.1)\.
- Xuet 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 innovation2\(4\)\.Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p4.1)\.
- Yanagida \(1979\)T\. YanagidaHorizontal gauge symmetry and masses of neutrinos\.Conf\. Proc\. C7902131,pp\. 95–99\.Cited by:[§2](https://arxiv.org/html/2608.20686#S2.p2.1)\.
- Zhang and Gu \(2025\)J\. Zhang and B\. GuAdvances in reinforcement learning for intelligent program synthesis\.In2025 5th International Conference on Neural Networks, Information and Communication Engineering \(NNICE\),pp\. 1734–1739\.Cited by:[§1](https://arxiv.org/html/2608.20686#S1.p2.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ℤN\\mathbb\{Z\}\_\{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=6\\mathbb\{Z\}\_\{N\}=6and descends, and the same red×\\timesmasking 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ℤN\\mathbb\{Z\}\_\{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=4\\mathbb\{Z\}\_\{N\}=4branch, 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 AThe CDRL Loop: A Step\-by\-Step Walkthrough

Figure[7](https://arxiv.org/html/2608.20686#A0.F7)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](https://arxiv.org/html/2608.20686#S1.F1)\(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ℤN\\mathbb\{Z\}\_\{N\}choice, then each particle’s representation, then its charge, and so on\)\. What Figure[7](https://arxiv.org/html/2608.20686#A0.F7)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](https://arxiv.org/html/2608.20686#alg1), 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ℤN\\mathbb\{Z\}\_\{N\}choices at the root are an illustrative subset of the nine allowed in this theory space \(N∈\{2,…,10\}N\\in\\\{2,\\dots,10\\\}\)\.

## Appendix BAdditional Experimental Details

### B\.1Compute 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\.2Additional 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](https://arxiv.org/html/2608.20686#bib.bib5)\.

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](https://arxiv.org/html/2608.20686#S5.SS4)\), we treat an MCTS decision as high\-confidence when the dominant action receives more than95%95\\%of visits and has a positive value estimate\. Progress buckets require at least1010such samples; each decision tree has maximum depth33, requires at least1010samples to split a node and55samples per leaf, and is fit with an 80/20 train\-test split when enough data is available\.

### B\.3Baselines

We compare againstAMBer\(Autonomous Model Builder\)[12](https://arxiv.org/html/2608.20686#bib.bib37), an RL framework for neutrino flavor model discovery\. AMBer performs iterative model refinement using scalar rewards derived from the physics evaluation pipeline, includingχ2\\chi^\{2\}fit quality, the number of free parameters, and a bonus for exploring higher\-orderℤN\\mathbb\{Z\}\_\{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](https://arxiv.org/html/2608.20686#bib.bib65), and a DNN\+MCTS framework[62](https://arxiv.org/html/2608.20686#bib.bib9)\. These baselines isolate the contributions of planning, neural guidance, and symbolic reasoning\.

#### B\.3\.1LLM Baseline Details

We evaluate a prompting\-based baseline using GPT\-5\.3[64](https://arxiv.org/html/2608.20686#bib.bib68)\. 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, \(ii\) formatting instructions specifying the matrix structure and allowed assignments, and \(iii\) 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\.4Neural 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 bytanh\\tanh

### B\.5Additional Training Details

We provide the concrete hyperparameters for the MCTS and network training described in Section[4](https://arxiv.org/html/2608.20686#S4)\. We use:

- •Max iterations: 30
- •Episodes per iteration: 100
- •MCTS simulations per move: 150
- •MCTScpuctc\_\{\\text\{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\.6Parallelization

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 CSearch 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](https://arxiv.org/html/2608.20686#S5.SS4)\. Each observation is a shallow decision tree that predicts one block assignment \(a representation or aℤN\\mathbb\{Z\}\_\{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](https://arxiv.org/html/2608.20686#alg2); the aggregate effect of reusing them is reported in Figure[6](https://arxiv.org/html/2608.20686#S5.F6)\.

### C\.1A4×ℤ4A\_\{4\}\\times\\mathbb\{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\_chargeTrain: 0\.917 Test: 0\.917

E1\.Z4 = 3?3E1\.Z4 = 1?12YesNoYesNo

E3\.Z4\_chargeTrain: 0\.972 Test: 0\.944

E2\.Z4 = 1?1E1\.Z4 = 4?42YesNoYesNo

N1\.Z4\_chargeTrain: 0\.911 Test: 1\.000

L2\.Z4 = 3?2E3\.Z4 = 1?24YesNoYesNo

Hd\.repTrain: 0\.615 Test: NA

E3\.rep = 1’?11’YesNo

phi1\.Z4\_chargeTrain: 0\.654 Test: 0\.429

Hu\.Z4 = 2?3Hu\.Z4 = 4?3E1\.Z4 = 1?43YesNoYesNoYesNo

phi2\.Z4\_chargeTrain: 0\.719 Test: 0\.444

Hu\.Z4 = 1?42YesNo

### C\.2A4×ℤNA\_\{4\}\\times\\mathbb\{Z\}\_\{N\}

Constant assignments

L1\.rep = 3E2\.rep = 1’N1\.rep = 3phi1\.rep = 3phi2\.rep = 3phi3\.rep = 3phi4\.rep = 3

E2\.Z5\_chargeTrain: 0\.938 Test: 0\.882

E1\.Z5 = 2?2E1\.Z5 = 1?14YesNoYesNo

E3\.repTrain: 0\.707 Test: 0\.727

E2\.rep = 1’?1”1YesNo

E3\.Z5\_chargeTrain: 0\.926 Test: 0\.968

E2\.Z5 = 4?4E1\.Z5 = 2?2E2\.Z5 = 1?15YesNoYesNoYesNo

N1\.Z5\_chargeTrain: 0\.861 Test: 0\.900

E2\.Z5 = 3?3E1\.Z5 = 2?2L3\.Z5 = 5?42YesNoYesNoYesNo

Hu\.repTrain: 0\.889 Test: 0\.600

E3\.rep = 1”?1’E3\.rep = 1?1’1”YesNoYesNo

### C\.3T19×ℤ4T\_\{19\}\\times\\mathbb\{Z\}\_\{4\}

Left edge: Yes Right edge: No

L1\.Z4\_chargeTrain: 0\.792 Test: 0\.714

4

E1\.Z4\_chargeTrain: 0\.611 Test: 0\.600

L2\.Z4 = 4?1L1\.Z4 = 1?21

E2\.repTrain: 0\.950 Test: 0\.905

E1\.rep = 1?1’1

E2\.Z4\_chargeTrain: 0\.938 Test: 0\.857

E1\.Z4 = 2?2E1\.Z4 = 1?13

E3\.repTrain: 0\.685 Test: 0\.694

E1\.rep = 1”?E2\.rep = 1”?1’1”1

E3\.Z4\_chargeTrain: 0\.924 Test: 0\.926

E1\.Z4 = 2?2E2\.Z4 = 4?4E2\.Z4 = 3?31

N1\.repTrain: 0\.960 Test: 0\.932

L2\.rep = 3\_3b?3\_33\_3b

Hu\.repTrain: 0\.522 Test: 0\.667

E3\.rep = 1?1”N3\.rep = 3\_2b?1’N1\.rep = 3\_3?1’1

Hu\.Z4\_chargeTrain: 0\.978 Test: 0\.833

4

Hd\.repTrain: 0\.821 Test: 0\.875

N3\.rep = 3\_2?1”E2\.rep = 1?1”1

phi1\.repTrain: 0\.859 Test: 0\.941

L3\.rep = 3\_3b?3\_2bE1\.rep = 1?3\_33\_3b

phi2\.repTrain: 0\.750 Test: 0\.625

N2\.rep = 3\_3?3\_2bE1\.rep = 1”?3\_2N3\.rep = 3\_2?3\_13\_3

phi3\.repTrain: 0\.741 Test: 0\.714

N1\.rep = 3\_3?3\_2b3\_1

phi5\.repTrain: 0\.857 Test: 0\.750

3\_2b