[Matryoshka-devel] Evil axioms

Giles Reger giles.reger at manchester.ac.uk
Wed Apr 19 20:49:52 CEST 2017


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<mailto: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<mailto: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<mailto: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<mailto:matryoshka-devel at lists.gforge.inria.fr>
https://lists.gforge.inria.fr/mailman/listinfo/matryoshka-devel

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/matryoshka-devel/attachments/20170419/e57d5b35/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: sosTheoryReasoning.pdf
Type: application/pdf
Size: 316492 bytes
Desc: sosTheoryReasoning.pdf
URL: <http://lists.gforge.inria.fr/pipermail/matryoshka-devel/attachments/20170419/e57d5b35/attachment-0001.pdf>


More information about the matryoshka-devel mailing list