Archive for April, 2012

I grade grad AI

This semester I have been co-teaching (with the awesome Martial Hebert) CMU’s graduate artificial intelligence (grad AI) course. It’s been a lot of fun teaching AI to a class where a significant fraction of the students build robots for a living (possibly some of the students are robots, especially the ones who got a perfect score on the midterm exam). Although the last class is on May 2, I already gave my last lecture, so this seems like a good time to share some thoughts.

My general impression is that many AI courses try to cover all of AI, broadly defined. Granted, you get Renaissance students who can write “hello world” in Prolog while reciting the advantages and disadvantages of iterative deepening depth-first search. On the down side, breadth comes at the expense of depth, and the students inevitably get the very wrong impression that AI is a shallow field. Another issue is that AI is so broad that some if its subdisciplines are only loosely related, and in particular someone specializing in, say, algorithmic economics, may not be passionate about teaching, say, logic (to give a completely hypothetical example).

Our version of the course is far from perfect, but we did concentrate on only several favorite topics, and covered them in-depth. We taught a few of the usual topics, but with a twist. Some examples include: upper and lower bounds for randomized alpha-beta pruning, existence of solutions to CSPs using the Lovasz Local Lemma, optimality of A* (in terms of the number of explored nodes) among all admissible algorithms, and the computational hardness of classical planning. In addition, we taught some unusual topics: motion planning (three lectures), perception (three lectures), and, of course, algorithmic economics (five lectures!).

So what should every aspiring AI researcher know about algorithmic economics? Here is my shamelessly biased view.

  1. Computational social choice (first lecture, second lecture): common voting rules, manipulation, the Gibbard-Satterthwaite Theorem, computational complexity of manipulation, applications to multiagent systems and human computation.
  2. Computational game theory (first lecture, second lecture): prisoner’s dilemma, existence and complexity of Nash equilibrium, applications of Nash to interdomain routing (OK, this is a STOC paper, but it’s one of my favorites and I couldn’t resist) and the smart grid, mediated equilibrium, correlated equilibrium and its complexity, Stackelberg strategies, security games, auctions, combinatorial auctions. Covering auctions in 30 minutes is ridiculous, but the Vickrey auction is a must.
  3. Computational fair division (lecture): cake cutting algorithms, strategyproof cake cutting, complexity of fair cake cutting, applications of fair division to resource allocation in data centers (yep, this is a systems paper by systems people, but who’s to say it’s not AI?). Fair division is admittedly a niche area within AI, but it’s been getting increasing visibility in the last AAAIs/IJCAIs and it’s just too much fun to skip.

Sometimes the line between theory and AI (and systems) is quite blurred, but some fun and important topics such as truthful approximation algorithms and the price of anarchy are arguably not AI. Fortunately I’m scheduled to co-teach “great theoretical ideas in computer science” in Fall 2013; one great meta idea seems to be that you can teach whatever you want as long as you can prove it, and I expect that this stuff will make the cut.


Read Full Post »

The newly founded Technion-Microsoft Electronic-Commerce Research Center will hold a one day workshop on electronic-commerce, on May 30th.  They invite submissions for short presentations and posters.

Read Full Post »

The list of papers accepted to EC 2012 have been posted.

Read Full Post »

My colleague Boris Shaliach has been working for years on computerized formalization of mathematics.  After making a name for himself in the 1980’s in the, then hot, AI topic of automatic theorem proving, and getting tenure, he has since continued working on extending this automatic theorem proving to the whole of mathematics.  His work is certainly no longer main stream AI, and he does not “play” the usual academic game: he hardly published anything since the late 80’s, and to this date he does not have a web page.  I have to admit that most of us in the department did not believe that anything would come out of this research, politely calling it “high risk high yield”.  However as he is an excellent teacher, was able to get a steady stream of European grants, advises a very large number of graduate students, and in general is friendly and interesting to talk to, everyone likes him.

For years he has been trying to convince everyone that mathematics will soon be done only by computers.  His basic argument was that contrary to our intuitive feeling that mathematics requires the peak of human intelligence, and that the cleverness seen in mathematical proofs can never be replaced by a computer, the truth is exactly opposite.  Mathematics is so difficult for humans precisely because of human limitations: evolution has simply not optimized humans for proving theorems, and this is exactly where computers should beat humans easily.  His example was always how chess turned out to be easy for computers while natural language understanding or face recognition turned out to be much harder because humans seem to be “optimized” for these tasks.  (I have to admit that he held this position even before computers beat the human world champion, pointing out that very early chess programs already beat him.)  In this vein, I could not get him too excited about the recent amazing advances in computerized Go, and he was much more impressed by the success of Google’s language translation and by IBM’s Watson.

His baby has always been a formalized mathematics computer program, called URIM-VETUMIM, that defined a computer-readable language for specifying mathematical theorems and proofs.  He was one of the original group behind the QED manifesto, and is one of not too many researchers still actively working on that goal of formalizing existing mathematics into a computerized readable form. It seems that there is a small industry of computer systems that allow one to formally describe mathematical axiomatic systems, theorems and proofs, and can then verify syntactically the correctness of a proof. His system, like many in the genre, uses the Zermelo-Fraenkel set theory as its axiomatic system and he has spent an enormous amount of effort trying to enter larger and larger pieces of mathematics formally into the system.  In fact, for about 20 years he has provided jobs for many undergraduate students in the math department who were paid for taking standard math textbooks and formalizing them into his URIM-VETUMIM system.  This turned out to be much harder than it seems where at the beginning, months would be required for formalizing one little lemma, but over time this became much more efficient, as his steady stream of CS M.Sc. students improved the human interface, adding various short cuts (glorified macros) and sometimes even a little intelligence in the form of proof assistants.  One of the nice things about his URIM-VETUMIM system is that he never worried about students making errors: if it “compiled” into his system then it was correct.

I got involved in his efforts, helping him with the incentives engineering of replacing our math students with a “crowd-sourcing” alternative.  His idea was to utilize Chinese math students who are very good and  yet are willing to work for really low wages.  He had some contacts in leading Math departments in China, and I helped him a bit as he set up a nice Mechanical-Turk-like system optimized for having Chinese math students enter theorems and proofs into the URIM-VETUMIM format.

I used to have long discussions with him about what the point of this formalization was: after all he is taking mathematical knowledge that we already have and translating it into a clearly less efficient computerized format — so what’s the gain?  He had two points: first he claims that most proofs in published mathematical papers are buggy. Usually these are “small” bugs that can be fixed by any mathematician reading the paper, but often there are significant ones.  He always pointed out the absurdity that important mathematical proofs (like for Fermat’s last theorem) required more than a year of “verification” by expert mathematicians — really of fixing various holes in them — before they are believed.  His analogy was that writing a mathematical proof was similar to writing a computer program, but there was no “compiler” for mathematical theorems that allowed one to verify correctness.  His second point was that that one first needs a large database of formalized existing mathematical knowledge before one may hope for new computer-invented proofs.

Unfortunately, the various groups attempting the formalization of mathematics have not agreed on a common language, so each group is working on its own pet language, and none of them seems to have reached critical mass so far.  There seems to be some kind of informal competition between the groups about who can formalize more math into their system.  Luckily most of the large systems have either made their database publicly available on the web or were willing to provide Boris with their data.  Indeed in the last decade or so, many of his graduate students built systems that “translated” from the databases of his competitors into his own URIM-VETUMIM format.

Now comes the interesting stuff.  Over the years many of his graduate students did work on various automatic theorem proving ideas, and kept writing more and more programs, each of them doing something better than the previous ones (and other things worse…)  Over the years has has amassed literally dozens of programs that can automatically prove mathematical theorems, each one with some non-trivial yet very limited capabilities. Amazingly he was able to keep all the software of his former students functional and kept running every program on the updated mathematical URIM-VETUMIM database as it grew.  His latest project was to combine all these provers in a “meta-algorithm” of the form that won the netflix challenge where the idea is to combine all the existing algorithms in his arsenal by running them all and choosing the “best” at each point.  Of course the actual implementation is much more nuanced as involves using the large existing database to statistically determine which algorithms are best attempted in which cases, I suppose somewhat similarly to how SATzilla wins the SAT solving contests.  However the combination of partial results from the various algorithms into  single “proof” seems to be rather straight forward since they all just provide mathematical “lemmas” in the URIM-VETUMIM format.  His meta-algorithms now constantly run in the background of his PC cluster, churning new input to the database as well as fine tuning the parameters of the meta-algorithms.

In the last year he has taken this a step forward and has designed a clear API for adding external theorem proving algorithms that are then automatically incorporated into his meta-algorithms.  Building on his Mechanical-Turk-for Chinese-Math-Students setup, he is now crowd-sourcing sub-algorithms for his meta-theorem-proving-algorithm, this time from Chinese CS students.  By now he has paid tens of thousands of dollars to hundreds of Chinese students who have contributed pieces of code.  It seems that at this point it is very difficult to keep track of the contents of the URIM-VETUMIM system: both the mathematical knowledge data and the software have been build over the course of more than 20 years, with different pieces of it coming from various sources.  This seems to be fine as Boris guards closely the core of the system: the URIM-VETUMIM language specification and the proof verifier.

Now comes the punchline: the system just spat out a “proof” of the Reimann hypothesis. The “proof” is a 200Mb long text file that is human-readable in the sense of understanding each line, but with no structure that a human can really understand.  It is clear that the proven “statement” is that of the Reimman hypothesis, and the “proof” is verified by the software to be a formally correct proof of the theorem using Zermello-Fraenlkel set theory (with the axiom of choice, I think).

Now what?

Read Full Post »

%d bloggers like this: