danesabo/Obsidian
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

vault backup: 2025-05-06 17:56:28

Browse Source
This commit is contained in:
Dane Sabo 2025-05-06 17:56:28 -04:00
parent e43bbbb187
commit 2cfa12c7ed
9 changed files with 173 additions and 46 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

40
.obsidian/graph.json vendored
View File

@ -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
}

3
.obsidian/plugins/colored-tags/data.json vendored
View File

@ -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
}

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

@ -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

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

@ -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

40
Literature Notes/Formal verification of neural network controlled autonomous systems.md Normal file
View File

@ -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

12
Literature Notes/Literature Note.md
View File

@ -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" -%}

25
Neural Network Formal Methods/NNFM Ontology.canvas
View File

@ -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"}
]
}

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

@ -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?**

31
Paper Queue.md Normal file
View File

@ -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)
```