From 2cfa12c7ed0a59c3bb96194f5003b4c2e246ddcd Mon Sep 17 00:00:00 2001 From: Dane Sabo Date: Tue, 6 May 2025 17:56:28 -0400 Subject: [PATCH] vault backup: 2025-05-06 17:56:28 --- .obsidian/graph.json | 40 +++--------------- .obsidian/plugins/colored-tags/data.json | 3 +- ...mal Methods applied to Machine Learning.md | 42 ++++++++++++++++++- ...esis - Challenges and Future Directions.md | 9 ++-- ...l network controlled autonomous systems.md | 40 ++++++++++++++++++ Literature Notes/Literature Note.md | 12 ++++-- .../NNFM Ontology.canvas | 25 +++++++++-- ...mal Methods applied to Machine Learning.md | 17 ++++++++ Paper Queue.md | 31 ++++++++++++++ 9 files changed, 173 insertions(+), 46 deletions(-) create mode 100644 Literature Notes/Formal verification of neural network controlled autonomous systems.md create mode 100644 Paper Queue.md diff --git a/.obsidian/graph.json b/.obsidian/graph.json index 59e9868d..ba672c93 100755 --- a/.obsidian/graph.json +++ b/.obsidian/graph.json @@ -1,56 +1,28 @@ { "collapse-filter": false, - "search": "-\"Readme\" -\"Weekly\" -path:\"1 Daily Notes\" -path:\"900s Calendars\" ", + "search": "", "showTags": false, "showAttachments": false, "hideUnresolved": false, "showOrphans": true, - "collapse-color-groups": true, + "collapse-color-groups": false, "colorGroups": [ { - "query": "path:\"4 Qualifying Exam\" ", - "color": { - "a": 1, - "rgb": 16767785 - } - }, - { - "query": "path:\"200 Library Papers\" ", + "query": "path:\"Library Papers\" ", "color": { "a": 1, "rgb": 10100099 } }, { - "query": "path:\"5 Thesis\" ", + "query": "path:\"Thesis\" ", "color": { "a": 1, "rgb": 59041 } }, { - "query": "file:README", - "color": { - "a": 1, - "rgb": 16711744 - } - }, - { - "query": "path:\"300s School\" ", - "color": { - "a": 1, - "rgb": 6054102 - } - }, - { - "query": "path:\"3-99 Research\" ", - "color": { - "a": 1, - "rgb": 5419488 - } - }, - { - "query": "path:\"9999 Personal/Z\" ", + "query": "path:\"Personal/Z\" ", "color": { "a": 1, "rgb": 2653655 @@ -67,6 +39,6 @@ "repelStrength": 20, "linkStrength": 0.723958333333333, "linkDistance": 30, - "scale": 0.0889892578125, + "scale": 0.3003387451171875, "close": true } \ No newline at end of file diff --git a/.obsidian/plugins/colored-tags/data.json b/.obsidian/plugins/colored-tags/data.json index 496f6807..77320f71 100755 --- a/.obsidian/plugins/colored-tags/data.json +++ b/.obsidian/plugins/colored-tags/data.json @@ -225,7 +225,8 @@ "InFirstPass": 213, "ToRead": 214, "Computer-Science---Logic-in-Computer-Science": 215, - "Computer-Science---Programming-Languages": 216 + "Computer-Science---Programming-Languages": 216, + "dead": 217 }, "_version": 3 } \ No newline at end of file diff --git a/Literature Notes/A Review of Formal Methods applied to Machine Learning.md b/Literature Notes/A Review of Formal Methods applied to Machine Learning.md index 5492f9ba..d1bb865e 100644 --- a/Literature Notes/A Review of Formal Methods applied to Machine Learning.md +++ b/Literature Notes/A Review of Formal Methods applied to Machine Learning.md @@ -6,9 +6,9 @@ authors: - "Miné, Antoine" citekey: "urbanReviewFormalMethods2021" +publish_date: 2021-04-21 +last_import: 2025-05-06 --- -Imported: 2025-05-06 4:59 pm -Accessed: 2025-03-31 3:11 pm # Indexing Information **DOI** @@ -19,6 +19,7 @@ Accessed: 2025-03-31 3:11 pm #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 > @@ -28,6 +29,43 @@ Accessed: 2025-03-31 3:11 pm ![[Paper Notes/A Review of Formal Methods applied to Machine Learning.md]] ## Highlights From Zotero +>[!tip] Brilliant +> Recent advances in artificial intelligence and machine learning and the availability of vast amounts of data allow us to develop computer software that efficiently and autonomously perform complex tasks that are difficult or even impossible to design using traditional explicit programming (e.g., image classification, speech recognition, etc.). This makes machine-learned software particularly attractive even in safetycritical applications, as it enables performing a whole world of new functions that could not be envisioned before +> 2025-05-06 5:03 pm + +>[!warning] Dubious +> Safety-critical applications require an extremely high level of insurance that the software systems behave correctly and reliably. +> 2025-05-06 5:04 pm + + +>[!highlight] Highlight +> In contrast, research in formal methods for the development and assurance of machine learning systems remains today extremely limited. It is however rapidly gaining interest and popularity, mostly driven by the growing needs of the automotive and avionics industries. +> 2025-05-06 5:07 pm + +>[!highlight] Highlight +> Specifically, in the following, we give an introduction to formal methods (Section 2) with a particular focus on static analysis by abstract interpretation [37], as it offers a unifying theory for reasoning about disparate formal verification approaches (Section 2.3). +> 2025-05-06 5:07 pm + +>[!highlight] Highlight +> Another interesting possibility is to develop approaches to determine constraints on the training process that enforce a desired property on the trained model. For instance, one could enforce a specific behavior for a given input range of interest, or a particular structure of the trained model that facilitates its subsequent verification [171] (or its abstraction for verification [125, 145, 62]). +> 2025-05-06 5:10 pm + +>[!highlight] Highlight +> More generally, verification methods should allow verifying the behavior of trained models under all circumstances and not just over the expected safe input space. This is particularly useful in cases in which the trained model is part of a larger machine learning-based system [53] and is thus more susceptible to receive unexpected inputs, e.g., from malfunctioning sensors +> 2025-05-06 5:11 pm + +>[!highlight] Highlight +> In this case, it would be useful to design verification methods able to relate the behavior of the inexact model to the optimal expected behavior, e.g., by determining the worst-case approximation of the trained model. +> 2025-05-06 5:12 pm + +>[!highlight] Highlight +> Finally, there is a need for further approaches that support diverse model structures, such as recurrent neural networks [95, 175], and that can verify model implementations by taking floating-point rounding errors into account [140, 141, 105]. +> 2025-05-06 5:13 pm + ## Follow-Ups +>[!example] + >For instance, they are used at an industrial level in avionics [146], where the development processes of aircraft software systems have very stringent assurance and verification requirements mandated by international standards (i.e., DO-178C). + >- [ ] #Follow-Up + diff --git a/Literature Notes/Enhancing Cyber-Physical System Dependability via Synthesis - Challenges and Future Directions.md b/Literature Notes/Enhancing Cyber-Physical System Dependability via Synthesis - Challenges and Future Directions.md index 426fd99f..e4c845cc 100644 --- a/Literature Notes/Enhancing Cyber-Physical System Dependability via Synthesis - Challenges and Future Directions.md +++ b/Literature Notes/Enhancing Cyber-Physical System Dependability via Synthesis - Challenges and Future Directions.md @@ -6,10 +6,10 @@ authors: - "Amorim, Arthur" citekey: "taylorEnhancingCyberPhysicalSystem2025" +publish_date: 2025-06-23 location: "Naples, Italy" +last_import: 2025-05-06 --- -Imported: 2025-05-06 4:57 pm -Accessed: 2025-05-05 12:00 am # Indexing Information @@ -18,6 +18,7 @@ Accessed: 2025-05-05 12:00 am #InFirstPass + >[!seealso] Related Papers > @@ -25,9 +26,11 @@ 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>[!done] Important +## 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 diff --git a/Literature Notes/Formal verification of neural network controlled autonomous systems.md b/Literature Notes/Formal verification of neural network controlled autonomous systems.md new file mode 100644 index 00000000..15d4bffa --- /dev/null +++ b/Literature Notes/Formal verification of neural network controlled autonomous systems.md @@ -0,0 +1,40 @@ +--- +authors: + + - "Sun, Xiaowu" + + - "Khedr, Haitham" + + - "Shoukry, Yasser" + +citekey: "sunFormalVerificationNeural2019" +publish_date: 2019-04-16 +publisher: "Association for Computing Machinery" +location: "New York, NY, USA" +pages: 147–156 +last_import: 2025-05-06 +--- + +# Indexing Information +**DOI** +[10.1145/3302504.3311802](https://doi.org/10.1145/3302504.3311802) +**ISBN** +[978-1-4503-6282-5](https://www.isbnsearch.org/isbn/978-1-4503-6282-5) + + + +#ToRead + + +>[!Abstract] +>In this paper, we consider the problem of formally verifying the safety of an autonomous robot equipped with a Neural Network (NN) controller that processes LiDAR images to produce control actions. Given a workspace that is characterized by a set of polytopic obstacles, our objective is to compute the set of safe initial states such that a robot trajectory starting from these initial states is guaranteed to avoid the obstacles. Our approach is to construct a finite state abstraction of the system and use standard reachability analysis over the finite state abstraction to compute the set of safe initial states. To mathematically model the imaging function, that maps the robot position to the LiDAR image, we introduce the notion of imaging-adapted partitions of the workspace in which the imaging function is guaranteed to be affine. Given this workspace partitioning, a discrete-time linear dynamics of the robot, and a pre-trained NN controller with Rectified Linear Unit (ReLU) non-linearity, we utilize a Satisfiability Modulo Convex (SMC) encoding to enumerate all the possible assignments of different ReLUs. To accelerate this process, we develop a pre-processing algorithm that could rapidly prune the space of feasible ReLU assignments. Finally, we demonstrate the efficiency of the proposed algorithms using numerical simulations with the increasing complexity of the neural network controller.>[!seealso] Related Papers +> + +# Annotations +## Notes +![[Paper Notes/Formal verification of neural network controlled autonomous systems.md]] + +## Highlights From Zotero + +## Follow-Ups + diff --git a/Literature Notes/Literature Note.md b/Literature Notes/Literature Note.md index 8eb9da01..d6d3014d 100755 --- a/Literature Notes/Literature Note.md +++ b/Literature Notes/Literature Note.md @@ -6,6 +6,7 @@ authors: {% endfor -%} {% endfor %} citekey: "{{ citekey }}" +publish_date: {{ date | format("YYYY-MM-DD") }} {% if itemType == "journalArticle" -%} journal: "{{ publicationTitle }}" {% endif -%} @@ -27,9 +28,8 @@ location: "{{ place }}" {% if pages -%} pages: {{ pages }} {% endif -%} +last_import: {{ importDate | format("YYYY-MM-DD") }} --- -Imported: {{ importDate | format("YYYY-MM-DD h:mm a") }} -Accessed: {{ accessDate | format("YYYY-MM-DD h:mm a")}} # Indexing Information {% if DOI -%} @@ -56,6 +56,7 @@ Accessed: {{ accessDate | format("YYYY-MM-DD h:mm a")}} }}{% if not loop.last -%}, {% endif %}{% endfor %} {% set in_read = 0 -%} +{% set dead = false -%} {%- for collection in collections -%} {%- if collection.name == "! 3. Grok'd" -%} {%- set in_read = 3 -%} @@ -63,6 +64,8 @@ Accessed: {{ accessDate | format("YYYY-MM-DD h:mm a")}} {%- set in_read = 2 -%} {%- elif collection.name =="! 1. First Pass" -%} {%- set in_read = 1 -%} + {%- elif collection.name == "! dead" -%} + {%- set dead = true -%} {%- endif -%} {%- endfor -%} @@ -75,6 +78,9 @@ Accessed: {{ accessDate | format("YYYY-MM-DD h:mm a")}} {% elif in_read == 0%} #ToRead {%- endif %} +{% if dead == true %} +#dead +{%- endif%} {% if abstractNote -%} >[!Abstract] @@ -94,7 +100,7 @@ Accessed: {{ accessDate | format("YYYY-MM-DD h:mm a")}} ## Highlights From Zotero {#- Process non-Purple highlights -#} {% for a in annotations -%} -{% if (a.type == "highlight" or a.type == "underline") and a.colorCategory != "Purple" -%} +{% if (a.type == "highlight" or a.type == "underline") and a.colorCategory != "Purple" %} {% if a.colorCategory == "Blue" -%} >[!tip] Brilliant {% elif a.colorCategory == "Green" -%} diff --git a/Neural Network Formal Methods/NNFM Ontology.canvas b/Neural Network Formal Methods/NNFM Ontology.canvas index 27933d42..39684138 100644 --- a/Neural Network Formal Methods/NNFM Ontology.canvas +++ b/Neural Network Formal Methods/NNFM Ontology.canvas @@ -1,7 +1,26 @@ { "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"} + {"id":"5e184d3db8adc84a","x":-1000,"y":-585,"width":250,"height":60,"type":"text","text":"NEWER"}, + {"id":"ce7357ee8c8c4a0c","x":-330,"y":1400,"width":250,"height":60,"type":"text","text":""}, + {"id":"bbe4a58a5af748eb","x":-1000,"y":920,"width":250,"height":60,"type":"text","text":"OLDER"}, + {"id":"6b62b3a19b06fc0a","type":"file","file":"Literature Notes/A Review of Formal Methods applied to Machine Learning.md","x":490,"y":-120,"width":420,"height":400,"color":"3"}, + {"id":"bac68ab8fa2c1c9b","type":"file","file":"Literature Notes/Formal verification of neural network controlled autonomous systems.md","x":-40,"y":520,"width":400,"height":400,"color":"1"}, + {"id":"35eebdf6214c8c88","type":"text","text":"# Machine Learning","x":185,"y":-760,"width":440,"height":80}, + {"id":"cdbcb13db184af6e","type":"text","text":"## Neural Networks","x":185,"y":-312,"width":250,"height":100}, + {"id":"bcc9c2b5dc701338","type":"text","text":"# Formal Methods","x":-480,"y":-759,"width":440,"height":80}, + {"id":"684196d797ac66e3","type":"file","file":"Literature Notes/Enhancing Cyber-Physical System Dependability via Synthesis - Challenges and Future Directions.md","x":-720,"y":-462,"width":480,"height":400,"color":"3"}, + {"id":"f9208a6e4a7ef241","x":-653,"y":-592,"width":346,"height":74,"type":"text","text":"## Linear Temporal Logic"}, + {"id":"6d8080147062d756","type":"text","text":"## Control Systems","x":-80,"y":-640,"width":250,"height":85} ], - "edges":[] + "edges":[ + {"id":"96f75a4631d60661","fromNode":"bcc9c2b5dc701338","fromSide":"bottom","toNode":"6b62b3a19b06fc0a","toSide":"top"}, + {"id":"bc94b9297ce2103a","fromNode":"6d8080147062d756","fromSide":"bottom","toNode":"bac68ab8fa2c1c9b","toSide":"top"}, + {"id":"766a32fa431c6398","fromNode":"bcc9c2b5dc701338","fromSide":"bottom","toNode":"bac68ab8fa2c1c9b","toSide":"top"}, + {"id":"cac141857b18b1d4","fromNode":"cdbcb13db184af6e","fromSide":"bottom","toNode":"bac68ab8fa2c1c9b","toSide":"top"}, + {"id":"25f8b04d82996c32","fromNode":"bbe4a58a5af748eb","fromSide":"top","toNode":"5e184d3db8adc84a","toSide":"bottom"}, + {"id":"4c55047c849221b0","fromNode":"35eebdf6214c8c88","fromSide":"bottom","toNode":"cdbcb13db184af6e","toSide":"top"}, + {"id":"8e7231a4f14bca4a","fromNode":"35eebdf6214c8c88","fromSide":"bottom","toNode":"6b62b3a19b06fc0a","toSide":"top"}, + {"id":"c9fd438ad36d91b7","fromNode":"bcc9c2b5dc701338","fromSide":"bottom","toNode":"f9208a6e4a7ef241","toSide":"top"}, + {"id":"941d0f5178c0c38c","fromNode":"f9208a6e4a7ef241","fromSide":"bottom","toNode":"684196d797ac66e3","toSide":"top"} + ] } \ No newline at end of file diff --git a/Paper Notes/A Review of Formal Methods applied to Machine Learning.md b/Paper Notes/A Review of Formal Methods applied to Machine Learning.md index c8928910..c51745f6 100644 --- a/Paper Notes/A Review of Formal Methods applied to Machine Learning.md +++ b/Paper Notes/A Review of Formal Methods applied to Machine Learning.md @@ -1,9 +1,26 @@ # 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 **What is the main thrust?** diff --git a/Paper Queue.md b/Paper Queue.md new file mode 100644 index 00000000..e0f14aab --- /dev/null +++ b/Paper Queue.md @@ -0,0 +1,31 @@ +**Waiting for first pass:** +```dataview +table file.name as "Paper", authors as "Authors", publish_date as "Date Published", last_import as "Date Imported" +from #ToRead +sort publish_date desc +where file.name != "Literature Note" +``` + +**Waiting for second pass:** +```dataview +table file.name as "Paper", authors as "Authors", publish_date as "Date Published", last_import as "Date Read" +from #InFirstPass +sort publish_date desc +where file.name != "Literature Note" +``` + +**Waiting for third pass:** +```dataview +table file.name as "Paper", authors as "Authors", publish_date as "Date Published", last_import as "Date Read" +from #InSecondPass +sort publish_date desc +where file.name != "Literature Note" +``` + +**Recently read:** +```dataview +table file.name as "Paper", authors as "Authors", publish_date as "Date Published", last_import as "Date Read" +from "Literature Notes" +sort publish_date desc +where last_import >= date(today) - dur(7day) +```