Lean Verifier ie Formal verification of ML Models

Stream: Machine Learning for Theorem Proving

[Robert]

Has anyone taken a look at this: https://github.com/fraware/leanverifier? It seems interesting, what are your all thoughts on this? Not sure if the main author is on the zulip channel to tag him.

[Kim Morrison]

The demo app is just a web app mockup, where everything is just a link back to repo?

[Matteo Cipollina]

Robert ha scritto:

Has anyone taken a look at this: https://github.com/fraware/leanverifier? It seems interesting, what are your all thoughts on this? Not sure if the main author is on the zulip channel to tag him.

interesting but it seems to be at an early stage and uses mixed Lean3/Lean 4 syntax, I'm not sure it compiles

[Alex Meiburg]

I was curious about their definition of "robustness" of a model:

/--
Robust classification property:
A classification function f is robust at level ε if any two inputs within ε (L2 norm) yield the same output.
--/
def robustClass (f : Array Float → Nat) (ε : Float) : Prop :=
  ∀ (x x' : Array Float), distL2 x x' < ε → f x = f x'

So you can perturb the input by an vector of norm at most ε and the output must be unchanged. But ... that implies that the function is constant, because you can just keep perturbing by ε and over. I was even more confused when they actually proved that some model was robust, in the same repo! But it turns out that they assumed, as axioms, that the model was (1) Lipschitz, and (2) has a margin property. Lipschitz implies that it's a continuous function. The margin property states that the classifier is always at least 0.1, or at most -0.1. But if you take a continuous function with the margin property, then it must also be a constant classifier. So the proof checks out!

[Alex Meiburg]

but the pipeline on a whole looks like a pretty neat idea, a good way to "import" models from a JSON to Lean, and then you can write proofs about them? but it looks pretty early