Remarks on Classes of Random Bounties

by Brown, Saturday, October 03, 2020, 11:48 (428 days ago)
edited by Brown, Saturday, October 03, 2020, 11:53

One of my concerns about the random bounty propositions is that they often seem too easy. (I'll say more about each category below.) Each time an easy one is generated, it creates bad incentives for stakers. Specifically a staker might refuse to publish any commitments other than their own to try to ensure their document with the proof is published first. As long as easy ones are rare, this probably isn't a big issue, but I don't think they're so rare at the moment.

I think the AIM problems are the best, in terms of being unlikely to be easy. I was worried about these since in August it was reported to me that CVC4-SAT18 could find countermodels to many of them, indicating they have small finite counterexamples. This was surprising to me since I know the smallest possible counterexamples would have a domain of size 5. Looking closer it turned out there's a bug in the FOF printout of the problem. It's leaving out the definitions of "a" and "K" in the FOF specification, making the conjectures always very easy to make false.

I spent some time testing all possible finite loops of size 5 and 6 and none of them are actual counterexamples to any of the AIM reward bounty propositions so far. I also tried 8 loops of size 7 and these also didn't give counterexamples. I'm reasonably convinced that when there are countermodels, they will be difficult for model finders to generate. The fact that The AIM Conjecture is still open is a strong indication that cases where the conjecture is provable will also be difficult.

So, one possibility for a hard fork would be to just make the AIM1 and AIM2 classes the only kind of (new) reward bounty propositions. They're relatively easy to explain to newcomers and will provide a simple way for people from outside the theorem proving community to understand the conjectures. All of them ask the same kind of question: is there a finite set with a binary operation satisfying some equations and falsifying one of two very specific equations?

It's also easier to make the case that the AIM1 and AIM2 conjectures are "meaningful" since they relate to an open problem in mathematics.

Here's my summary about the other classes:

Random HF : These are easy too often, if someone just ignores most of the irrelevant parts of the proposition. For example, it's often easy enough to prove one by using an instantiation like "constant False" or "constant True" for one quantifier and not caring about the instantiations of other quantifiers.

QBF : Experiments with some QBF solvers a few months ago suggested to me that with current technology and a 10 minute time out, about 40% of the random QBF problems can be solved. It's still "difficult" (practically, not in principle) to obtain a Proofgold proof term for the problem, but I doubt that's a serious problem. As soon as someone overcomes it, far too many of the QBF problems are too easy.

Set Constraints : I don't have a strong opinion here, but it seems likely many could be solved using the SETVAR techniques of Bledsoe and Feng (adapted for higher-order theorem proving by me, see my CADE 2002 paper).

Higher-Order Unification: While this is undecidable, Huet's preunification (and various extensions over the decades) would likely make many of these relatively easy.

Untyped Combinator Unification: Again, this is an undecidable problem class, but Vampire was able to quickly say many of the corresponding first-order problems were countersatisfiable (14 out of 19). This is surprisingly high and makes me wonder if there is a bug in either the problem generation or the fof representation of the problem.

Abstract HF Problems: CVC4-SAT and Vampire togethere were able to say 4 out of 61 of these were countersatisfiable within a minute. That's not too bad, but I've also found at least one example from this class that was very easy -- where the conjecture follows by instantiating one quantifier of an axiom. I suspect that if people focused on solving these problems, too high a percentage would turn out to be easy.

Diophantine: Again, while this is a class of undecidable problems, it's not clear how difficult the randomly generated conjectures are in practice. So far no prover has proven or disproven any of the ones from this class, but it's easy to imagine someone familiar with integer programming would know some tricks to make many of the problems easy to solve.