[SMT-COMP] Fwd: Re: [smt-lib] Fwd: Proof Validation Track for SMT-COMP

[Haniel Barbosa]

Fowarding my reply to the SMT-COMP list as well, in case anybody is in
the diff.

Haniel Barbosa writes:

> Hello,
>
> So I see that we have many competing views, what a surprise. :)
>
> I agree with the general feeling that a proof track in SMT-COMP, in
> the interest of adoption, should not put a heavy (virtually
> insurmountable?) burden on the developers. I believe that forcing the
> solvers to implement their own elaborators increases this burden
> prohibitively. Therefore my view is:
>
> - one format is used for the proof track. Every entrant must print
>   proofs in that format. This format contains coarse-grained (hard to
>   check) and fine-grained (easy to check) rules.
>
> - a tool, the validator, is used by the competition that can check
>   fine-grained steps, maybe can elaborate coarse-grained steps into
>   fine-grained ones to be checked.
>
> There is a lot of unknowns for the above. For things the validator
> can't elaborate (preprocessing passes may be a common instance for
> this) one could, as Jochen suggested, generate SMT problems and throw
> SMT solvers at them, like we do in the unsat-core track.
>
> Defining ways to score solvers with the above unknowns would be hard
> as well. Probably there could be different tracks, for "valid proofs"
> vs "good proofs". 
>
> What is the format? What is the validator? I think it's not reasonable
> to expect a lot of work on this solely for the purpose of running an
> SMT-COMP track. Therefore I believe it makes sense to piggyback on
> projects with a wider scope. The Alethe format (bias alert: I'm
> involved with it) is supported by multiple SMT solvers (veriT and
> cvc5), uses SMT-LIB as term language, has coarse- and fine-grained
> steps, and is integrated into into Coq [1] and Isabelle/HOL [2]. The
> project is actively developed and multiple ways of extending it are
> being considered. An independent checker, in Rust, is under
> development and is also indented to elaborate proofs into Alethe's
> own fine-grained steps but also to other backends, like LFSC, Lean or
> other low-level proof checkers people may have and want to contribute
> to. It's not a closed project.
>
> So it might be interest to consider it instead of new formats. Or
> translations into it from your format of choice.
>
> A note on François' two cents: I agree that one can handle
> coarse-grained steps in a trusted way with certified complex checkers,
> but given the sheer scope of SMT-LIB theories and all the moving parts
> that go into them I believe a more flexible approach of pushing this
> complexity into elaborators that do not need to be correct by
> construction is more suitable.
>
> Best,
>
> [1] SMTCoq: A Plug-In for Integrating SMT Solvers into Coq
> [2] Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant
>
>
> Jochen Hoenicke writes:
>
>> On Wed, 21 Jul 2021 at 00:25, Simon Cruanes <simon.cruanes.2007 at m4x.org> wrote:
>>>
>>> A small example (eq_diamond2 in QF_UF):
>>> https://c-cube.github.io/quip-book/reference/example.html
>>
>> Thanks for the input. Your proof format is on the same level as the
>> format I have in mind.  Converting between the formats should be
>> straight-forward (at least for the proof on this page).  Your bool-c
>> rule corresponds to my Tseitin-axioms, the ccl rule in that example is
>> my transitivity axiom and would be written (transitivity x0 y0 x1). My
>> planned syntax is a bit less verbose, omitting the proved clause from
>> the stepc (in my syntax deft and stepc are just let).   I'm not sure
>> if including the clause is helpful for debugging.  I think if the
>> resolution rule takes the pivot literal and checks for the presence of
>> the pivot literal in the antecedents that already helps enough. The
>> proof checker could also dump the clauses for debugging purposes.
>>
>>> Roughly I'd say it's close to Alethe but with coarser grained
>>> inferences, explicit polarities in clauses, and a lot of vaporware when
>>> it comes to instantiations since I don't have any actual quantified
>>> proofs in it yet.
>>
>> I guess your ccl rule allows more than just transitivity.  We have a
>> similarly complicated cc-lemma in our prover.  It produces the same
>> clause as your ccl rule and annotates it with all the paths used in
>> the CC-graph (for fast proof checking; we have to traverse the paths
>> anyway to collect the equalities).  When combining this with Array
>> theory (which is integrated into CC theory), the complexity became too
>> much to handle, especially for our interpolator. We found that
>> post-processing the cc-lemma to use only transitivity, congruence and
>> hyper-resolution is not so difficult and made interpolation of CC
>> lemmas and proof-checking almost trivial.  The post-processor just
>> builds a transitivity axiom for each path, a congruence axiom for each
>> equality on a path that is not already in the clause, orders these
>> axioms by dependency, and then combines the axioms with a single
>> hyper-resolution rule.
>>
>>> On Tue, 20 Jul 2021, Jochen Hoenicke wrote:
>>> > I'm still not sure whether one should also distinguish between negated
>>> > literals and "not"-terms.  It would create even more overhead and
>>> > would require Tseitin axioms for not.  It could be avoided by
>>> > automatically converting every term starting with not to a literal
>>> > without not, handling  any number of nested not.  Only, it's a little
>>> > against my philosophy of keeping it really strict :)
>>>
>>> Agreed that it's useful to have first-class clauses. For the polarities,
>>> I currently have them; a clause looks like this:
>>> `(cl (+ a) (+ b) (- (or a b)))`. However I've found the need for a rule
>>> named "nn" (negation normalization) which turns `(cl (- (not a)) …)`
>>> into `(cl (+ a) …)`, and it's a bit ugly and unclear when the solver
>>> needs to produce it.
>>
>> The Tseitin-clauses for not are just "+(not a), +a" and "-(not a),-a",
>> and resolving with one of them is your nn step.
>>
>> If "not" itself is used to represent negated literal in clauses, you get a
>> problem with double negation.  Resolving "C \/ (not (not a))" with
>> "(not a) \/ a" on the pivot "(not a)" does not only look strange, but you
>> are resolving with a tautological clause containing a literal with both
>> polarities.  To avoid this in this setting, a double-negation must be
>> removed automatically and silently.
>>
>> I have a preliminary write-up of my axioms and overall format, but I
>> wanted to clean it up and incorporate the feedback I got so far.  I
>> also haven't started with the proof checker yet.  Although it wouldn't
>> differ so much from the proof-checker we have in our solver if you
>> would strip all the high-level proof rules from it.
>>
>> Regards,
>>   Jochen


-- 
Haniel Barbosa
https://homepages.dcc.ufmg.br/~hbarbosa/