diff --git a/Zettelkasten/Fleeting Notes/Editing/thesis_ideas_notes.md b/Zettelkasten/Fleeting Notes/Editing/thesis_ideas_notes.md index 9f86c6aa9..e37ce504f 100644 --- a/Zettelkasten/Fleeting Notes/Editing/thesis_ideas_notes.md +++ b/Zettelkasten/Fleeting Notes/Editing/thesis_ideas_notes.md @@ -1,3 +1,19 @@ # Notes on [[thesis-ideas-2025-07-30]] +What needs done: +- [X] 1 needs edited and reviewed + - [X] Review outcomes. I really don't like outcome + number 1. + +- [X] Review and edit 2 + +- [ ] Review and edit 3 + - [ ] Write an impact section + +- [ ] Review and edit 4 + - [ ] Needs more goal + +- [ ] Review and edit 5 + +- [ ] Review and edit 6 diff --git a/Zettelkasten/Fleeting Notes/Journal/2025_08_07.md b/Zettelkasten/Fleeting Notes/Journal/2025_08_07.md index ccd6f9298..327de4175 100644 --- a/Zettelkasten/Fleeting Notes/Journal/2025_08_07.md +++ b/Zettelkasten/Fleeting Notes/Journal/2025_08_07.md @@ -1,7 +1,7 @@ --- --- -# 2025-08-06 +# 2025-08-07 Today I have not gotten too much done, but I did get here early today. Today, I'll sell the truck and work on Sam's car. I saw Patrick today too, which was nice. Robert's stuff diff --git a/Zettelkasten/Fleeting Notes/Journal/2025_08_10.md b/Zettelkasten/Fleeting Notes/Journal/2025_08_10.md new file mode 100644 index 000000000..8c23c2ec4 --- /dev/null +++ b/Zettelkasten/Fleeting Notes/Journal/2025_08_10.md @@ -0,0 +1,8 @@ +--- +--- + +# 2025-08-10 +Today I'm finishing the thesis ideas, for real this time. + +I'm also going to get a model of a heat exchanger working. + diff --git a/Zettelkasten/Permanent Notes/thesis-ideas.md b/Zettelkasten/Permanent Notes/thesis-ideas.md index 259fae878..80ca420b7 100644 --- a/Zettelkasten/Permanent Notes/thesis-ideas.md +++ b/Zettelkasten/Permanent Notes/thesis-ideas.md @@ -5,38 +5,49 @@ suggested I write down 6 ideas, and from them we shall figure out a possible topic idea that I can really start working on. -I used ChatGPT to do some of the heavy lifting based on the -papers I've been reading, and leveraged the 'deep research' -feature. Here are some of my favorite ideas, broken down -into goals, outcomes, impact, and related papers. - ___________________________________________________________ ## **Integrating Shielding into Nuclear Power Control** ### Goal: -The goal of this research is develop machine learning -enabled control algorithims for nuclear power applications -that incoporate shielding: a formal guarantee of adherence -to system specifications without augmenting the machine -learning process. + +The goal of this research is to use temporal logic shielding +to do online safety assurance of a machine learning (ML) +based controller for a reactor control system (RCS). While +ML-based controllers can outperform traditional rule-based +or PID control systems, their lack of provable safety +guarantees has prevented their deployment in nuclear control +applications. This work proposes to integrate shielding into +a ML-based RCS to provide a strong safety guarntee. +Shielding uses temporal logic specifications to define an +area in the state space that is safe. If the ML controller's +predicted actions leave this space or violate a +specification, the shield intervenes and engage a +safety-oriented fallback controller. This way, safety +guarantees are still provided by the fallback controller, +but the ML controller is free to operate within the verified +safe region.. ### Outcomes: + For this research to be successful, I will accomplish the following: -1. Identify key controllers in a nuclear power context with - the most benefit from using an ML-based controller +1. Translate regulatory and system level requirements into a + temporal logic specification to synthesize a controller +'shield'. This shield monitors the ML controller and +intervenes whenever a requirement is predicted to be +violated. -2. Translate regulatory and system level requirements into a - formal specification to synthesize a controller 'shield'. - This shield monitors the ML controller and intervenes - whenever a requirement is predicted to be violated. +2. Design a verified fallback controller against the same + verification requirements that can either return the +reactor to the safe state space or safely shut down the +reactor. 3. Evaluate performance of the ML controller with attached - shield, while assessing the amount of shield useage for - different operating scenarios (power up, shut down, regular - load following) + shield, while assessing shield intervention frequency for +different operating scenarios (power up, shut down, regular +load following). ### Impact: @@ -45,17 +56,16 @@ rule-based controllers by adapting to nonlinear dynamics, optimizing over multi-objective cost functions, and changing plant conditions. But, these ML controllers are often *unexplainable*, meaning that their global behavior is not -easily understood.This unexplainability prevents ML based -controllers from being used in high-assurance usecases such -as nuclear power. Shielding can address this issue, by -providing a formal runtime assurance, allieviating the -burden of explainability away from the machine learning -algorithm. This work would further bring regulatory -requiremnts into the formal design of control systems and -help bridge the gap between high assurance systems and the -start of the art in control. +easily understood. This prevents ML based controllers from +being used in high-assurance usecases such as nuclear power. +Shielding can address this issue, by providing a formal +runtime assurance, alleviating the burden of explainability +away from the machine learning algorithm. This work would +further bring regulatory requiremnts into the formal design +of control systems and high ### Relevant Papers + [[safe-reinforcement-learning-via-shielding]] [[evaluating-robustness-of-neural-networks-with-mixed-integer-programming]] @@ -64,50 +74,71 @@ ___________________________________________________________ ## **Formally Verified Neural Network Control of Control Rod System** ### Goals: -The goal of this research is to use formal methods to ensure that -a neural network based control rod controller will never violate -safety guarantees of a reactor trip system. To do this, a -satisfiability modulo theory method will be applied to -exhaustively search the network for potential failure modes. + +The goal of this resarch is to use formal methods to verify +safety properties of neural network controller for a reactor +control system. Neural network based controllers are able to +efficiently control nonlinear systems with complex +objectives, but by their nature are are opaque systems whose +behavior is not easily analyzed. That being said, once a +neural network is trained, it is an entirely deterministic +system. Recent techniques using satisfiability modulo theory +(SMT) or mixed integer linear programming (MILP) encodings +of neural networks have been used to verify neural network +controller behavior adheres to constraints for fixed input +spaces. This work will adapt these methods to be used with +nuclear-specific safety constraints and enable provably safe +neural network control for the nuclear industry. ### Outcomes: -If this research is successful, I will have accomplished the + +For this research to be successful, I will accomplish the following: -- Build a neural network controller for real time control of a -control rod system. +1. Build a neural network controller for real time control + of a control rod system. -- Formalize safety guarantees of shutdown margin in a -satisfiability modulo theory embedding +2. Encode shutdown margin safety requirements into a SMT or + MILP framework. -- Formally verify that the neural network based controller will -not violate any shutdown margin restrictions +3. Formally verify that the neural network based controller + will not violate any shutdown margin restrictions while +still meeting operational goals. ### Impact: -SMT solvers and MILP formulations have been applied to neural -networks to ensure that the network is resilient to input -perturbations. I think we can expand this to more general -considerations of the state space, especially when there are a -relatively small number of states such as in power contexts. The -benefit of this system is that we would get closer to saying -neural network based systems can be high assurance for physical -systems. + +SMT and MILP methods of verifying neural networks have been +previously applied to classification problems, but have not +been utilized to check neural network controllers for +adherence to cyber-physical system requirements. Critical +infrastructure control such as nuclear power is an ideal +candidate for these methods to be utilized, however, because +the systems being controlled have a bounded and +well-characterized state space compared to other neural +network controller usecases (autonomous flight, autonomous +driving, image classification, etc.). This work, if +successful, will help ease tensions about neural network +controllers' safety for critical infrastructure, and allow a +new class of provably safe control architectures to be used +in high assurance systems. ### Related Papers: + [[reluplex-an-efficient-smt-solver-for-verifying-deep-neural-networks]] [[evaluating-robustness-of-neural-networks-with-mixed-integer-programming]] [[formal-verification-of-neural-network-controlled-autonomous-systems]] - ___________________________________________________________ ## **Temporal Logic Specifications for Autonomous Controller Synthesis** ### Goals: + The goal of this program is to use temporal logic specifications to procedurally generate autonomous supervisory controllers for a reactor system. ### Outcomes: + If this research is successful, I will have accomplished the following: @@ -129,11 +160,13 @@ ___________________________________________________________ ## **Formally Verified Runtime Monitoring and Fallback** ### Goals: + If this research is successful, we will be able to generate autonomous controller shields that provably adhere to specifications written with temporal logic. ### Outcomes: + - Create an intermediary shield that mediates signals between an optimal control system and the physical plant (MODBUS)? @@ -145,6 +178,7 @@ shield components will not allow an arbitrary controller to reach an unsafe state. ### Impact: + Shielding is one of the preeminent ways to do safe machine learning controllers. Instead of putting the proof burden on the machine learning component, shielding creates a safe @@ -162,6 +196,7 @@ engineers of these systems to quickly and clearly implement a shield, without all of the cumbersome derivation. ### Related Papers: + [[on-using-real-time-reachability-for-the-safety-assurance-of-machine-learning-controllers]] [[enhancing-cyber-physical-system-dependability-via-synthesis-challenges-and-future-directions]] [[safe-reinforcement-learning-via-shielding]] @@ -172,6 +207,7 @@ ___________________________________________________________ (8) ### Goals: + The goal of this research is to use machine learning to identify system faults of a reactor control system during runtime. A digital twin will be compared to measurements @@ -181,6 +217,7 @@ that safety strategic decisions about the plant can be made autonomously. ### Outcomes: + For this research to be successful, I will accomplish the following: @@ -199,6 +236,7 @@ control modes rather than only responding with reactor shutdown. ### Impact: + The nuclear energy industry's largest expense is operations and maintenance (O&M). These costs include typical reactor repair and refueling, the labor involved to complete such @@ -229,17 +267,19 @@ Finally reactor safety can be improved by greater autonomy yada yada find some reasons to back this up. ### Related Papers: - ___________________________________________________________ ## **Verified Adaptive Control** + ### Goals: + The goal of this research is to create an adaptive controller that can adjust to system dynamics changes over time to maintain an optimal control, while using formal methods to provide strong safety guarantees about the malleable control law. ### Outcomes: + For this research to be successful, I will accomplish the following: @@ -259,6 +299,7 @@ suspended in the salt I'd assume chemistry is pretty strictly controlled. I'm sure I can find other examples. ### Impact: + Certain reactor control systems are already automatic systems, such as constant temperature or pressure controls for operating at steady state. These simple controllers are able to follow load @@ -274,5 +315,3 @@ of safety in order to be attractive to the nuclear industry. ### Related Papers: - -