Can Deep Learning be applied to Automated Deduction?

Deep learning is just a deeply layered neural network, and by deep they mean more than one internal layer. It has recently gained much attention because of its successes with images and go and speech and all sorts of things plain old NNs weren't doing so well at.

But what about automated deduction? That's not rhetorical, this is entirely speculative and answer free. I am wondering if DL (or any ML technique) could be thrown at AD (or ATP (automated theorem Proving) whatever you'd like to call it).

First the optimism: wow wouldn't that be cool, a method that would prove really hard mathematical theorems (the ATP community has to work hard and do a lot by hand to do things like flyspeck) or even . But desiring the outcome doesn't say anything about the implementation.

Next the pessimism. By analogy, images and speech/text are iffy optimization problems. Lots of perturbations get you the same thing. But logic (and similar combinatorial problems) are all or nothing. It is either true/proven or false/wrong. how could an approximation optimization method translate to logical combinatorial problems? Where do you get the scads of supervised instances required by DL? Millions of tagged images from MNIST but from TPTP literally only thousands.

So, I don't know. But just because I don't know how to do it doesn't mean it can't be done.

A small nitpick about a small p-value problem trope

Lately the p-value has been getting a lot of press, almost entirely bad (tip of the iceberg). Whatever it is and means has been up for discussion as it hasn't had since NPHT was created (the Bayesians have been fighting against it, or rather fighting for alternatives, since the 60's).

Hidden in the middle of this storm, or a small tornado on the side, is the issue of data fishing or p-hacking. Since only a p-value of less than .05 is considered 'statistically significant, only such values are considered publishable leading to the problems of: selective publishing (ignoring significant non-results), and p-hacking (if one p-value isn't good enough, change you hypothesis and testing little by little until you get a p-value below the threshold). The problematic trope is stated in roughly the following manner:

At p-level threshold set at 5% (or .05 or 1/20), all you need is 20 studied hypotheses to get one hypothesis that is significant by chance.

It's so obvious!  With 1/20th probability, you need 20 tries to guarantee a hit! The intention is that you shouldn't make many hypothesis tests at a time, otherwise you'll get some false hypothesis stated as true.

But you may notice with that wording that it is a classic gambler's misinterpretation, 'the run has to end!'. Each hypothesis test is independent, and so the probability of the next test will not change if all the previous tests are all hits or all not or whatever.

Whatever you think of p-values, and whatever you think they mean, they are probabilities. Probabilities of what is complicated and nuanced and misleadingly stated and problematic and the firm basis for statistical inference for the past hundred years. But still, they are probabilities of something and a strict threshold of 5% of accepting a hypothesis over rej... forget that verbiage. it's a 1/20 probability event.


So now we're in the realm of basic probability (and its own difficulties) but they should be shared by Bayesians, Frequentists, Kolmogorov..ans, Keynesians (he had his own!). So any hypothesis has a probability of .05 of being positive, a hit. What's the probability of a hit in 1 trial? 5%. What's the probability of a hit (at least one hit) in 2 trials? 3? n trials? Those are harder but only a tiny bit, basic probability/combinatorics. What's the probability of at least one hit? One minus the probability of no hits at all. What's the probability of no hits in n trials? (probability of no hit in one trial)^n. They are independent events so you multiply. Final answer:


\[
P({\rm hit\ in\ n\ trials}) = 1-P({\rm no\ hit})^n = 1- 0.95^n
\]

Well, not final exactly, it's just a formula. We don't yet have a good picture of what it means in realation to our intuition about 'it'll take 20 to make sure we have a hit'.

So then a picture:



It starts at 0, rises in exponential decay asymptotically to 1, but is a little slower than you'd expect for an exponential because the base is so close to 1.


The usual way to present such probabilities is, like the birthday paradox, to say how many trials it takes to get %50 chance. Multiplying .95 a few times we see that it takes 14 trials for there to be more than 50/50 chance that at least one item is a hit. To get to 95% chance, it takes 59 trials. There's no guarantee that there'll be a hit, just the probability gets smaller and smaller.


I make this point to... well, to pick a nit. You do more experiments, the more likely there will be one that is 'statistically significant' totally by chance. Intuition and logic lead to that immediately. But the logic is never done and one step of it doesn't lead to correct two steps. I do realize it is a bit of a mouthful and difficult to digest to say 'after 14 trials there will be a fifty-fifty for a false positive'? 50/50? It's not obvious how that relates to 5%, but the erroneous 20*.05 = 100% does obviously relate.


In the end, to say '5% means 20 experiments', which seems so directly and intuitively obvious, is wrong. In the right direction, but wrong.

A serious proposal about Daylight Saving Time

People everywhere hate the spring change in clocks for Daylight Saving Time.

First, it's annoyingly tiring having to get up one hour earlier. And feeling like you can stay up a whole hour later. And this leading to wanting to stay in bed that much longer even more. Annoying.

Second, the average effect of this annoyance on the population. This leads to, statistically, 'studies have been done', of reduced physical performance leading to accidents (lower light levels from sun than in the previous week), and an increase in heart attacks and strokes (not exactly excuses to lie in bed a bit longer).

DST changes things twice a year. In a preindustrial society, without fast travel and communication, time zones are not useful. DST is useful for... for what I'm not sure. More daylight in the evening? That's not for work, that's for ... I don't know, kids to stay outside and play longer?

But if that is desired, but also we'd like the feature of no changing of wakeup time, I have a radical new idea, which though it sounds strange, is not entirely a crackpot idea. My proposal:

Have clock time pegged to sunrise.

And call that time 6am. No matter where you are on Earth.

First there is the practical consideration, then there is the implementation. Practically, it fulfills the feature of never changing. You always get to wakeup at the same time. Nowadays we all choose to go to bed pretty much irrelevant to sunset anyways. And the farmers don't have their delivery schedules screwed up when the milking cows don't care about these crazy human practices.

Implementation may be the most difficult, and here is where some of the subtleties come out. However, this is the 21st century. The point is that sunrise is equivalent to longitude, and this is determinable now by any variety of methods but also by pure calculation (whose coefficients were determined by those methods or in the end skywatching).

We all have at our disposal computation devices that are minute in bulk (phones, watches, RFID chips) with GPS positioning (via satellites), that can determine longitude within a few meters (2?). So sunrise will be a few seconds off from someone 10 miles west (15 degrees = 1 hour sunrise difference, 1 degree ~= 60 miles ... 10 miles ~= 24 seconds). This continuous difference sounds like it is insurmountable... except by computation, which is currently trivially executable. You're having a phone meeting with someone at 9:30am, you're in downtown Chicago and they're in Kansas City, MO (~415 miles west). That's around 7 degrees or 28 minutes. If the appointment is at 9:30AM Chicago Loop time, in Kansas City it is ~9AM. The appointment making software would calculate the time for the recipient based on their address. For coordination there can still be a UTC which is the time at one particular longitude.

There are some very minor difficulties that are barely in the realm of practical considerations. Depending on your latitude, noon (or six hours after sunrise) may not correspond to the highest point of the sun in the sky, but that's the case now anyway (just not as much). Also for higher latitudes, sunset will change drastically in the spring in fall (sunset coming later one day to the next by up to 10 minutes, making the feel of the evening change within the week.

There's cultural precedence for this. Many ancient calendars count the change of day (but not when to rise or go to bed) to sunset, so why not sunrise. Our mental perception of the 'next day starting', despite the European style (derived from Roman) changeover at the sun point opposite to sun's zenith (yes, I'm avoiding 'midday' and 'noon' for the moment),  is truly when we wake up around dawn or more naturally at dawn.

So that's it. Free idea. Go forth and implement. Just give me credit. If there are problems, I'd like to blame the future implementation.

Of course, this doesn't fix the problems of Jews and Muslims north of the Arctic Circle with practices on cooking or fasting concerning sundown.

Review: Ready Player One

"Ready Player One" by Ernest Cline, is a sci-fi novel about a kid, living in an impoverished near future, escapes like most of the population into a super-powered virtual world invented by a Steve Jobs style nerd. The plot of the novel is following this kid trying to find an 'easter egg' planted by this eccentric inventor bajillionaire, all by playing different video games or by using pop cultural references from nerd culture () most of these from the 70's and 80's (the dawn of blockbuster movies, and PCs and video games (arcade games, PC games, and pre-Mario Bros game controllers).

I don't know. The nerd-pop-cultural references were all there. Star Wars, Star Trek, Blade Runner, Monty Python, War Games. Joust, Defender, Dig Dug, D&D, all well referenced, lines of dialog. All well suited to my personal memory of teen years. Lots of excitement and virtual explosions and real explosions and plot twists and I'm sure hidden easter eggs in the novel itself.

But I'm an old dude. I don't see how kids these days (2011) would appreciate the references.

The tone is very much 'young adult novel'. It should be advertised as such, because it's not Philip K Dick if you're expecting that. The concerns are all of a cliché 18 year old (does that girl like me? I will obviously win this game having played it literally hundreds of times or literally never! I hate my welfare aunt who I live with since my parents died.)

The writing is like Asimov. I don't mean that as a compliment. Despite its obvious attempts at being modern and PC, they all come across as clunky white-male-teenager-privileged like a nice mormon dad coming to terms with a child caught drinking coffee. The main character's best friend on-line, a dude like himself but cooler, turns out in real life to, wait for it, it's shocking, are you sure you won't be shocked, a shy black overweight lesbian. Oh and the girl I like in the virtual world whose avatar is totally hot, in real life, she's also hot except she has a port wine stain on her face. The horror. The shame. The forced lesson of understanding of others without being other.

And the plot should be considered simply a string of the most unmotivated deus ex machina's and Mary Sue. And this is two levels deep, both in the engineered MMORG world and in the simulated games within that world. Oh did I mention this one hidden rule that you get 40 lives if you die the right may in this video game? Convenient that the best friend of the inventor comes to help out the gang at the last minute. Oh no, the opponents destroyed absolutely everything (virtual) with a  pixel bomb (sorry, that's not in the book but it's the shortest way to give the same idea), but the one tiny thing needed to complete this one magic task left happens to have survived? I'll win a bajillion dollars, I think I'll share it with my friends even though I won the game at the end, I'm a great guy!

The book is a lot of fun (moreso if you recognize the references). But it's mostly processed sugar and wish-fulfillment. Should be a fun movie, which should be able to avoid most of these clunkers.

An annoying argument/information trope

You know what really bugs me? When you're reading an article and it says:

"Last year, 350 bajillion Americans stabbed themselves in the face with a fork"

Yes, that's tragic. But the additional thing that annoys me is that nowhere in the article does it say how many people are using forks when they don't stab themselves in the face or at all, how often did people do it last year or in the world, or what the data source is, or if this was a meal accident vs kitchen clean up accidents, or what about people stabbing others like that, or if this is counting repeat offenders or stabby motions or what.

But the biggest annoyance of all is the bigness of the number. How big is that number really? Why that number (which usually sounds like it is quite a bit more than the number of forks or people with the capacity to do such a thing). It's like magical thinking, saying a big exact number invokes some mystical 'wow'. It's a very specific thing for a very fuzzy idea. Self stabbing bad. A lot bad. Wow, lots of bad things is bad. Wow.

Oh, so you want me to be specific? OK, specifically any article anywhere that mentions a number. Mostly science popularization articles.

Sure, the main problem is the base rate fallacy, but it's so much further down the scale than that. It's the 'Wow, a number' fallacy.