[Matryoshka-devel] Evil axioms

Cezary Kaliszyk cezarykaliszyk at gmail.com
Thu Apr 20 05:08:00 CEST 2017


One more related thing is automatically figuring out the basic logical
facts and removing them (from the training data). They can be derived
by the ATP automatically, and they do slow down the proof (evilness).
We do this in HH and I think there was once a similar thing in SH?

C.


On Wed, Apr 19, 2017 at 8:49 PM, Giles Reger
<giles.reger at manchester.ac.uk> wrote:
> Hi Jasmin,
>
> Q1 seems to be ‘folklore’ in the superposition world and I’m not aware of
> any explicit paper on the subject but the idea of avoiding evilness
> motivates a lot of things i.e. ordering restrictions, set of support. Our
> paper “Selecting the Selection” at last year’s IJCAR motivates a set of
> literal selection functions in terms of not selecting ‘evil’ literals,
> although we do not use this lovely term. We have some unpublished and
> immature work on promoting ‘nice’ subclauses in the AVATAR framework which
> follows a similar motivation.
>
> We (Martin and I) are actually looking at Q2 at the moment. We have a paper
> at IWIL within the context of theory axioms (attached) and are beginning to
> extend this to axioms in general. The idea is not ground breaking: the
> general approach is to separate ‘good’ and ‘bad’ axioms and then restrict
> inferences between ‘bad’ axioms. Within (arithmetic) theory reasoning the
> bad axioms are axioms of the theory. Once we have such a framework we can
> attempt to automatically detect ‘bad’ axioms etc, but we haven’t gone down
> this road yet (ongoing research). Notice that most of what superposition
> theorem provers do is about avoiding evilness.
>
> With respect to Q3. I think it is interesting. We already have strong
> guesses about what the patterns would look like for superposition solvers,
> and I guess SMT people have their intuitions, and I also guess that evilness
> will mean different things for the two approaches. However, a study like
> this could surprise us, which would be fun. We conducted a different study
> recently to test some folklore about fast-growing search spaces and the
> results were not as clear-cut as I expected (unless I forget).
>
> Of course, your point that sometimes we need these evil things is an
> important one. The hypothesis is that most reasoning doesn’t need evil
> things but then when we need the evil things we have to pay for them and
> whilst we attempt to mitigate their evilness a bit, we still have to pay
> quite heavily.
>
> On this point
>
> The thing we haven't tried yet, but should, is to transform the
> statistically learned guidance into some rule-based heuristics that are
> explainable and understandable by humans.
>
>
> It sounds like a great challenge, but I think sometimes it is just magic and
> effort can be wasted working out where the rabbit came from. Occasionally
> (once or twice) we have added an option based on a strong intuition, and
> then decided to add another option that does the opposite thing to confirm
> our intuition, and then find that the opposite thing does better in many
> cases. And we can apply some post-hoc justification, but this doesn’t
> necessarily help us make the right choice next time ;)
>
> Cheers, Giles
>
>
> On 19 Apr 2017, at 19:22, Josef Urban <josef.urban at gmail.com> wrote:
>
> Hi Jasmin,
>
> Larry had some manual blacklisting in SH long ago.
>
> I have always believed that such things are very context/strategy dependent
> and should be learned depending on such context. Both for premise selection
> and for internal guidance. The data are out there.
>
> The thing we haven't tried yet, but should, is to transform the
> statistically learned guidance into some rule-based heuristics that are
> explainable and understandable by humans.
>
> Josef
>
> On Apr 19, 2017 19:29, "Blanchette, J.C." <j.c.blanchette at vu.nl> wrote:
>
> Hi all,
>
> I was about to write an email with five recipients but then it occurred to
> me that we have this mailing list, which can be used for general discussions
> as well as for announcements. I hope this is not too much of a problem to
> whomever I promised the list would be low traffic.
>
> The typical "hammer" use case of automatic provers includes hundreds of
> heuristically selected lemmas as axioms in the generated problems. However,
> I've often observed that some axioms can be "evil", meaning that a single
> axiom can be enough to go from "provable within 1 s" to "the prover spins
> seemingly forever". This is not so surprising in itself (both superposition
> and SMT are unstable in many ways), but I suspect that this evilness might
> not always be the result of randomness. Maybe some axioms are just generally
> evil, and the provers are not always robust enough.
>
> For example, it is well known that for superposition provers, axioms with
> unit equalities between two variables, such as extensionality
>
>         (forall x. F x = G x) => F = G
>
> are known as being evil, because they can a priori be applied anywhere to
> rewrite any term into any term; they're extremely "prolific", yielding lots
> of new clauses. Superposition provers neutralize this by down-prioritizing
> such inferences, so that such evil axioms are not actually evil in the end.
> (The price you pay is that when you really need them, they don't kick in;
> but see also the work by the Vampire guys on extensionality in
> superposition.)
>
> Extensionality is not evil thanks to the down-prioritization (or Vampire's
> extensionality extension), but there might be other patterns that are evil
> for prover X or calculus Y. I have some concrete questions below, but I'd be
> curious about your thoughts or further questions.
>
> Q1. Is this concept of "evilness" discussed anywhere in the literature?
>
> Q2. Do provers have some general robustness mechanisms to deal with evil
> axioms? Should this be investigated?
>
> Q3. Would it make sense to empirically evaluate the evilness of thousands of
> axioms and to try to identify some patterns? Has anybody ever done anything
> like that?
>
> For the record, axiom a28 in the attached SMT-LIB problem ruins everything
> on that problem for the repository version of veriT. I don't know if it's
> really evil, though, without trying to add it to other easily solvable
> problems.
>
> Cheers,
>
> Jasmin
>
>
> _______________________________________________
> matryoshka-devel mailing list
> matryoshka-devel at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/matryoshka-devel
>
> _______________________________________________
> matryoshka-devel mailing list
> matryoshka-devel at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/matryoshka-devel
>
>
>
> _______________________________________________
> matryoshka-devel mailing list
> matryoshka-devel at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/matryoshka-devel
>



-- 
Cezary Kaliszyk, University of Innsbruck,
http://cl-informatik.uibk.ac.at/cek/


More information about the matryoshka-devel mailing list