automatic programming, theorem proving & intelligence

[gusl]

I've been working on a difficult programming puzzle, whose main difficulty consists in computing a function efficiently. The specification is therefore much simpler than the solution. This should make it a perfect case for applying automatic programming: what is required is "cleverness", not "knowledge". (of course, this "knowledge" does not include knowledge of heuristics, knowledge of mathematical theorems, etc. (all of which *are* useful), since they are low-Kolmogorov-Complexity, being consequences of just a few axioms.)

It reminds me of something like Fermat's Last Theorem: easy to state, hard to prove. It's also easy to write an algorithm that eventually proves it, but very hard to make it output the proof before the end of the universe: just do a breadth-first proof search through the axioms of ZFC (if we don't want to worry about interpretations or waste time proving non-computable results, then I think substituting ZFC with "Lambda Calculus" will do). The "creativity" lies in finding the representation with which the proof-finding becomes computationally easy. (Could Lenat's and Colton's "automated mathematicians" be applied to Automatic Programming? Kerber is probably interested in the automated design of mathematical concepts: is this applicable?)

The smart way to tackle such problems, therefore, is to do a "representation search". We can implement heuristics used by human mathematicians (Colton and Pease have worked on "Lakatos-Style Reasoning").

Can normal Automated-Theorem Provers find "creative" proofs and "Proofs without Words" of the sort found here? Why not? Because they are missing representations. Jamnik's work could be used to add diagrammatic representations to such automated mathematicians.

This reminds me of Kasparov vs Deep Blue. It seems that Deep Blue won by "brute force". Not brute force alone, of course: without the tons of hours spent on making it smarter, all those computations would still have gotten them nowhere. But a "fair" game would have been one in which Deep Blue's computational resources were limited: you're only allowed so many megaflops or whatever. While it is hard to quantify the computational power of Kasparov's brain (in fact, it's probably a hybrid analog-digital computer), accepting the outcome of the match as indicating that Deep Blue is a "better chess player" than Kasparov is like saying that a retarded giant is a "better fighter" than a tiny man, when "fairness" requires putting them in different weight categories.


Notes:

fare suggests that Jacques Pitrat has done relevant work on automatic programming, but I haven't found such a reference.

simonfunk has suggested that AI could emerge out of compilers, since they are try to be code-optimization machines. One problem with this, of course, is that most programming languages are specified to perform the exact computations determined by the code (maybe not Prolog). The kind of "compilers" relevant here are something like code-generators (given a formal specification). (would very general constraint-solvers be helpful too?). In any case, a compiler that "optimizes" such a function would need to come up with the required representations.

Comments

[mathemajician.livejournal.com]

Well, 10^16 FLOPS is a pretty common estimate of what is needed to simulate the human cortex in real time, thus if Kasparov was using just 1% of his cortex to play chess, then to simulate that you might need 10^14 FLOPS. According to the IBM site Deep Blue did about 10^12 calculations per second.

I think that if Kasparov met a version of Deep Blue with 100x as much CPU power... he'd be in deep trouble.

[gustavolacerda.livejournal.com]

Well, 10^16 FLOPS is a pretty common estimate of what is needed to simulate the human cortex in real time

Simulate to what level? I can imagine lots of irrelevant data being simulated, or just simply a very lossy process. Can you really compare this with the computational capacity of a well-designed digital computer?... and who says Kasparov is using 1% of his cortex to play chess?

[mathemajician.livejournal.com]

Sure, it's hard to know how many FLOPS are needed to simulated the human cortex. And is he using 1% of his cortex for chess, again hard to tell. Other tasks like language use non-trivial proportions of the cortex so it seems likely to me that a pro chess player would use at least 1% of his cortex.

My point is really just this: If I do some basic numbers with reasonable sounding values I get the computation that Kasparov's brain uses to be 100x higher than Deep Blue. You're claiming that it's the other way around, but I haven't seen any argument as to why this is the case yet.

[zarex.livejournal.com]

I thought there was more to the Kasparov loss controversy. I think many were claiming it was unfair because Deep Blue was allowed to "study" earlier games of Kasparov, while Kasparov was not allowed to do the same. [ among other things ]

I think that if it were a fair match, Kasparov would have won.

[brkvw.livejournal.com]

you might enjoy this programming language www.Rebol.com
A littlie like Lisp...

[gwillen.livejournal.com]

(defvar rebol (apply #'buzzword-bingo (apply #'restrictive-license 'lisp)))

It does look neat, though. But I'm rather skeptical.

[(Anonymous)]

Being skeptical is healthy.

But what are you skeptical of exactly?

[brkvw.livejournal.com]

Doh!

[gwillen.livejournal.com]

I'm skeptical that Rebol is anything more than Lisp with a large number of buzzwords added, a large amount of community standardization subtracted, and a restrictive license. (In general I won't use a language for which there is only one implementation... if I can't implement it myself it's too dangerous for me to be stuck with code written in it.)

From their license page: "REBOL/Core is free ... you cannot modify the software."

[brkvw.livejournal.com]

You have addressed separate issues in one sentence. You are welcome to do that. But is your issue it is not OS, that it is more complex than you understand, or that it is a glorified Lisp.

I can do my best to address these:

1. Right, it is not OS, which means you don't get to look at the all the source. However, it even has a command built in to self analyze the code.

2. Complex. I hope so, the creator of Rebol invented preemptive multitasking. One smart cookie.

3. No, it is not a glorified Lisp. We have written over 1M lines of Rebol. We could not have done this in Lisp.

[gwillen.livejournal.com]

My primary issue is that it is not open. I'm not a zealot -- I'm happy to use tools that are closed-source. But not programming tools... my code is critically important to me. I can't entrust it to a black-box system I can't see the inside of. And I can't see good programmers (who are the only ones who would care about the innovations this system offers) being willing to trust it either.

Suppose I wrote a bunch of Rebol and then you went bankrupt? What prevents the language from dying? Suppose I want a feature in the language that you don't care about? Do I need to port everything I've ever written to another platform?

[brkvw.livejournal.com]

OK, so your sticking point is OS.

Then you will have only those tools that are as good as those offered in OS. No worries...

[gwillen.livejournal.com]

Don't get me wrong there either, I'm happy to use closed-source programming tools... but I don't like closed-spec languages, for which there cannot ever be open-source tools, even were I to sit down and write them myself, and I get the impression that Rebol is such a language.

[brkvw.livejournal.com]

I know of several projects to build open source versions of Rebol.