reproducible SAT/SMT reasoning

Stream: lean4

[Adrien Champion]

A while ago, during a monthly dev update (which I miss dearly), I asked whether Lean 4 plans to integrate SMT reasoning to solve "easy" goals automatically like Sledgehammer / SMTCoq do, and how.

[Adrien Champion]

IIRC, Leo answered that doing so raises reproducibility problems, i.e. you would need a notion of heartbeat at solver-level that is consistent across platforms, machines... Otherwise, you easily end up with builds that fail ("timeout") in some environment/machines and succeed in others.

[Adrien Champion]

At this point, I'm pretty sure Leo mentioned something that could solve this problem. I think the name of that solution was something like "SAT minus minus" ("SAT--"?), but it was not written down so I might have heard wrong (or just remember wrong).

[Adrien Champion]

I searched for that name, or for SAT/SMT-related techniques with a reproducible notion of heartbeat, but could not find anything that seemed related to what Leo was saying.

[Adrien Champion]

Does anyone remember or know about this? Did I hallucinate the whole conversation?!

[Max Nowak 🐉]

I think SMT solvers are mostly useful to run once, find a proof, which is then either enshrined in a sequence of tactics instead, or in a call to a resolution/superposition prover (such as Isabelle's metis or Lean's duper). SMT calls are rather slow, so it would be a bad idea to have calls to an smt tactic in mathlib. There are (at least?) two projects for currently building a Lean4 hammer.

I'm not sure what you or Leo meant with heartbeat :(.

[Adrien Champion]

My understanding is that a heartbeat metric is a deterministic, reproducible measure of a tool/algorithm progress. It's better in terms of reproducibility than timeouts which depend on pretty much the whole hardware/software environment

[Adrien Champion]

But I'm starting to think this was a fever dream, especially since what you said makes a lot of sense. lean-smt it is then :grinning:

[Adrien Champion]

I'm pretty sure this conversation happened during the first dev update meeting, for which I cannot find a video, so...

[Adrien Champion]

@Max Nowak 🐺 what's the other "Lean 4 hammer" project, besides lean-smt?

[Reid Barton]

I would guess that the discussion was about invoking an external solver, which may run for a long time or forever, so there is no deterministic way to stop the solver if it runs for "too long", unless it is somehow integrated with Lean's heartbeats system.

[Adrien Champion]

I'm starting to think that, if this conversation actually happened, there was probably a misunderstanding between my question and his answer (most likely on my end)

[Jannis Limperg]

I thought this SMT-- idea was to have a very slimmed-down SMT solver actually implemented in Lean, working with Lean data structures. Like the ematch functionality in Lean 3. Then one would need a deterministic timeout mechanism as discussed here. But maybe we should ask the people involved. :innocent:

[Adrien Champion]

Ah! Maybe it was not a fever dream afterall

[Adrien Champion]

@Jannis Limperg Is "SMT--" a known, published thing, or is it just a (temporary) name for a potential implementation? A quick search for it returned nothing

[Jannis Limperg]

It's an idea of Leo's which has not been seriously worked on since the Lean 3 days afaik.

[Adrien Champion]

I see, thank you very much for the clarification :smiley_cat:

[Max Nowak 🐉]

There are timeout options for SMT solvers, I don't see the problem?

[Max Nowak 🐉]

Adrien Champion said:

Max Nowak 🐺 what's the other "Lean 4 hammer" project, besides lean-smt?

I've been slowly working on my own hammer (translation only, no proof reconstruction yet) targeting higher order smt solvers, as a student project. I didn't know lean-smt existed before I started :sweat_smile:. We'll see how it goes, maybe I can contribute to the lean-smt project.

[Adrien Champion]

Max Nowak 🐺 said:

There are timeout options for SMT solvers, I don't see the problem?

Reproducibility

[Adrien Champion]

A timeout does not mean anything for the program, it's just an order to stop that triggers whenever. Even on the same machine and environment, two runs with the same timeout will not stop at the same exact "place in the unfolding of the algorithm", meaning in general you can get "an answer" or "timeout" pretty much randomly with the same program, same input, same timeout.
Never mind on different machines with different everything

[Max Nowak 🐉]

Ahhhh now I finally understand the problem. IMO the solution is to only use hammers akin to library_search: Once.

[Adrien Champion]

Right, but as @Jannis Limperg clarified it seems that "SMT--" was referring to a dialed back SMT solver implemented directly in Lean to do some reasoning on lean objects. I'm not sure the goal of SMT-- is to realize a sledgehammer-like feature, but I'm in way over my head so I think we will have to wait for someone (probably Leo) to clarify further

[Adrien Champion]

I mean, maybe SMT-- is not even related to proof search (though that'd be surprising), maybe it's (also) for unification / type class resolution / ... (just freestyling at this point)

[Jason Rute]

It is not an SAT solver, but you might be interested in MagnusHammer. #Machine Learning for Theorem Proving > New paper: Magnushammer. It is currently for Isabelle and would require external neural network tools, but on the other hand it seems to do a lot that Sledgehammer can do and more, and I personally think it is a simpler concept.

[Jason Rute]

Although, I guess MagnusHammer still needs general purpose reasoning tactics, like Isabelle’s MESON tactic, to reconstruct the proof so I guess this gets back to the question of putting some sort of powerful reasoning tactics directly into Lean.

[Jason Rute]

(Reading this topic again, I missed the point. Ignore me.)

[Adrien Champion]

Jason Rute said:

(Reading this topic again, I missed the point. Ignore me.)

I'm still grateful for what you said and the link you provided :heart:

[James Gallicchio]

Marijn Heule is also working on some new proof formats for SMT that will hopefully make reproducibility & verification easier. But there are many other hurdles to overcome with SMT integration in Lean :)

[Max Nowak 🐉]

James Gallicchio said:

Marijn Heule is also working on some new proof formats for SMT that will hopefully make reproducibility & verification easier. But there are many other hurdles to overcome with SMT integration in Lean :)

Can you elaborate on that new format? I'm curious!

[James Gallicchio]

I don't really know what direction he's thinking about. I think it's something along the lines of Joseph Reeve's proof skeletons work as well as prior work on LRAT/DRAT formats for SAT

[Reid Barton]

But it's really for SMT solvers and not just SAT solvers right?