>This repository provides a framework for specifying and proving properties—such as robustness, fairness, and interpretability—of machine learning models using Lean 4
FV of AI systems is hard and this repo massively oversells itself. The Lean code itself is weird (AI generated?) and the "fairness" example proves that if a (linear) classifier always returns "yes" then the percentage of people classified as "yes" is the same across all demographics which isn't meaningful since this percentage is 100% for every possible group of people.
I was watching a video [1] the other day about the challenges FV faces for AI if it's something you're be interested in. I'm not really familiar with FV for neural networks and not sure what progress looks like in the field but I know ANSR [2] and TIAMAT [3] are doing related things
>This repository provides a framework for specifying and proving properties—such as robustness, fairness, and interpretability—of machine learning models using Lean 4
FV of AI systems is hard and this repo massively oversells itself. The Lean code itself is weird (AI generated?) and the "fairness" example proves that if a (linear) classifier always returns "yes" then the percentage of people classified as "yes" is the same across all demographics which isn't meaningful since this percentage is 100% for every possible group of people.
I was watching a video [1] the other day about the challenges FV faces for AI if it's something you're be interested in. I'm not really familiar with FV for neural networks and not sure what progress looks like in the field but I know ANSR [2] and TIAMAT [3] are doing related things
[1]: https://www.youtube.com/watch?v=bs5snugP1VA
[2]: https://www.darpa.mil/research/programs/assured-neuro-symbol...
[3]: https://www.darpa.mil/research/programs/transfer-from-imprec...