Agent problem solving by inductive and deductive program synthesis

How do people learn abstract concepts unsupervised? Psychologists broadly recognize two types of concepts, declarative knowledge and procedural knowledge: know-what and know-how. While much work has focused on unsupervised learning of declarative concepts as clusters of features, there is much less clarity on the representation for procedural concepts and the methods for learning them. In this thesis, I claim that programs are a good representation for procedural knowledge, and that program synthesis is a promising mechanism for procedural learning. Prior attempts at AI program synthesis have taken a purely deductive approach to building provably corrent programs. This approach requires many axioms and non-trivial interaction with a human programmer. In contrast, this thesis introduces a new approach called SSGP (Sample Solve Generalize Prove), which combines inductive and deductive synthesis to autonomously synthesize programs with no extra knowledge outside of the program specification. The approach is to generate examples, solve the examples, generalize from the solutions, and then prove the generalization correct.This thesis presents two systems, Spec2Action and HELPS. Given a logical specification, Spec2Action determines the relations to change to perform simple operations on data structures. The main part of its task is to uncover the recursive structure of the domain from the purely logical input spec. HELPS generates sequential programs with loops and branches using STRIPS actions as the primitive statements. It solves generalizations of classic AI tasks like BlocksWorld. The two systems use SAT solving and other grounded reasoning techniques to solve the examples and generalize the solutions. To prove the abstracted hypotheses, the systems use a novel theorem prover for doing recursive proofs without an explicit induction axiom.

Department dc:contributor.department

Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science.

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2008

Author dc:creator

• Fox, Harold, 1979-

Advisor dc:contributor.advisor

• Howard E. Shrobe.

• Electrical Engineering and Computer Science.

Statement dc:rights

• M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission.

Licence dc:rights.uri

• http://dspace.mit.edu/handle/1721.1/7582

Language dc:language.iso

eng

Handle dc:identifier.uri

http://hdl.handle.net/1721.1/45882

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/45882