Fight The Lemmas

Posted on October 3, 2017 by Spencer

Reliable and Interpretable AI lecture was so cool!! A PhD student, Dana, was standing in for the prof, and she talked about her own research in “Exact Programming by Example”.

Dana tackled the problem of learning a logical formula from a set of examples. The formula had to be expressible as a disjunction (big OR) of predicates (things like isAdult, isFemale), etc.

She made this cool implication graph and used properties of the graph to search the hypothesis space of formulas. I thought I understood it…

Then I went to Mittagsseminar, which was cool, about “adversarial edge coloring”, grabbed some free leftover dessert with the other Mittagsvolk in the VIS lounge (met a girl I’d seen at Tanzquotient!) and then brought some to Martin, who was studying. Ran off for exercise, then lunch, then met Martin again to study. Martin had been reviewing the morning’s lecture and got hung up on a little detail at the beginning of the Exact PBE slides..

Fighting the Lemmas

After that, we were in the CAB for nearly 5 hours. We found one mistake in the slides, thought we were mistaken in our identification of the mistake, corrected another diagram with lots of hard work and logic and realized we were right, corrected the lemma, found another broken lemma and figured that out too. By the time we got to the main algorithm, we were almost too tired to understand it, but understand it we did in one last heroic effort.

Walk for a Wii

Returned to Culmann about 7:30, ready to socialize and let my brain slip into oblivion. I cooked myself a big plate of eggs and sat down with some Italian bros; they thought I was high, I was so out of it. But eventually the food settled in and I noticed that some people (incl. Gideon, Emily and Eric) were setting up a Wii. They needed batteries for the remotes, and Abhi and I wanted to go on a walk, so we killed two birds with one stone. Ruth joined and we walked down to the Coop, grabbed batteries, and came back up.

We fired up the remotes and then MarioKart. Gideon played a game or two, then I stepped in. Ruth and I were about equally skilled and played a bunch of intense games and drank camomile with honey. Tried to get Betty to join us and failed. Hit the hay around midnight.