Duper - Josh Clune

Stream: Lean Together 2024

[Max Nowak 🐉]

@David Thrane Christiansen Question to Josh: It is possible to translate Fin, Vec, etc into just HOL + a wellformedness predicate. Sounds like duper doesn't do this (yet)? Or does it result in ugly translated problems which are very inefficient to solve?

(I would have asked myself but I'm in a library :sweat_smile: )

[David Thrane Christiansen]

I'll ask it for you in the question session

[Max Nowak 🐉]

Thanks :+1:

[Marcus Rossel]

@Josh Clune If duper (practically) relies on receiving only few relevant lemmas, do you expect premise selection to work well with duper?

[Max Nowak 🐉]

Thanks for the answer :)

[Josh Clune]

Marcus Rossel said:

Josh Clune If duper (practically) relies on receiving only few relevant lemmas, do you expect premise selection to work well with duper?

It's hard to know whether something will be "efficient enough" in practice to be useful before actually doing it, but I'm optimistic that Duper will fit in well with a full sledgehammer pipeline. In a sledgehammer pipeline, the first form of premise selection you have is a relevance filter (sometimes a machine learning thing, sometimes a heuristic thing, sometimes a combination) that generates a ton of related lemmas from the library (think hundreds). Hooking Duper up to that directly wouldn't work well. However, in a sledgehammer pipeline, the second thing you do is send the problem (with all the lemmas from the relevance filter) off to an external prover which doesn't need to worry about proof production, and can therefore operate much more efficiently. Then, if the external prover succeeds, it can send back just the lemmas it actually used to obtain a proof. I'm optimistic that Duper will be able to perform reasonably well given just the lemmas that an external prover like Zipperposition needed to solve the problem.

[Ricardo Correia]

Josh Clune said:

I'm optimistic that Duper will be able to perform reasonably well given just the lemmas that an external prover like Zipperposition needed to solve the problem.

These external provers (including Zipperposition) don't just reason on provided lemmas, they also have theory-specific reasoning (hence the T in SMT). Is Duper also going to do that?
Thanks for the great talk btw!

[Marcus Rossel]

Josh Clune said:

if the external prover succeeds, it can send back just the lemmas it actually used to obtain a proof. I'm optimistic that Duper will be able to perform reasonably well given just the lemmas that an external prover like Zipperposition needed to solve the problem.

So in such a pipeline the theorem would basically be proven twice?

[Max Nowak 🐉]

Isabelle's sledgehammer invokes SMT solvers and uses them as a glorified relevance filter. Those lemmas are then passed into its own superposition prover metis for "proof reconstruction". So it's not that unusual. It works surprisingly well for Isabelle, I imagine it'll be fine for Lean. (I don't know any details though, just speaking from my own relatively limited experience).

[Josh Clune]

Ricardo Correia said:

These external provers (including Zipperposition) don't just reason on provided lemmas, they also have theory-specific reasoning (hence the T in SMT). Is Duper also going to do that?
Thanks for the great talk btw!

I'm not sure that Zipperposition has domain-specific reasoning like SMT solvers do. I'd have to double check that. But in either case, there aren't any current plans for Duper to support domain-specific reasoning (besides what it can figure out if you just give it a bunch of domain-specific lemmas). The first target is to get a full sledgehammer pipeline for problems that are essentially first-order or higher-order. Once we're past that target, it might be interesting to explore integrating more domain-specific things into Duper, but that's much farther away.

[Josh Clune]

Marcus Rossel said:

So in such a pipeline the theorem would basically be proven twice?

Yes, but the theorem would only need to be proven twice the first time it's proven. After the external prover finds the lemmas Duper needs to prove the problem, the sledgehammer call could be converted to a Duper call (with the appropriate lemmas supplied) so that future compilations of the file only need to use Duper, and don't even need call the external prover.

[Notification Bot]

Zory Zhang has marked this topic as resolved.

[Notification Bot]

Zory Zhang has marked this topic as unresolved.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Hey @Josh Clune , that was a really great talk! In your high-level description, you said that the superposition loop uses a passive set (initially all facts) and an active set (initially empty), and tries to derive a contradiction. The passive set is initially populated by $H ∪ {¬φ}$ where $H$ are the hypotheses and $φ$ the goal. At one point the ATP community discovered that simply reasoning forwards from $H$ can be quite unproductive as the set is usually consistent (e.g. the group axioms or whatever), and one needs to use $¬φ$ or facts derived from it in some crucial way. This is called the set of support strategy, described e.g. here. I am wondering: do you anything goal-oriented like this, and if not, could you?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Max Nowak 🐉 said:

Isabelle's sledgehammer invokes SMT solvers and uses them as a glorified relevance filter. Those lemmas are then passed into its own superposition prover metis for "proof reconstruction". So it's not that unusual. It works surprisingly well for Isabelle, I imagine it'll be fine for Lean. (I don't know any details though, just speaking from my own relatively limited experience).

Afaik from chatting to people involved in this effort, the 'glorified relevance filter' used to be true of a very early version of the Isabelle sledgehammer but is no longer true. That is, the early version did only transmit the used lemmas and not much more from the external solver to metis, but nowadays when calling e.g. Z3, Z3 will absolutely export the proof steps it applied, and the sledgehammer uses that information. The information is still not a full proof, but it's more than just a list of lemmas.

[Josh Clune]

Wojciech Nawrocki said:

Hey Josh Clune , that was a really great talk! In your high-level description, you said that the superposition loop uses a passive set (initially all facts) and an active set (initially empty), and tries to derive a contradiction. The passive set is initially populated by $H ∪ {¬φ}$ where $H$ are the hypotheses and $φ$ the goal. At one point the ATP community discovered that simply reasoning forwards from $H$ can be quite unproductive as the set is usually consistent (e.g. the group axioms or whatever), and one needs to use $¬φ$ or facts derived from it in some crucial way. This is called the set of support strategy, described e.g. here. I am wondering: do you anything goal-oriented like this, and if not, could you?

Duper doesn't currently implement the full set of support strategy that you linked to. However, when preprocessing is disabled, Duper does have some heuristics in place to prefer reasoning about clauses that are closely derived from the goal. Currently, there are some technical issues that prevent us from using those same heuristics when preprocessing is enabled (it's nontrivial to determine which of the facts output by Auto's preprocessing and monomorphization procedures were derived from the goal), but that is a problem that we are actively working on, and our intent is to at least reach a state where those same heuristics can be used regardless of whether Duper is using Auto's preprocessing and monomorphization procedures.

[Josh Clune]

Wojciech Nawrocki said:

Afaik from chatting to people involved in this effort, the 'glorified relevance filter' used to be true of a very early version of the Isabelle sledgehammer but is no longer true. That is, the early version did only transmit the used lemmas and not much more from the external solver to metis, but nowadays when calling e.g. Z3, Z3 will absolutely export the proof steps it applied, and the sledgehammer uses that information. The information is still not a full proof, but it's more than just a list of lemmas.

I think the situation is a bit more complicated than that. There are some SMT solvers whose proofs Isabelle can use for more direct proof reconstruction (Z3 and veriT). However, the set of external provers that the sledgehammer will call is larger than the set of provers for which this direct proof reconstruction is possible. So there are some instances in which Isabelle will achieve proof reconstruction by actually following the proof output by an external solver, but there are other instances where this approach isn't feasible and so the lemma-based proof reconstruction approach (i.e. just using the external solver to figure out which lemmas you need) is still used.