Auto sync: 2025-08-29 10:21:31 (9 files changed)

M  .obsidian/plugins/colored-tags/data.json

M  .sessions/nvim_config.vim

D  Projects/HX_PINN/HX_model.py

A  "Zettelkasten/Fleeting Notes/Daily/2025-08-27.md"

A  "Zettelkasten/Permanent Notes/20250826114550-heilmeier-catechism.md"

A  "Zettelkasten/Permanent Notes/Thesis/3100-erlm-quad-chart-template.odp"

A  "Zettelkasten/Permanent Notes/Thesis/DR-20250826144307-heilmeier-questions.md"

A  "Zettelkasten/Permanent Notes/Thesis/DR-20250826145452-title-ideas.md"

.obsidian/plugins/colored-tags/data.json

@@ -323,7 +323,8 @@
     "Formal-Methods": 311,
     "admin": 312,
     "hub": 313,
-    "daily": 314
+    "daily": 314,
+    "weekly": 315
   },
   "_version": 3
 }

.sessions/nvim_config.vim

@@ -18,11 +18,12 @@ badd +27 ~/.config/nvim/lua/custom/language_specific_commands/markdown_and_tex.l
 badd +37 ~/.config/nvim/lua/custom/configs/lspconfig.lua
 badd +2 custom/init.lua
 badd +11 custom/mappings.lua
+badd +385 custom/zk.lua
 argglobal
 %argdel
-edit ~/.config/nvim/lua/custom/configs/lspconfig.lua
+edit custom/zk.lua
 argglobal
-balt ~/.config/nvim/lua/custom/language_specific_commands/markdown_and_tex.lua
+balt ~/.config/nvim/lua/custom/plugins.lua
 setlocal foldmethod=manual
 setlocal foldexpr=v:lua.vim.treesitter.foldexpr()
 setlocal foldmarker={{{,}}}
@@ -33,12 +34,12 @@ setlocal foldnestmax=20
 setlocal foldenable
 silent! normal! zE
 let &fdl = &fdl
-let s:l = 37 - ((36 * winheight(0) + 28) / 57)
+let s:l = 375 - ((40 * winheight(0) + 30) / 60)
 if s:l < 1 | let s:l = 1 | endif
 keepjumps exe s:l
 normal! zt
-keepjumps 37
+keepjumps 375
-normal! 059|
+normal! 067|
 tabnext 1
 if exists('s:wipebuf') && len(win_findbuf(s:wipebuf)) == 0 && getbufvar(s:wipebuf, '&buftype') isnot# 'terminal'
   silent exe 'bwipe ' . s:wipebuf

Projects/HX_PINN/HX_model.py

@@ -1,235 +0,0 @@
-# PINN for a tube-in-tube heat exchanger (steady 2D xr)
-# - Uses automatic differentiation for PDE residuals
-# - Prescribes velocity fields u_h(x,r), u_c(x,r)
-# - Solves for Th, Tw, Tc
-
-import torch
-import torch.nn as nn
-
-# ====== User-configurable physical constants (nondimensional if you scaled) ======
-Pe_h = 100.0  # Peclet (hot side)  = u_h*L/alpha_h
-Pe_c = 120.0  # Peclet (cold side) = u_c*L/alpha_c
-alpha_w_ratio = 1.0  # wall alpha relative to hot-side alpha if nondim
-Ri = 1.0  # inner radius (nondim, after scaling)
-Ro = 1.3  # outer radius
-
-device = "cuda" if torch.cuda.is_available() else "cpu"
-dtype = torch.float32  # float32 is usually fine; use float64 if residuals are stiff
-
-
-# ====== Velocity profiles (nondim) ======
-def u_h(x, r):
-    # Poiseuille in a circular tube: u_max*(1 - (r/Ri)^2). Here Ri=1 in nondim.
-    return 2.0 * (1.0 - r**2)  # average=1 if scaled; adjust factor to match Pe_h
-
-
-def u_c(x, r):
-    # Simple plug profile in annulus as a first approximation
-    return torch.ones_like(r)
-
-
-# ====== Network ======
-class MLP(nn.Module):
-    def __init__(self, in_dim=2, hidden=128, depth=7, out_dim=3, act=nn.SiLU):
-        super().__init__()
-        layers = [nn.Linear(in_dim, hidden), act()]
-        for _ in range(depth - 1):
-            layers += [nn.Linear(hidden, hidden), act()]
-        # Separate heads for Th, Tw, Tc improves conditioning
-        self.backbone = nn.Sequential(*layers)
-        self.head_h = nn.Linear(hidden, 1)
-        self.head_w = nn.Linear(hidden, 1)
-        self.head_c = nn.Linear(hidden, 1)
-
-        # Xavier init helps with tanh/SiLU nets
-        def init(m):
-            if isinstance(m, nn.Linear):
-                nn.init.xavier_uniform_(m.weight)
-                nn.init.zeros_(m.bias)
-
-        self.apply(init)
-
-    def forward(self, x, r):
-        z = torch.stack([x, r], dim=-1)
-        f = self.backbone(z)
-        Th = self.head_h(f)
-        Tw = self.head_w(f)
-        Tc = self.head_c(f)
-        return Th, Tw, Tc
-
-
-net = MLP().to(device).to(dtype)
-
-
-# ====== Utility: gradients via autograd ======
-def grads(y, x):
-    return torch.autograd.grad(
-        y, x, grad_outputs=torch.ones_like(y), create_graph=True
-    )[0]
-
-
-# ====== Collocation samplers ======
-def sample_in_hot(N):
-    # x in [0,1], r in [0,Ri]
-    x = torch.rand(N, 1, device=device, dtype=dtype)
-    r = Ri * torch.sqrt(torch.rand(N, 1, device=device, dtype=dtype))  # area-uniform
-    return x.requires_grad_(True), r.requires_grad_(True)
-
-
-def sample_in_wall(N):
-    x = torch.rand(N, 1, device=device, dtype=dtype)
-    r = torch.sqrt(
-        (Ro**2 - Ri**2) * torch.rand(N, 1, device=device, dtype=dtype) + Ri**2
-    )
-    return x.requires_grad_(True), r.requires_grad_(True)
-
-
-def sample_in_cold(N):
-    x = torch.rand(N, 1, device=device, dtype=dtype)
-    r = (Ro + (Ro)) * 0.5 * 0 + (
-        torch.rand(N, 1, device=device, dtype=dtype) * (Ro - Ri) + Ri
-    )  # simple annulus
-    return x.requires_grad_(True), r.requires_grad_(True)
-
-
-def sample_interface_Ri(N):
-    x = torch.rand(N, 1, device=device, dtype=dtype)
-    r = torch.full_like(x, Ri, requires_grad=True)
-    return x, r
-
-
-def sample_interface_Ro(N):
-    x = torch.rand(N, 1, device=device, dtype=dtype)
-    r = torch.full_like(x, Ro, requires_grad=True)
-    return x, r
-
-
-def sample_inlet_hot(N):
-    x = torch.zeros(N, 1, device=device, dtype=dtype, requires_grad=True)
-    r = Ri * torch.sqrt(torch.rand(N, 1, device=device, dtype=dtype))
-    return x, r
-
-
-def sample_inlet_cold_counterflow(N):
-    x = torch.ones(N, 1, device=device, dtype=dtype, requires_grad=True)
-    r = torch.rand(N, 1, device=device, dtype=dtype) * (Ro - Ri) + Ri
-    return x, r
-
-
-def sample_outlet_hot(N):
-    x = torch.ones(N, 1, device=device, dtype=dtype, requires_grad=True)
-    r = Ri * torch.sqrt(torch.rand(N, 1, device=device, dtype=dtype))
-    return x, r
-
-
-def sample_outlet_cold(N):
-    x = torch.zeros(N, 1, device=device, dtype=dtype, requires_grad=True)
-    r = torch.rand(N, 1, device=device, dtype=dtype) * (Ro - Ri) + Ri
-    return x, r
-
-
-# ====== Boundary condition targets (nondim) ======
-T_h_in = 1.0  # scale so hot inlet is 1
-T_c_in = 0.0  # cold inlet is 0
-
-# ====== Training loop ======
-opt = torch.optim.Adam(net.parameters(), lr=1e-3)
-
-for it in range(20000):
-    opt.zero_grad()
-
-    # ----- Interior residuals -----
-    Nh = Nw = Nc = 512
-    xh, rh = sample_in_hot(Nh)
-    xw, rw = sample_in_wall(Nw)
-    xc, rc = sample_in_cold(Nc)
-
-    Th, Tw, Tc = net(xh, rh)
-    Th_x = grads(Th, xh)
-    Th_r = grads(Th, rh)
-    Th_xx = grads(Th_x, xh)
-    Th_rr = grads(Th_r, rh)
-    # Hot PDE: u_h dTh/dx = (1/Pe_h)*(Th_rr + (1/r) Th_r + Th_xx)  (choose to keep xx or drop)
-    uh = u_h(xh, rh)
-    hot_res = uh * Th_x - (1.0 / Pe_h) * (Th_rr + (1.0 / rh) * Th_r + Th_xx)
-
-    (Tw_,) = net(xw, rw)[1:2]  # only Tw
-    Tw_x = grads(Tw_, xw)
-    Tw_r = grads(Tw_, rw)
-    Tw_xx = grads(Tw_x, xw)
-    Tw_rr = grads(Tw_r, rw)
-    wall_res = Tw_rr + (1.0 / rw) * Tw_r + Tw_xx  # alpha_w absorbed in scaling
-
-    Tc = net(xc, rc)[2]
-    Tc_x = grads(Tc, xc)
-    Tc_r = grads(Tc, rc)
-    Tc_xx = grads(Tc_x, xc)
-    Tc_rr = grads(Tc_r, rc)
-    uc = u_c(xc, rc)
-    cold_res = uc * Tc_x - (1.0 / Pe_c) * (Tc_rr + (1.0 / rc) * Tc_r + Tc_xx)
-
-    L_pde = hot_res.pow(2).mean() + wall_res.pow(2).mean() + cold_res.pow(2).mean()
-
-    # ----- Interface continuity (temperature + flux) -----
-    Ni = 256
-    xi, rRi = sample_interface_Ri(Ni)
-    Th_i, Tw_i, _ = net(xi, rRi)
-    # fluxes: -k dT/dr. With nondim, use ratios; set k_w/k_h = kw_rel, etc.
-    dTh_dr = grads(Th_i, rRi)
-    dTw_dr = grads(Tw_i, rRi)
-    kw_over_kh = 1.0
-    L_int_Ri = (Th_i - Tw_i).pow(2).mean() + (dTh_dr - kw_over_kh * dTw_dr).pow(
-        2
-    ).mean()
-
-    xo, rRo = sample_interface_Ro(Ni)
-    _, Tw_o, Tc_o = net(xo, rRo)
-    dTw_dr_o = grads(Tw_o, rRo)
-    dTc_dr_o = grads(Tc_o, rRo)
-    kc_over_kw = 1.0
-    L_int_Ro = (Tc_o - Tw_o).pow(2).mean() + (kc_over_kw * dTc_dr_o - dTw_dr_o).pow(
-        2
-    ).mean()
-
-    # ----- Boundary conditions -----
-    Nb = 256
-    x_in_h, r_in_h = sample_inlet_hot(Nb)
-    Th_in_pred = net(x_in_h, r_in_h)[0]
-    L_in_h = (Th_in_pred - T_h_in).pow(2).mean()
-
-    x_in_c, r_in_c = sample_inlet_cold_counterflow(Nb)
-    Tc_in_pred = net(x_in_c, r_in_c)[2]
-    L_in_c = (Tc_in_pred - T_c_in).pow(2).mean()
-
-    # Outlets: convective (∂T/∂x ≈ 0)
-    x_out_h, r_out_h = sample_outlet_hot(Nb)
-    Th_out = net(x_out_h, r_out_h)[0]
-    L_out_h = grads(Th_out, x_out_h).pow(2).mean()
-
-    x_out_c, r_out_c = sample_outlet_cold(Nb)
-    Tc_out = net(x_out_c, r_out_c)[2]
-    L_out_c = grads(Tc_out, x_out_c).pow(2).mean()
-
-    # Symmetry at r=0: dTh/dr = 0
-    Ns = 128
-    xs = torch.rand(Ns, 1, device=device, dtype=dtype, requires_grad=True)
-    rs0 = torch.zeros_like(xs, requires_grad=True)
-    Th_axis = net(xs, rs0)[0]
-    L_sym = grads(Th_axis, rs0).pow(2).mean()
-
-    # ----- Total loss with simple weights (tune these!) -----
-    L = (
-        1.0 * L_pde
-        + 5.0 * (L_int_Ri + L_int_Ro)
-        + 2.0 * (L_in_h + L_in_c)
-        + 1.0 * (L_out_h + L_out_c)
-        + 1.0 * L_sym
-    )
-
-    L.backward()
-    opt.step()
-
-    if it % 1000 == 0:
-        print(
-            f"it={it}  L={L.item():.3e}  PDE={L_pde.item():.3e}  IF={L_int_Ri.item()+L_int_Ro.item():.3e}"
-        )

Zettelkasten/Fleeting Notes/Daily/2025-08-20.md

@@ -3,7 +3,7 @@ id: 2025-08-20
 title: Daily — 2025-08-20
 type: daily
 created: 2025-08-20T13:54:13Z
-modified: 2025-08-20T19:10:43Z
+modified: 2025-08-22T15:06:52Z
 tags: [daily]
 ---
 

Zettelkasten/Fleeting Notes/Daily/2025-08-22.md

@@ -0,0 +1,24 @@
+---
+id: 2025-08-22
+title: Daily — 2025-08-22
+type: daily
+created: 2025-08-22T15:41:02Z
+modified: 2025-08-22T16:03:15Z
+tags: [daily]
+---
+
+# Daily — 2025-08-22
+
+## Quick capture
+
+- Got to work kind of late. Feeling sicky af. Probably no
+darts tonight with PSM.
+- Working on moving all my notes into zettels
+- Lunch w AS today
+- Okay i'm starting to feel a little better (12:03PM)
+
+## Tasks
+
+- [ ] 
+
+## Notes

Zettelkasten/Fleeting Notes/Daily/2025-08-25.md

@@ -0,0 +1,29 @@
+---
+id: 2025-08-25
+title: Daily — 2025-08-25
+type: daily
+created: 2025-08-25T16:02:00Z
+modified: 2025-08-26T13:56:53Z
+tags: [daily]
+---
+
+# Daily — 2025-08-25
+
+## Quick capture
+
+- Got in a little later today, but the bike is here! Gotta
+text Alisa about it.
+
+- I have 2 classes today (grumble grumble grumble). 
+    - ME 3100 ERLM is Monday and Wednesday at 1PM-2:15PM
+    - NUCE 2101 - Nuclear Core Dynamics is tonight
+    6PM-8:30PM, like usual
+
+- I also enrolled in my health insurance.
+
+
+## Tasks
+
+- [ ] 
+
+## Notes

Zettelkasten/Fleeting Notes/Daily/2025-08-26.md

@@ -0,0 +1,19 @@
+---
+id: 2025-08-26
+title: Daily — 2025-08-26
+type: daily
+created: 2025-08-26T15:05:38Z
+modified: 2025-08-26T15:06:58Z
+tags: [daily]
+---
+
+# Daily — 2025-08-26
+
+## Quick Capture
+
+- I started this morning doing some email
+- Now I'm hangin out in starbucks doing some work for the
+quad chart n'at
+- First, what the fuck is a quad chart??
+
+## Notes

Zettelkasten/Fleeting Notes/Daily/2025-08-27.md

@@ -0,0 +1,32 @@
+---
+id: 2025-08-27
+title: Daily — 2025-08-27
+type: daily
+created: 2025-08-27T18:33:33Z
+modified: 2025-08-28T17:57:53Z
+tags: [daily]
+---
+
+# Daily — 2025-08-27
+
+## Quick capture
+
+COLE GROUP MEETING
+Accomplishments:
+- Quad chart
+- writing more about LTL and building out some notes from
+papers
+- Found resources about temporal logic
+- first nuce class has happened. Codes and standards were
+cancelled
+
+to do:
+- Write goals and outcomes
+- Write more about approach. This is squishtastic
+- Actually finalize some outcomes. How do i navigate the
+fact that within switching mechanisms there is dynamics
+happening
+- I didn't say anything about what a hybrid system is.
+That's kind of the whole point of the thing.
+
+## Notes

Zettelkasten/Hub Notes/HUB-20250822135454-formal-methods.md

@@ -0,0 +1,38 @@
+---
+id: HUB-20250822135454
+title: Formal Methods
+type: hub
+created: 2025-08-22T17:54:54Z
+modified: 2025-08-22T17:57:39Z
+tags: [hub]
+aliases: []
+---
+
+# Formal Methods
+
+> The purpose of this hub is to make a high level hub of
+> everything formal methods related (which is a lot!!!)
+
+## Related hubs
+
+- [[formal-methods-in-machine-learning]]  
+
+## Related Zettels
+### Topics
+
+[[Abstract Interpretation for Formal Methods]]
+[[Satisfiability Modulo Theory]]
+[[Mixed Integer Linear Programming]]
+[[Complete vs. Incomplete Formal Methods]]
+
+### Tools
+[[Strix]]
+
+
+## Sources / Literature
+
+- [[a-review-of-formal-methods-applied-to-machine-learning]]
+
+## Open questions / Next actions
+
+- [ ] 

Zettelkasten/Permanent Notes/20250822134355-formal-methods-in-machine-learning.md

@@ -0,0 +1,10 @@
+---
+id: 20250822134355
+title: Formal Methods in Machine Learning
+type: permanent
+created: 2025-08-22T17:43:55Z
+modified: 2025-08-22T17:43:55Z
+tags: []
+---
+
+# Formal Methods in Machine Learning

Zettelkasten/Permanent Notes/20250822135802-abstract-interpretation-for-formal-methods.md

@@ -0,0 +1,15 @@
+---
+id: 20250822135802
+title: Abstract Interpretation for Formal Methods
+type: permanent
+created: 2025-08-22T17:58:02Z
+modified: 2025-08-25T16:01:46Z
+tags: []
+---
+
+# Abstract Interpretation for Formal Methods
+
+Abstract interpretation in a formal methods context takes
+something about a system and makes an approximation of it in
+order to make reasoning about it easier.
+

Zettelkasten/Permanent Notes/20250826111220-quad-charts.md

@@ -0,0 +1,58 @@
+---
+id: 20250826111220
+title: Quad Charts
+type: permanent
+created: 2025-08-26T15:12:20Z
+modified: 2025-08-26T15:20:50Z
+tags: []
+---
+
+# Quad Charts
+
+Quad charts are the briefest of research proposals, and are
+a way of conveying a research idea in just one
+slide. 
+
+The audience for a quad chart is usually non-technical. The
+content should reflect this.
+
+Quad charts consist of quadrants:
+
+## Quadrant 1 (Upper Left): Goals and Objectives
+
+This quadrant states the goal of the research in a single
+sentence, and lists the outcomes underneath it. Often you
+can start with "The goal of this research is to..."
+
+Then, the outcomes follow: "If this research is
+successful, we should be able to do the following:
+
+1. ...
+2. ...
+3. ...
+(4.?)
+
+It is critical that no jargon is used here. It is very
+tempting to do so.
+
+## Quadrant 2 (Bottom Left): Research Approach
+
+This quadrant answers the question: "What's new in your
+approach?"
+
+## Quadrant 3 (Top Right): Pretty Picture
+
+This is a break for the reader, and likely the first thing
+they'll actually look at on the chart. This figure should
+illustrate a key idea about the work that you want the
+reader to take away.
+
+No personal information should be included.
+
+## Quadrant 4 (Bottom Right): Impact and Contact Info
+
+This quadrant answers the question of "Who cares? What
+difference will it make if you're successful?"
+
+This quadrant should also contain contact info of the
+principal investigator, and if applicable, their advisor.

Zettelkasten/Permanent Notes/20250826114550-heilmeier-catechism.md

@@ -0,0 +1,40 @@
+---
+id: 20250826114550
+title: Heilmeier Catechism
+type: permanent
+created: 2025-08-26T15:45:50Z
+modified: 2025-08-26T16:02:59Z
+tags: []
+---
+
+# Heilmeier Catechism
+
+George Heilmeier was a program manager at the Defense
+Advanced Research Projects Administration (DARPA) who was
+flummoxed with research proposals for artificial
+intelligence. In order to quickly sort through the
+proposals, he developed an 8 question system to quickly cut
+through the muck.
+
+This is the Heilmeier Catechism:
+
+1. What are you trying to do? Articulate your research with
+   absolutely no jargon.
+
+2. How is it done today and what are the limits of current
+   practice?
+
+3. What's new in your approach and why will you be
+   successful?
+
+4. Who cares? If you're successful, what difference will it
+   make?
+
+5. What are the risks?
+
+6. How long will it take?
+
+7. How much will it cost?
+
+8. What are the midterm and final exams? How will you
+   measure success?

Zettelkasten/Permanent Notes/Literature Notes/LIT-20250822120822-a-review-of-formal-methods-applied-to-machine-learning.md

@@ -0,0 +1,97 @@
+---
+id: LIT-20250822120822
+title: A Review of Formal Methods applied to Machine Learning
+type: literature
+created: 2025-08-22T16:08:22Z
+modified: 2025-08-22T16:11:25Z
+citekey: 
+---
+
+# A Review of Formal Methods applied to Machine Learning
+
+**Category:** This is a review paper. 
+
+**Context:** This paper tries to keep up with where formal
+methods are for machine learning based systems. It is not
+necessarily a controls paper, but a broader machine learning
+paper in general.
+
+**Correctness:** Really well written on the first pass. Easy
+to understand and things seem well cited.
+
+**Contributions:** Great citations showing links to
+different papers and also provides nice spots for forward
+research. Talks about how verification needs to be done
+along the whole pipeline: from data prep to training to
+implementation. There needs to be more work on proving
+things about model behavior, but in general this review has
+a positive outlook on the field. 
+
+**Clarity:** Very well written, easy to understand. Except,
+what is abstractification of a network?
+
+## Second Pass
+This review gives an overview of formal
+methods applied to machine learning. Formal methods has been
+used for ML to test for robustness for various perturbations
+on inputs. They start by talking about several types of
+formal methods, including deductive verification, design by
+refinement, proof assistants, model checking, and semantic
+static analysis, and then finally, abstract interpretation
+of semantic static analysis. The last one has been used the
+most in FM of ML.
+
+A large part of the paper focuses on formal methods for
+neural network perturbation robustness. They split up the
+methods into two types: complete and incomplete formal
+methods. Complete formal methods are *sound* and *complete*.
+This means they do not have false positives or false
+negatives. These methods generally do not apply well to
+large networks (beyond hundreds gets rough), but give the
+highest level of assurance. Here, there are two more
+subcategories: SMT based solvers and MILP-based solvers.
+
+SMT solvers are Satisfiability Modulo Theory solvers. These
+solvers a set of constraints and check to see whether or not
+all of the constraints can be satisfied. Safety conditions
+are encoded as the *nA Review of Formal Methods applied to Machine Learningegation* of the safety constraint. That
+way, if a safety condition is violated, the SMT solver will
+pick it up as a counter example. 
+
+MILP based solvers are Mixed Integer Linear Programming
+solvers. MILPs use linear programming where certain
+constraints are integers to reduce the solving space.
+Instead of having an explicity satisffiability condition on
+safety or not, MILPs instead can use a minimizing function
+to generate counter examples. For example, a MILP saftey
+condition might be formalized as: $$ \text{min}\space
+\bf{x}_n$$ where a negative value of $\bf{x}_n$ is 'a valid
+counter example'.
+
+There are also 'incomplete formal methods'. These incomplete
+methods are sound, meaning they will not produce false
+negatives, but they may not be complete, meaning they may
+produce false positives. They scale better, but the false
+positives can be pretty annoying.
+
+One of the main incomplete methods is abstract
+interpretation. Things get very weird very fast--this is all
+about zonotopes and using over approximation of sets to say
+things about stability. There is weird stuff going on with
+cell splitting and merging that seems like a to grasp. But,
+apparently it works. 
+
+Next, they spend some time talking about other machine
+learning methods and the formal methods that have been
+applied to them. Of particular interest to me is the formal
+method application to support vector machines and decision
+trees. There are some useful methods for detecting
+robustness to adversarial inputs, and knowing what the
+nearest misclassification adversarial case is.
+
+## Third Pass
+**Recreation Notes:**
+
+**Hidden Findings:**
+
+**Weak Points? Strong Points?**

Zettelkasten/Permanent Notes/Literature Notes/to_process/A Review of Formal Methods applied to Machine Learning-Note.md

@@ -0,0 +1,77 @@
+# First Pass
+**Category:** 
+This is a review paper. 
+
+**Context:** 
+This paper tries to keep up with where formal methods are for machine 
+learning based systems. It is not necessarily a controls paper, but a broader
+machine learning paper in general.
+
+**Correctness:** 
+Really well written on the first pass. Easy to understand and things seem 
+well cited.
+
+**Contributions:** 
+Great citations showing links to different papers and also provides nice spots
+for forward research. Talks about how verification needs to be done along the
+whole pipeline: from data prep to training to implementation. There needs to 
+be more work on proving things about model behavior, but in general this
+review has a positive outlook on the field. 
+
+**Clarity:** 
+Very well written, easy to understand. Except, what is abstractification of a 
+network?
+
+# Second Pass
+This review gives an overview of formal methods applied to machine learning.
+Formal methods has been used for ML to test for robustness for various 
+perturbations on inputs. They start by talking about several types of formal 
+methods, including deductive verification, design by refinement, proof 
+assistants, model checking, and semantic static analysis, and then finally, 
+abstract interpretation of semantic static analysis. The last one has been 
+used the most in FM of ML.
+
+A large part of the paper focuses on formal methods for neural network 
+perturbation robustness. They split up the methods into two types: complete
+and incomplete formal methods. Complete formal methods are *sound* and 
+*complete*. This means they do not have false positives or false negatives. 
+These methods generally do not apply well to large networks (beyond 
+hundreds gets rough), but give the highest level of assurance. Here, there
+are two more subcategories: SMT based solvers and MILP-based solvers.
+
+SMT solvers are Satisfiability Modulo Theory solvers. These solvers a set
+of constraints and check to see whether or not all of the constraints can be 
+satisfied. Safety conditions are encoded as the *negation* of the safety constraint.
+That way, if a safety condition is violated, the SMT solver will pick it up as a 
+counter example. 
+
+MILP based solvers are Mixed Integer Linear Programming solvers. MILPs use
+linear programming where certain constraints are integers to reduce the
+solving space. Instead of having an explicity satisffiability condition on safety
+or not, MILPs instead can use a minimizing function to generate counter
+examples. For example, a MILP saftey condition might be formalized as:
+$$ \text{min}\space \bf{x}_n$$
+where a negative value of $\bf{x}_n$ is 'a valid counter example'.
+
+There are also 'incomplete formal methods'. These incomplete methods are
+sound, meaning they will not produce false negatives, but they may not be
+complete, meaning they may produce false positives. They scale better, but
+the false positives can be pretty annoying.
+
+One of the main incomplete methods is abstract interpretation. Things get very
+weird very fast--this is all about zonotopes and using over approximation of sets
+to say things about stability. There is weird stuff going on with cell splitting 
+and merging that seems like a to grasp. But, apparently it works. 
+
+Next, they spend some time talking about other machine learning methods and
+the formal methods that have been applied to them. Of particular interest to me
+is the formal method application to support vector machines and decision 
+trees. There are some useful methods for detecting robustness to adversarial 
+inputs, and knowing what the nearest misclassification adversarial case is.
+
+# Third Pass
+**Recreation Notes:**
+
+**Hidden Findings:**
+
+**Weak Points? Strong Points?**

Zettelkasten/Permanent Notes/Literature Notes/to_process/A systematic classification of neural-network-based control-Note.md

@@ -0,0 +1,32 @@
+# First Pass
+**Category:**
+This paper is a literature review
+
+**Context:** 
+Mukul says that there are a whole bunch of thrusts out there about neural 
+network based controllers, and that there needs to be a better way to 
+parse what research is what
+
+**Correctness:** 
+Looks good to me I suppose.
+
+**Contributions:** 
+Here's the most important figure in the whole thing:
+![[Pasted image 20250721095146.png]]
+
+**Clarity:** 
+Well written.
+
+# Second Pass
+**What is the main thrust?**
+
+**What is the supporting evidence?**
+
+**What are the key findings?**
+
+# Third Pass
+**Recreation Notes:**
+
+**Hidden Findings:**
+
+**Weak Points? Strong Points?**

Zettelkasten/Permanent Notes/Literature Notes/to_process/An autonomous control framework for advanced reactors-notes.md

@@ -0,0 +1,59 @@
+---
+alias: tee-hee-hee
+---
+
+# An autonomous control framework for advanced reactors notes
+
+## First Pass
+**Category:** 
+This is a vision-like paper.
+
+**Context:** 
+Dr. Wood is a professor of nuclear engineering at the University of Tennesse.
+He started working at UT after working at ORNL for 20+ years where he was
+a senior researcher. He works on common cause failures.
+
+**Correctness:** 
+There are not many citations, and a lot of the paper seems like it is off-the-cuff. 
+This was an invited article though in the *Nuclear Engineering and Technology* 
+journal. He's also got quite the resume.
+
+**Contributions:** 
+Dr. Wood gives a good overview of where we are (automated control), and
+where we need to go (autonomous control). Comparisons are made to other 
+industries, and how they've addressed these challenges. Clarifications are made
+with respect to how the nuclear industry is unique.
+
+**Clarity:** 
+Well written and clear, but a bit wordy at times. Examples are used but 
+sometimes it just feels like a mouthful.
+
+## Second Pass
+**What is the main thrust?**
+Wood talks a lot about what it means for a system to be autonomous. He 
+actually starts with a etymological argument- "*automatos* means self-acting,
+whereas *autonomos* means independent." The point of an autonomous system 
+is that it must be able to make intelligent decisions that a human would 
+otherwise make. Knowing how to handle degraded or faulty sensors or 
+actuators, switching controller trains, and knowing when scramming is
+necessary are all decisions that an autonomous system would make, that
+a simple automated system could not. The key is in the decision making.
+
+**What is the supporting evidence?**
+Dr. Wood compares a lot to NASA control systems for the Mars rovers. These
+systems use two tiers of controllers: a decision layer and a functionality layer. 
+The functionality layer does what you think--it manages the physical 
+functioning. The decision layer is different. It decides on controller modes and 
+works instead with operational level goals.
+
+**What are the key findings?**
+The biggest findings are that an autonomous control system for a nuclear
+power plant is possible, but by far the biggest roadblock is a high assurance 
+decision making system. 
+
+## Third Pass
+**Recreation Notes:**
+
+**Hidden Findings:**
+
+**Weak Points? Strong Points?**

Zettelkasten/Permanent Notes/Literature Notes/to_process/Automation levels for nuclear reactor operations- A revised perspective - Note.md

@@ -0,0 +1,36 @@
+# First Pass
+**Category:** 
+This is a paper following a workshop. It is kind of a big picture / idea 
+type paper.
+
+**Context:** 
+This paper was written after a workshop took place to talk about recent NRC
+regulations. They talk about how different industries categorize the level
+of autonomy in systems, and create autonomous levels of reactor control.
+
+**Correctness:** 
+Vivek Agarwal chaired ANS in Chicago this past year. He's the real deal
+
+**Contributions:** 
+They contribute a first thought on how to go about creating milestones for
+autonomous systems, and give us a language to use when describing what level
+of autonomy a system is gunning for.
+
+**Clarity:** 
+Clearly written. Very nice!
+
+# Second Pass
+**What is the main thrust?**
+
+**What is the supporting evidence?**
+
+**What are the key findings?**
+
+# Third Pass
+**Recreation Notes:**
+
+**Hidden Findings:**
+
+**Weak Points? Strong Points?**
+
+<!The quick brown fox jumps over the lazy dog. The dog takes a nice nap. :)>

Zettelkasten/Permanent Notes/Literature Notes/to_process/Economics and finance of Small Modular Reactors- A systematic review and research agenda-Note.md

@@ -0,0 +1,32 @@
+# First Pass
+**Category:** 
+Systematic Review
+
+**Context:** 
+This paper is from the civil engineering school at the University of Leeds. 
+They are doing an overview of economics and finance research of small
+modular reactors.
+
+**Correctness:** 
+Can not say. Is a review!
+
+**Contributions:** 
+They do a good break down of the research we have done ('what we know') and
+what needs done ('what we do not know'). They point out a big discrepancy that we do not have a lot of research on operations and maintenance costs. 
+
+**Clarity:** 
+Nicely written. Easy to understand.
+
+# Second Pass
+**What is the main thrust?**
+
+**What is the supporting evidence?**
+
+**What are the key findings?**
+
+# Third Pass
+**Recreation Notes:**
+
+**Hidden Findings:**
+
+**Weak Points? Strong Points?**

Zettelkasten/Permanent Notes/Literature Notes/to_process/Enhancing Cyber-Physical System Dependability via Synthesis- Challenges and Future Directions-Note.md

@@ -0,0 +1,33 @@
+# First Pass
+**Category:** This paper is an experimental paper. 
+
+**Context:** The context of this paper is using a couple different techniques 
+synthesize control programs using different formal methods tools.
+
+**Correctness:** I trust Max's integrity. Some of the citations were funky and
+the intro was fluffy though.
+
+**Contributions:** 
+This paper shows that using LTL and other formal methods still struggles to 
+generate controllers for significantly challenging systems. The high bay 
+warehouse used to create this paper had to be simplified. Then, they introduce
+an SMT solver based method to try to generate code.
+
+**Clarity:** 
+The intro and conclusion do not provide very strong clarity on what they 
+actually did other than "high assurance is high difficulty", and that we're not 
+really there yet on HACPS.
+
+# Second Pass
+**What is the main thrust?**
+
+**What is the supporting evidence?**
+
+**What are the key findings?**
+
+# Third Pass
+**Recreation Notes:**
+
+**Hidden Findings:**
+
+**Weak Points? Strong Points?**

Zettelkasten/Permanent Notes/Literature Notes/to_process/Evaluating Robustness of Neural Networks with Mixed Integer Programming-Note.md

@@ -0,0 +1,42 @@
+# First Pass
+**Category:** 
+This is a methods paper. 
+
+**Context:** 
+This paper proposes a way of using mixed integer linear programming (MILP)
+to  evaluate properties of neural networks.
+
+**Correctness:** 
+Formal
+
+**Contributions:** 
+They do nifty things with bounds tightening and presolving that makes their
+solver very fast compared to the state of the art or Reluplex. They also talk 
+about stable and unstable neurons.
+
+**Clarity:** 
+They have a really good explanation of what a MILP problem is and how one
+might encode a neural network as one.
+
+# Second Pass
+**What is the main thrust?**
+The main thrust is their new solving method of MILPs for neural networks.
+With their method, neural networks can have their neurons analyzed to 
+prove whether or not the network is robust to input perturbations. This is 
+especially important for classifiers, who need to know if there are sneaky
+nonlinearities that can be harmful to a built system (like a glitch). This 
+method of bounds tightening and MILP usage makes their solver much faster
+and therein more capable to handle large networks.
+
+**What is the supporting evidence?**
+They have a whole bunch of experimental results.
+
+**What are the key findings?**
+MILPs and bound tightening is very good!
+
+# Third Pass
+**Recreation Notes:**
+
+**Hidden Findings:**
+
+**Weak Points? Strong Points?**

Zettelkasten/Permanent Notes/Literature Notes/to_process/Formal requirements elicitation with FRET-Note.md

@@ -0,0 +1,31 @@
+# First Pass
+**Category:** 
+This is a weird one. This paper is essentially just a 'state-of-the-FRET' paper
+
+**Context:** 
+FRET comes from NASA and is a tool to line up requirements in a temporal
+language.
+
+**Correctness:** 
+Formal. But they don't really go into details.
+
+**Contributions:** 
+Really I don't think they contribute much here than an explanation of what's
+going on.
+
+**Clarity:** 
+Easy to read. 
+
+# Second Pass
+**What is the main thrust?**
+
+**What is the supporting evidence?**
+
+**What are the key findings?**
+
+# Third Pass
+**Recreation Notes:**
+
+**Hidden Findings:**
+
+**Weak Points? Strong Points?**

Zettelkasten/Permanent Notes/Literature Notes/to_process/Formal verification of neural network controlled autonomous systems-Note.md

@@ -0,0 +1,31 @@
+# First Pass
+**Category:** 
+Methods paper
+
+**Context:** 
+Using NN w/ LiDAR to say safety reliability claims using FM
+
+**Correctness:** 
+Assumptions seem good, other than anticipating LiDAR as a 
+continuous data stream. 
+
+**Contributions:** 
+1. Framewok for formally proving safety properties of autonomous robots using LiDAR and NNs
+2. Something something imaging-adapted partitions. A 'notion'
+
+**Clarity:** 
+Very well written and clear.
+
+# Second Pass
+**What is the main thrust?**
+
+**What is the supporting evidence?**
+
+**What are the key findings?**
+
+# Third Pass
+**Recreation Notes:**
+
+**Hidden Findings:**
+
+**Weak Points? Strong Points?**

Zettelkasten/Permanent Notes/Literature Notes/to_process/Hardware In The Loop Papers-Note.md

@@ -0,0 +1,50 @@
+---
+creation date: 2024-08-08
+modification date: Thursday 8th August 2024 09:57:16
+tags:
+  - Research
+  - "#Survey"
+---
+# Preamble
+### Notable Links
+[[ARCADE Implementation at the University of Pittsburgh]]
+[[1. A shortlist of ARCADE Experiments]]
+## What are we doing?
+Collecting and organizing papers about HiTL testing. Making notes about 'em. Stuff like that.
+## Why are we doing it?
+08-08-2024: I'm writing a paper for [[2. (SR-CIST) Workshop on Security and Resiliency of Critical Infrastructure and Space Technologies]] and really need to know about hardware in the loop testing. 
+## Who cares?
+Me. Andrew, probably. Dan, a lot.
+# Papers
+## Summary Table
+```dataview
+table without id
+link(file.path, title) as "Title", year as "Year", authors as "Authors", readstatus as "Read Status"
+from outgoing([[]])
+where readstatus or readstatus=False 
+sort readstatus desc, year desc
+```
+## Papers about ARCADE
+[[maccaroneADVANCEDREACTORCYBER]]
+[[chenFullscopeHighfidelitySimulatorbased2024]]
+
+## Hardware In The Loop Papers
+[[mihalicHardwareintheLoopSimulationsHistorical2022]]
+[[bullockHardwareintheloopSimulation2004]]
+[[puysHardwareInTheLoopLabsSCADA2021]]
+[[choiRealTimeHardwareintheLoopHIL2021]]
+
+## Cybersecurity of OT Papers
+[[sunSoKAttacksIndustrial2021]]
+[[mclaughlinControllerawareFalseData2014]]
+[[chekoleEnforcingMemorySafety2018]]
+[[kushnerRealStoryStuxnet2013]]
+[[CyberAttackGerman2015]]
+[[sguegliaFederalOfficialsInvestigating2023]]
+## Formal Methods and PLCs
+[[fernandezadiegoApplyingModelChecking2015]]
+[[lopez-miguelPLCverifStatusFormal2022]]
+[[kleinFormallyVerifiedSoftware2018]] -- Littlebird paper
+
+## Kry10
+[[Kry10TechnicalOverview]]

Zettelkasten/Permanent Notes/Literature Notes/to_process/On Using Real-Time Reachability for the Safety Assurance of Machine Learning Controllers-Note.md

@@ -0,0 +1,36 @@
+# First Pass
+**Category:** Experimental Results
+
+**Context:** They used a F1/10 model of an autonomous car to test out a simplex
+safety structure on a neural network based controller. They try several
+different neural net types. Their trick is they use real time reachability to tell
+ when to switch between an optimal controller and the simplex guard.
+
+**Correctness:** 
+They seem to do things pretty well and by the book. All of their explanations
+make sense and they do a good job citing sources. They do punt when it comes
+to talking about the formal verification of the switching mechanism, but they 
+do make note that's future work.
+
+**Contributions:** 
+They show how a simplex system can work and the difficulties of the *sim2real* transition for machine learning controllers. 
+
+**Clarity:** 
+Really nicely written. 
+
+# Second Pass
+**What is the main thrust?**
+They use a simplex style controller setup with real time reachability to know when to use a optimal ML based controller vs. a safety oriented controller. They use the reachability to do this in real time, and demonstrate how different ML models line up against one another.
+
+**What is the supporting evidence?**
+They ran a whole bunch of experiments. They published all of the results, with their main metrics being Mean ML usage. 
+
+**What are the key findings?**
+The biggest findings are that when obstacles are introduced (or other general advesary behavior), the amount that the safety controller kicks in goes up by a lot. Sims can use around about 50+% ML controller based on the speed of the car, but when using the real track, the ML useage goes down below 20%. They also note their real track is much smaller than the simulation track.
+
+# Third Pass
+**Recreation Notes:**
+
+**Hidden Findings:**
+
+**Weak Points? Strong Points?**

Zettelkasten/Permanent Notes/Literature Notes/to_process/Reluplex- An Efficient SMT Solver for Verifying Deep Neural Networks-Note.md

@@ -0,0 +1,29 @@
+# First Pass
+**Category:** 
+Method
+
+**Context:** 
+Expanding SMT solvers to work with ReLU functions. They then applied this technology to a prototype DNN for a ACAS Xu (aircraft collision avoidance system for Autonomous Aircraft) system
+
+**Correctness:** 
+Seems good to me. Need to do deeper dive, can't really say correct or not at this point.
+
+**Contributions:** 
+Reluplex: a SMT algorithim that incorporates functionality for ReLU functions commonly found in DNN. This drastically impacts the types of networks that can be verified in scale.
+
+**Clarity:** 
+Well written and clear.
+
+# Second Pass
+**What is the main thrust?**
+
+**What is the supporting evidence?**
+
+**What are the key findings?**
+
+# Third Pass
+**Recreation Notes:**
+
+**Hidden Findings:**
+
+**Weak Points? Strong Points?**

Zettelkasten/Permanent Notes/Literature Notes/to_process/Remote nuclear microreactors- a preliminary economic evaluation of digital twins and centralized offsite control-Note.md

@@ -0,0 +1,34 @@
+# First Pass
+**Category:** 
+This is an economics research paper looking at how costs of microreactors will
+change with remote operation centers being introduced, and the proliferation
+of Digital Twins (DT)
+
+**Context:** 
+These are INL Researchers doing an LDRD. 
+
+**Correctness:** 
+A lot of dubious statements. Suspicious about their hailing of a digital twin as a 
+savior but they don't really address a lot of the cybersecurity concerns of 
+remote operation.
+
+**Contributions:** 
+Someone had to say the obvious that less control rooms will be less expensive
+to operate.
+
+**Clarity:** 
+Mediocre writing.
+
+# Second Pass
+**What is the main thrust?**
+
+**What is the supporting evidence?**
+
+**What are the key findings?**
+
+# Third Pass
+**Recreation Notes:**
+
+**Hidden Findings:**
+
+**Weak Points? Strong Points?**

Zettelkasten/Permanent Notes/Literature Notes/to_process/Runtime Safety Assurance Using Reinforcement Learning-Note.md

@@ -0,0 +1,35 @@
+# First Pass
+**Category:** 
+Simulation paper that talks about using a recovery controller in combination 
+with a nominal controller that is learned. The boundary to swtich between
+the two is a learned boundary.
+
+**Context:** 
+Drones
+
+**Correctness:** 
+Not very. They do really well in the intro and methodology, but shit hits the fan
+when it comes to the results. They don't explain things well, and also don't 
+really establish why their learned boundary between nominal and recovery
+controllers should be successful.
+
+**Contributions:** 
+The biggest contributions these guys make is demonstrating feasibility of their 
+reinforcement learned switching from the recovery controller and the nominal 
+controller.
+
+**Clarity:** 
+Well written until the whole thing came apart at the end.
+
+# Second Pass
+I read this a second time but I don't think it's worth it.
+
+Their main contribution is trying to use RL to learn when to switch to a 
+recovery controller. 
+
+# Third Pass
+**Recreation Notes:**
+
+**Hidden Findings:**
+
+**Weak Points? Strong Points?**

Zettelkasten/Permanent Notes/Literature Notes/to_process/Safe Reinforcement Learning via Shielding-Note.md

@@ -0,0 +1,29 @@
+# First Pass
+**Category:** 
+Method
+
+**Context:** 
+Making RL agents safe by 'shielding' - baking in specification checking into training by providing feedback to the network when an output (even while the system is live) produces an unsafe control
+
+**Correctness:** 
+Cited 1000+ times. I think it's correct.
+
+**Contributions:** 
+Shielding, a way to use RL in high assurance systems.
+
+**Clarity:** 
+Well written and easy to understand.
+
+# Second Pass
+**What is the main thrust?**
+
+**What is the supporting evidence?**
+
+**What are the key findings?**
+
+# Third Pass
+**Recreation Notes:**
+
+**Hidden Findings:**
+
+**Weak Points? Strong Points?**

Zettelkasten/Permanent Notes/Literature Notes/to_process/The Past, Present and Future of Cyber-Physical Systems- A Focus on Models-Note.md

@@ -0,0 +1,29 @@
+# First Pass
+**Category:** 
+Framework / Modelling 
+
+**Context:** 
+Showing that CPS can't be modeled like linear systems.
+
+**Correctness:** 
+Who knows.
+
+**Contributions:** 
+A big focus on **deterministic** models
+
+**Clarity:** 
+Some grammar mistakes and significant jabbering.
+
+# Second Pass
+**What is the main thrust?**
+
+**What is the supporting evidence?**
+
+**What are the key findings?**
+
+# Third Pass
+**Recreation Notes:**
+
+**Hidden Findings:**
+
+**Weak Points? Strong Points?**

Zettelkasten/Permanent Notes/Literature Notes/to_process/woodAutonomousControlFramework2017-notes.md

@@ -0,0 +1,3 @@
+# tee hee
+
+there is something here

Zettelkasten/Permanent Notes/Thesis/DR-20250826144307-heilmeier-questions.md

@@ -0,0 +1,39 @@
+---
+id: DR-20250826144307
+title: Heilmeier Questions
+type: thesis
+created: 2025-08-26T18:43:07Z
+modified: 2025-08-28T20:42:41Z
+tags: []
+---
+
+# Heilmeier Questions for my Thesis Topic
+
+**TITLE** 
+[[Thesis Title Ideas]]
+
+***High-Assurance Hybrid Controller Synthesis from Logical
+Specifications*** 
+
+## **What am I trying to do? No jargon!** 
+
+The goal of this research is to use formal methods to create
+hybrid controllers with provable guarantees of performance
+and safety. Hybrid control systems are control systems that
+have distinct changes in system dynamics under different
+conditions, which are often called modes. Modes are often
+defined by design requirements, and as such can be easily
+translated into formal specifications. This research will
+will eliminate the possible introduction of accidental
+errors while building controllers by automatically
+synthesizing the mode switching behavior from design
+requirements. Controller behavior within modes will be
+verified using reachability analysis.
+
+## **How is it done today?** 
+    
+## **What's new in my approach?** 
+
+## **Who cares?** 
+
+

Zettelkasten/Permanent Notes/Thesis/DR-20250826145452-title-ideas.md

@@ -0,0 +1,33 @@
+---
+id: DR-20250826145452
+title: Title Ideas
+type: thesis
+created: 2025-08-26T18:54:52Z
+modified: 2025-08-26T19:03:19Z
+tags: []
+---
+
+# Thesis Title Ideas
+
+## August 26th
+1. Hybrid Controller Synthesis from Logical Specifications
+
+2. Hybrid Mode Switching Controller Synthesis from
+   Regulatory Requirements as Logical Specifications
+
+3. Formally Verified Autonomous Hybrid Controller
+   Implementations Synthesized from Regulatory Requirements
+
+Okay so mixing these:
+
+*Formally Tractable Hybrid Controller Synthesis from Logical
+Specifications of Regulatory Requirements* 
+
+It's long. But Hybrid controller synthesis from logical
+specifications might not be enough? Also 'logical
+specifications of regulatory requirements' might not make
+much sense either. Y'know what, I think I like the first one
+best. I'm going with:
+
+***High-Assurance Hybrid Controller Synthesis from Logical
+Specifications***