NASEM webinar 4/23-4/25

Stream: Machine Learning for Theorem Proving

[Matthew Ballard]

My main takeaway from the first talk (all errors in interpretation of course my fault :)

Chlipala: metavariable creation and unification, as in Lean/Coq, is too expensive for verification across the full hardware/software stack.

[Mario Carneiro]

Hm, I'm disappointed that I missed this talk, are the slides or recording available anywhere?

[Matthew Ballard]

I believe these will be made available publicly but @Talia Ringer (who is moderating currently) will know better

[Adam Topaz]

I assume the recording will also be made public.

[Richard Osborn]

I believe this is the link to the event. Seems like you can rewind the webcast to see the talk?

[Matthew Ballard]

Oh great.

Btw, below is a screen capture of the slide I was referring to
Bad asymptotics for metavariable creation

This is something I was totally unaware of. I am not sure where the figure is from.

[Mario Carneiro]

I don't understand how the claim could be true, adding a new metavariable in lean is effectively constant time (more precisely, it's the cost of inserting into a PersistentHashMap)

[Mario Carneiro]

so surely there is some other aspect of this that is rolled into the cost

[Mario Carneiro]

I could understand if it was talking about adding new things to the LocalContext, this is known to be asymptotically bad (see Jason Gross's thesis). But metavariables are quite cheap to create, and less cheap to assign (because of the occurs check)

[Matthew Ballard]

I think the data is only from Coq. I interpreted it to include the assignment also but that may have been reading too much into it

[Mario Carneiro]

yes, Coq and Lean are significantly different under the hood so it's difficult to make blanket statements of this form

[Mario Carneiro]

that's not to say that Lean is actually doing better on this point, only that the places that are unnecessarily slow are somewhat different between them

[Mario Carneiro]

e.g. Qed is really slow in coq but this is basically never an issue in lean, because lean doesn't implement variables and sections in the same way

[Matthew Ballard]

Hold music is fresh.