Hello!

In general, I am interested in the problem of automated design. Given some functional primitives, methods of combination, and methods of abstraction, how can a computer system automatically construct systems to satisfy particular goals?

This part of computer science is commonly called classical artificial intelligence. Basically, the stock-in-trade is logic and complex representations instead of the statistics and vector algebra prevailing in modern, perception & learning focused artificial intelligence.

Specifically, I am interested in abstract planning. In ordinary planning, a program is given a start state and a goal state and must form a sequence of actions that will change the world from the start conditions to the goal conditions. I am interested in making general plans, that can go from any of a set of start states to any of a set of goal states. Such a plan would not just be a linear sequence of steps, but it must include conditions, loops, and subroutines. Essentially, this is program synthesis.

In general, this is pretty difficult (you wouldn't need computer programmers if the computer could just program itself!) I've been working on some simpler, more specific problems. One way of looking at program synthesis is as transforming a logical description of a problem (what you want the computer to do in general) into an operational recipe (a step by step list of instructions). Just as compilers have many intermediate representations of a program before they produce machine code, there are many intermediate logical representations of the program that are not fully operational, but that are closer than the original specification. This is where I am at now. I am trying to generate programs to perform operations on data structures (e.g. inserting into a circularly linked list, moving the minimum element of a list to the front) However, the programs produced are still relatively schematic, and they aren't yet abstract plans that would resolve to a sequence of primitive actions for a specific start state and goal state.

Here are some details: I represent the world at any given time as a set of relations. At a high-level, a program specifies how to change this set of relations (through additions and negations) in all worlds satisfying a particular predicate or condition. So, given a start condition and goal condition (specified in first-order logic), I generate examples, solve those examples, generalize from the solution, and then attempt to prove that the generalization is correct for all possible problem instances. This is a type of explanation-based learning, a classical machine learning technique, applied to a different context.

Proving the correctness of a generated program completely autonomously turns out to be the most difficult problem in this research agenda. As part of the solution, I've built a higher order theorem prover. The main contribution is a strict separation between the prover machinery and the proof language. The language allows you to write very modular, high-level proofs of basically any mathematical fact. The machinery is responsible for filling the gaps and making sure each step is justified by the ones before it.

Why am I doing all this in the first place? I became very interested in the way that people acquire motor-coordination skills. Think of someone learning to play a video game or a new sport or learn to use a new piece of equipment. At first they are slow and awkward and they also have to reason through each step of what they want to do. As people become experts, they become faster and less conscious of what they are doing. I interpret this as the brain learning common action patterns and strategies for the particular domain. In computer terms, this would be generalizing different, specific solved plans into an abstract program. I think program synthesis is an important problem for artificial intelligence, because I think it is something humans do in their high-level cognition. I'm also a firm believer that most of the important knowledge we have is procedural knowledge and not declarative knowledge: i.e. know-how, not know-what. We know where our friend's house is by imagining the sequence of turns and landmarks we hit as we walk there. We are less likely to remember their specific address. Program synthesis is one way I think that computers could learn procedural knowledge the way that humans do.