vault backup: 2025-05-06 17:02:17

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

@@ -223,7 +223,9 @@
     "To_Read": 211,
     "InSecondPass": 212,
     "InFirstPass": 213,
-    "ToRead": 214
+    "ToRead": 214,
+    "Computer-Science---Logic-in-Computer-Science": 215,
+    "Computer-Science---Programming-Languages": 216
   },
   "_version": 3
 }

Literature Notes/A Review of Formal Methods applied to Machine Learning.md

@@ -0,0 +1,33 @@
+---
+authors:
+
+  - "Urban, Caterina"
+  
+  - "Miné, Antoine"
+  
+citekey: "urbanReviewFormalMethods2021"
+---
+Imported: 2025-05-06 4:59 pm
+Accessed: 2025-03-31 3:11 pm
+
+# Indexing Information
+**DOI**
+[10.48550/arXiv.2104.02466](https://doi.org/10.48550/arXiv.2104.02466)
+#Computer-Science---Logic-in-Computer-Science, #Computer-Science---Machine-Learning, #Computer-Science---Programming-Languages
+
+
+#InFirstPass
+
+
+>[!Abstract]
+>We review state-of-the-art formal methods applied to the emerging field of the verification of machine learning systems. Formal methods can provide rigorous correctness guarantees on hardware and software systems. Thanks to the availability of mature tools, their use is well established in the industry, and in particular to check safety-critical applications as they undergo a stringent certification process. As machine learning is becoming more popular, machine-learned components are now considered for inclusion in critical systems. This raises the question of their safety and their verification. Yet, established formal methods are limited to classic, i.e. non machine-learned software. Applying formal methods to verify systems that include machine learning has only been considered recently and poses novel challenges in soundness, precision, and scalability. We first recall established formal methods and their current use in an exemplar safety-critical field, avionic software, with a focus on abstract interpretation based techniques as they provide a high level of scalability. This provides a golden standard and sets high expectations for machine learning verification. We then provide a comprehensive and detailed review of the formal methods developed so far for machine learning, highlighting their strengths and limitations. The large majority of them verify trained neural networks and employ either SMT, optimization, or abstract interpretation techniques. We also discuss methods for support vector machines and decision tree ensembles, as well as methods targeting training and data preparation, which are critical but often neglected aspects of machine learning. Finally, we offer perspectives for future research directions towards the formal verification of machine learning systems.>[!seealso] Related Papers
+>
+
+# Annotations
+## Notes
+![[Paper Notes/A Review of Formal Methods applied to Machine Learning.md]]
+
+## Highlights From Zotero
+
+## Follow-Ups
+

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

@@ -8,14 +8,15 @@ authors:
 citekey: "taylorEnhancingCyberPhysicalSystem2025"
 location: "Naples, Italy"
 ---
-Imported: 2025-05-06 3:46 pm
+Imported: 2025-05-06 4:57 pm
 Accessed: 2025-05-05 12:00 am
 
 # Indexing Information
 
 
 
-#ToRead
+#InFirstPass
+
 
 >[!seealso] Related Papers
 >
@@ -24,7 +25,18 @@ Accessed: 2025-05-05 12:00 am
 ## Notes
 ![[Paper Notes/Enhancing Cyber-Physical System Dependability via Synthesis- Challenges and Future Directions.md]]
 
-## Highlights From Zotero
+## Highlights From Zotero>[!done] Important
+> By formally designing safety and liveness requirements and synthesizing software that adheres to these specifications, unsafe behaviors can be prevented from the very beginning of system development.
+> 2025-05-06 4:37 pm
+>[!warning] Dubious
+> Preventing unsafe behaviors is achievable by meticulously engineering control software to prevent such behaviors. However, software often contains bugs that adversaries can exploit. Preventing bugs involves specifying the correct behavior of the system and proving that the software implementation adheres to the specification. However, these program verification-based approaches are challenging to apply [5], [9], [24].
+> 2025-05-06 4:44 pm
+> *Bugs r bad. Basically the main point.
+
+
+These citations don't really support the claim that they're attached to.*
+
+
 
 ## Follow-Ups
 

Neural Network Formal Methods/NNFM Ontology.canvas

@@ -1 +1,7 @@
-{}
+{
+	"nodes":[
+		{"id":"bcc9c2b5dc701338","x":-420,"y":-460,"width":600,"height":80,"type":"text","text":"# Papers about Controller Synthesis"},
+		{"id":"684196d797ac66e3","x":-420,"y":-320,"width":480,"height":400,"color":"3","type":"file","file":"Literature Notes/Enhancing Cyber-Physical System Dependability via Synthesis - Challenges and Future Directions.md"}
+	],
+	"edges":[]
+}

Paper Notes/A Review of Formal Methods applied to Machine Learning.md

@@ -0,0 +1,20 @@
+# First Pass
+**Category:** 
+**Context:** 
+**Correctness:** 
+**Contributions:** 
+**Clarity:** 
+
+# 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?**