This seems pointless, i.e. they might formalize the machine learning models (actually, the Lean code seems an AI-generated mix of Lean 3 and 4, probably doesn't compile), but the actual hard part is of course the proofs themselves, which they don't seem to solve.
Theorems of the kind "model X always does this desirable thing" are almost always false (because it's an imprecise model), and theorems of the kind "model X always does this desirable thing Y% of the time" seem incredibly hard to prove, probably impossible unless it's feasible to try the model on all possible inputs.
Even formulating the theorem itself is often extremely hard or impossible, e.g. consider things like "this LLM does not output false statements".
At least the author[0] seems to have some clout behind him. However, given that his code doesn't even compile and the premise seems massively over-stated, I wonder how his credentials (Stanford, etc) can even be genuine.
How do they deal with models with a stochastic element (most of generative AI)? Not sure how you intend to prove sampling. Are they going to perform (mathematical) analysis on every single normal distribution in the model?
I am very intrigued by this. It all seems AI generated. This same HN account posted another repo full of promises and which looks filled with AI generated stubs. What's going on? How did this reach the first page?
At least the author[0] seems to have some clout behind him. However, given that his code doesn't even compile and the premise seems massively over-stated, I wonder how his credentials (Stanford, etc) can even be genuine.
Cool that they work in this direction. We need NVIDIA, OS providers to at least have robust updatable blacklists of bad AI models (probably agentic ones) else hackers and rogue states will make a botnet of viruses with agentic components.
We’ll have no time for “AI antiviruses”, agency explosion (grabbing GPUs, compute time, tools) precedes intelligence explosion.
OS providers and NVIDIA must have skin in the game, feel responsible for bad models that run on its GPUs/OSes, fund safety research, same way Apple feels responsible for apps in its App Store and viruses on MacOS
This looks really interesting - Maybe someone with more knowledge on the subject could make a comparison with other frameworks and how far these guarantees can go? (e.g. fairness seems even ambiguous to define objectively)
>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
that's literally every single paper in academic CS (except theory). every claim is an exaggeration or lie by omission ("this only works on a small subset of ..."). every title is clickbait. every impl is worse than junior-level code. you become so jaded to it that you start to evaluate papers/projects based a premonition of what it could be rather than what it is.
At least the author[0] seems to have some clout behind him. However, given that his code doesn't even compile and the premise seems massively over-stated, I wonder how his credentials (Stanford, etc) can even be genuine.
Yeah, that was my thought too. Is this system formally verifying low-level stuff like, "if neurons A and B have a connection to neuron C, and A and B both fire, then..."?
It seems impossible to prove high-level things like "this computer vision system will never mis-identify a cat as a dog."
Theorems of the kind "model X always does this desirable thing" are almost always false (because it's an imprecise model), and theorems of the kind "model X always does this desirable thing Y% of the time" seem incredibly hard to prove, probably impossible unless it's feasible to try the model on all possible inputs.
Even formulating the theorem itself is often extremely hard or impossible, e.g. consider things like "this LLM does not output false statements".
[0] https://mateopetel.xyz/
[0] https://mateopetel.xyz/
We’ll have no time for “AI antiviruses”, agency explosion (grabbing GPUs, compute time, tools) precedes intelligence explosion.
OS providers and NVIDIA must have skin in the game, feel responsible for bad models that run on its GPUs/OSes, fund safety research, same way Apple feels responsible for apps in its App Store and viruses on MacOS
>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...
that's literally every single paper in academic CS (except theory). every claim is an exaggeration or lie by omission ("this only works on a small subset of ..."). every title is clickbait. every impl is worse than junior-level code. you become so jaded to it that you start to evaluate papers/projects based a premonition of what it could be rather than what it is.
[0] https://mateopetel.xyz/
It seems impossible to prove high-level things like "this computer vision system will never mis-identify a cat as a dog."