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?
Hmmm, there're no scientific work that really let's you do these things right now. And the repo doesn't cite any work, no associated paper.
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)
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 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".