SupGen

Stream: general

[Jason Rute]

@Victor Maia released a demo for a symbolic theorem prover called SupGen for (dependent?) type theory. See the post below for a demo video.

https://x.com/VictorTaelin/status/1881088337408377007
https://x.com/VictorTaelin/status/1881392823246729640

[Jason Rute]

I think out of the Lean projects, it is most similar to Canonical (@Chase Norman), but probably holds a similar space to Duper (@Josh Clune) and LeanSMT (@Abdalrhman M Mohamed). And to be honest, I have no idea how it works or if it is any good.

[Jason Rute]

Victor talks a lot about how this sort of thing could be used in place of neural AI. While I think he has some points on symbolic AI not being given enough credit, I also think something like this alone would have a limited use case. But it would be fun to find ways to test this (and the other symbolic solvers) out.

[Jason Rute]

There was a previous discussion on this sort of thing at #general > Duper and Program Synthesis

[Chase Norman]

I can confirm that at a high level we appear to be building the same functionality.

[Adam Topaz]

The link above doesn’t seem to work for me. Is there another link I could try?

[Jason Rute]

he deleted it for now: https://x.com/VictorTaelin/status/1881135609823289766

[Jason Rute]

Hopefully, he will post a new one soon.

[Adam Topaz]

https://x.com/VictorTaelin/status/1881392823246729640

[Gridiron Player]

Why a limited usecase?

[Jason Rute]

@Gridiron Player It doesn't have premise/lemma selection, so I can't see how it would be able to find and use relevant theorems and definitions in a library. It wouldn't make sense to prove everything from axioms/definitions. (The cut elimination theorem says that doing so can lead to more than exponential increases in proof size.) But at the same time, other symbolic solvers have the same problem and the solution is just to build a machine learning lemma selector. So if it had that, or if it was narrowly used in cases where the lemmas are known, then it could be powerful. (Similarly with Canonical, Duper, and LeanSAT.) Indeed if it could be hooked up to Auto then it could take advantage of whatever lemma selector is planned for auto. (Auto IIRC is an interface between Lean and symbolic solvers.)

[Jason Rute]

Of course, this is more opinion than fact, and I'd be happy to be proved wrong.

[Gridiron Player]

Thats probably a question for Victor, but couldn't you just wrap already existing theorems as a type and use them for search?

Just me thinking out loud here. I have no idea.

[Jason Rute]

Happy to have Victor (@Victor Maia) engage here. (Also, here is a recent reply of mine to him on X: https://x.com/JasonRute/status/1882393233701171671)

[Gridiron Player]

In programming its kind of the same problem. You need to be able to synthesize functions that use other functions. I was under the assumption that that will be possible with SupGen. If not, then it might be of limited usability.

[Abdalrhman M Mohamed]

Gridiron Player said:

Thats probably a question for Victor, but couldn't you just wrap already existing theorems as a type and use them for search?

Just me thinking out loud here. I have no idea.

Yes. All of those tactics use theorem types for search. It's just a question of which existing theorem is going to be useful. Any ATP will get lost in proof search if it gets overwhelmed with a large search space if given useless theorems (though some are more robust to this others)

[Gridiron Player]

Isn't that what Victor's HVM solves for? It's fast... HVM is kind of what makes SupGen so special, not the proof synthesis itself.

[Gridiron Player]

https://github.com/HigherOrderCO/HVM

[Gridiron Player]

https://x.com/VictorTaelin/status/1876458776980578596/photo/1

[Gridiron Player]

See explanation video about interaction nets on https://higherorderco.com/

[Jason Rute]

Victor is a good salesman, but it is hard to evaluate twitter posts. The idea isn't completely novel, as for example @Chase Norman's Canonical is similar. But maybe it is underexplored and maybe he has good ideas and tech. Also the current performance is hard to evaluate. There is no technical report/paper with benchmarks that I'm aware of. And it isn't clear that it is available to use.

[Jason Rute]

As for interaction nets, they have been discussed here before: #general > Kind lang

[Chase Norman]

(deleted)

[Gridiron Player]

Oh okay. Understood.

[Abdalrhman M Mohamed]

This is the first time I've encountered HVM. From what I read, it's not clear to me why or how it can improve proof search or type checking...

[Gridiron Player]

I guess we'll see how it plays out. I don't have the time to do a deep dive into interaction nets. All I understand is that he claims that HVM makes program synthesis / type checking faster, as well as everything else that can be parallelized.

[Jason Rute]

(Actually, maybe I'm mistaken about no benchmarks. Victor mentions something on X about it, https://x.com/VictorTaelin/status/1882171887704236227, but it is hard to skim through a 30-minute video.)

[Victor Maia]

(this this how you reply a thread here? zulip is so confusing)

just to clarify, the speedup doesn't come from parallelism, but from HVM's beta optimality. we use superpositions to share computations on the enumerated space. we tested against SOTA program synthesizers "by example" and it is considerably faster. I'm not focused on ATP yet as I want to first optimize for this use case. it will take a while for a paper and benchmarks, but it will come. this was an early demo. yes, it is similar to Canonical, and I expect it will greatly outperform it, for the same reasons it outperforms all other bruteforce-like solutions for program synthesis by example. but don't quote me on it until there is a paper...

[Jason Rute]

Welcome, and thanks for the engagement! I look forward to the paper.

[Jason Rute]

@Victor Maia For SOTA program synthesizers, does that include LELO? https://arxiv.org/abs/2310.19791

[Jason Rute]

Also, when you get to theorem proving (and maybe also program synthesis), how do you handle having a large library of possibly relevant theorems and definitions? Or are you side stepping this for now?

[Jason Rute]

For example, in program synthesis is there any context besides the definitions used in the type signature?

[Victor Maia]

@Jason Rute no, I'm specifically comparing to LLM-free synthesizers. I believe that extending this with the ability to learn will outperform LLMs, but this isn't what we have (yet).

[Victor Maia]

@Jason Rute you can use a context! So yes, this is compatible with a library of relevant theorems and definitions; it significantly speeds up the search, and your definitions compute optimally, so it is really, really fast at that. That's how we expect to beat LLMs (by dynamically learning such library, which would be the "model").

[Victor Maia]

Note that our synthesizer can already prove theorems (because it is just an enumerator in a dependently typed language), but that was almost by accident; there are some minor things missing to make this useful for APT (like the ability to synthesize types, which I didn't implement yet since I was focusing on programs by example). That's not hard to add though

[Victor Maia]

There are some important limitations though, currently we only recurse via folds etc., and it only finds linear programs.

[Jason Rute]

Lean has decrimination tree for searching over the full global context. It is used in tactics like apply? and exact? Are you using something similar? Also when you do ATP, can it be hooked up to Lean with an interface similar to what Canonical will use?

[Victor Maia]

there is no discrimination tree, the apply/exact tactics merely select from a superposition of the entire library - no fancy structure. there is no unification either (as usually understood); instead, metavariables are just superpositions of all possible terms of their type. due to optimal evaluation, every branch that doesn't type-check is discarded efficiently, so I believe we don't need a hardcoded structure to get the desired asymptotics. that said, adding one might be an interesting experiment to try, although I suspect it will be an anti-optimization due to the overhead of the tree itself...

I'm not very familiar with Lean or the interface that Canonical will use, but it is a separate language / type checker, so there would need to be some translation layer from Lean to SupGen and back for it to work?

[Gridiron Player]

@Victor Maia Im confused on the part where you said that SupGen can dybamically learn the Lean Library. I thought it would just be an enumerator. How so without deep learning?

Would the library contents just be added as a type or something?

Update: Nevermind, you said you would add the library as a superposition which is also really fast obviously

[Jason Rute]

What do you mean “added as a type”?

[Gridiron Player]

@Jason Rute I misunderstood it. I reread his post and realized that all the theorems will just be added in a superposition.

@Victor Maia Can you add superpositions to another superposition "recursively"?

Like

(1 , (2,3))

or would that not be necessary to add theorems to superpositions?

[Gridiron Player]

Nevermind, realizing that superpositions are (I think) just a result of how computations are shared in an inet, I think my question doesnt matter as much, as a theorem definition would just be added as computations to the graph, Im assuming.

Im a noob, just thinking outloud here lol.

[Jared green]

what does superpostition mean in this case?

[Alex Meiburg]

https://x.com/VictorTaelin/status/1884971947131314319?t=MSciy6PxTTK5uDbkOGhPyA&s=19

Very sorry to see this. I assume "not open source" also means "only available as a service over the Internet", which would definitely make this much less exciting.

[Chase Norman]

(deleted)

[Kim Morrison]

(Could I suggest not posting screenshots without explanation of what they are, or why you are posting them?)