Simon Colton's Research Interests

Overview
The Development of Automated Theory Formation
More Sophisticated Mathematical Theory Formation Models
The Combination of Reasoning Systems
Applications to Discovery Tasks in Pure Mathematics
Applications of ATF and Combined Reasoning to Other Domains
Improvement of AI Techniques
Automating Graphic Design, Visual Arts and Video Game Design Processes
Addressing Questions of Computational Creativity
Research Collaborators

For a full list of my publications, please visit the webpage here:

www.doc.ic.ac.uk/~sgc/cv.html#publications

 

Overview

I am an Artificial Intelligence (AI) researcher. I aim to stretch the boundaries of the intelligent tasks that computers can undertake successfully. I am particularly interested in questions of computational creativity, where the aim is to enable software to take on creative responsibility in scientific and artistic projects. I lead the computational creativity group, and much of the research described here has been undertaken in conjunction with group members, in addition to colleagues from various Universities and companies in the UK and around the world. For details of research undertaken in the computational creativity group, please visit the webpages here:

www.doc.ic.ac.uk/ccg

We investigate three principal areas of research. Firstly, we have developed and continue to improve upon a novel machine learning algorithm called Automated Theory Formation (ATF), which invents concepts, discovers regularities in data, and uses third party reasoning systems to prove and disprove hypotheses. Secondly, we investigate fruitful ways in which to combine disparate AI methods so that the whole is more than the sum of the parts. Thirdly, we apply ATF and various combined reasoning systems to intelligent tasks involving the simulation of creative behaviour in pure mathematics, bioinformatics, graphic design, visual arts and video game design. We are particularly interested in the technical and sociological challenges involved in building AI software which is independently creative. Our research can be broadly categorised into the eight areas described below.

 

1. The Development of Automated Theory Formation

Automated Theory Formation (ATF) is a novel machine learning technique which has been developed over 12 years, and which is implemented in the HR system. Given some background knowledge, HR forms new concepts from old ones using a set of production rules, and then makes conjectures which relate the concepts, by appealing to empirical patterns in the examples of the concepts. HR then uses third party systems to prove/disprove the conjectures (usually the Otter theorem prover and the MACE model generator). HR also interacts with computer algebra systems such as Maple and Gap, in order to calculate values for concepts. To drive a heuristic search, HR uses a weighted sum - with the weights set by the user - of measures of interestingness for concepts, i.e., having decided which concept is most interesting, HR builds new concepts from this. My book is the main reference text for Automated Theory Formation. The following papers describe some of the fundamental aspects of automated theory formation. The first paper is the main reference for ATF as an Inductive Logic Programming system, the other papers are from quite early on in the development of ATF.
  • Mathematical Applications of Inductive Logic Programming (MLJ 2006) [ pdf ]
  • The HR Program for Theorem Generation (CADE 2002) [ pdf ]
  • An Application-based Comparison of ATF and ILP (ETAI 2000) [ pdf ]
  • Automatic Identification of Mathematical Concepts (ICML 2000) [ pdf ]
  • Automatic Concept Formation in Pure Mathematics (IJCAI 1999) [ pdf ]
  • HR - Automatic Concept Formation in Finite Algebras (AAAI 1998) [ pdf ]
  • HR - A System for Machine Discovery in Finite Algebras (ECAI 1998) [ pdf ]
  • The Use of Classification in Automated Mathematical Concept Formation (SimCat 1997) [ pdf ]

 

2. More Sophisticated Mathematical Theory Formation Models

We have taken Automated Theory Formation as the basis for more in-depth studies into how mathematical theories can be formed automatically. In addition to providing extensions to the basic automated theory formation model and providing more background to the subject, these projects have led to more sophisticated systems for mathematical invention and machine learning in general, which take into account philosophical and psychological perspectives on theory formation. The following papers describe some of our projects in this area:

  • Three Next Generation Approaches to Automated Mathematical Theory Formation (MBR 2009) [ pdf ]
  • First Order Logic Concept Symmetry for Theory Formation (ARW 2009) [ pdf ]
  • Towards a Computational Model of Embodied Mathematical Language (AISB 2009) [ pdf ]
  • Automated Meta-Theory Induction in Pure Mathematics (ARW 2008) [ pdf ]
  • Using Formal Concept Analysis in Mathematical Discovery (MKM 2007) [ pdf ]
  • Proving Producibility of Concepts (ARW 2007) [ pdf ]
  • Towards Meta-level Descriptive ILP (ILP 2006) [ pdf ]
  • Managing Automatically Formed Mathematical Theories (MKM 2006) [ pdf ]
  • Using Model Generation in Automated Concept Formation (ARW 2006) [ pdf ]
  • A Model of Lakatos's Philosophy of Mathematics (ECAP 2004) [ pdf ]
  • Lakatos-style Methods in Automated Reasoning (IJCAI 2003) [ pdf ]
  • New Directions in Automated Conjecture Making (ARW 2003) [ pdf ]
  • Semantic Negotiation: Modelling Ambiguity in Dialogue (Edilog 2002) [ pdf ]
  • Lakatos-style Reasoning (ARW 2002) [ pdf ]
  • A Multi-agent Approach to Modelling Interaction in Human Mathematical Reasoning (IAT 2001) [ pdf ]
  • Experiments in Meta-theory Formation (AISB 2001) [ pdf ]
  • Assessing Exploratory Theory Formation Programs (AAAI 2000) [ pdf ]
  • Automated 'Plugging and Chugging' (Calculemus 2000) [ pdf ]
  • Agent Based Cooperative Theory Formation in Pure Mathematics (AISB 2000) [ pdf ]
  • Cross Domain Mathematical Concept Formation (AISB 2000) [ pdf ]

 

3. The Combination of Reasoning Systems

As described above, the HR system for theory formation routinely appeals to third party software as part of its core routine. This led us to address the more general question of when it is possible to combine AI techniques so that the whole is more than a sum of the parts. In total, we have experimented with various combinations of around 20 different AI systems, including descriptive and predictive machine learning systems, model generators, constraint solvers, satisfiability solvers, theorem provers and computer algebra systems. Many of the applications described below make use of a combination of reasoning systems. We have also looked at some more generic ways to combine AI systems. The following papers describe some of our projects in this area:
  • Joined-Up Reasoning for Automated Scientific Discovery (AAAI Fall Symposium 2008) [ pdf ]
  • A global workspace framework for combining reasoning systems (Calculemus 2008) [ pdf ]
  • Applications of a Global Workspace Framework to Mathematical Discovery (ESARM 2008) [ pdf ]
  • Integrating AI Systems for Classification in Non-Associative Algebra (Calculemus 2006) [ pdf ]
  • Employing Theory Formation to Guide Proof Planning (AISC/Calculemus 2002) [ pdf ]
  • A Grid-based Application of Machine Learning to Model Generation (KI 2004) [ pdf  ]

 

4. Applications to Discovery Tasks in Pure Mathematics

Pure mathematics is a unique domain for AI research, as mathematical enquiry involves many diverse forms of reasoning, hence we can look at the question of theory formation in pure mathematics and study computational systems which combine different AI techniques. In addition, the data in pure mathematics is usually error free, hence we can concentrate on pure forms of reasoning without (usually) requiring statistical interpretations. On numerous occasions, we have shown that HR and other systems can make mathematical discoveries of genuine value in graph theory, number theory and various algebraic domains of pure mathematics. In addition, by combining HR with multiple other AI systems, we have achieved new partial classifications of algebraic domains, which were previously beyond any computer (or human). The following papers describe some of our projects in this area:

  • Automatic Construction and Verification of Isotopy Invariants (JAR 2008) [ pdf ]
  • Classification Results in Quasigroup and Loop Theory via a Combination of Automated Reasoning Tools [ pdf ]
  • Automated Parameterisation of Finite Algebras (ESARM 2008) [ pdf ]
  • Computational Discovery in Pure Mathematics (Springer 2007) [ pdf ]
  • The Automatic Construction of Isotopy Invariants (IJCAR 2006) [ pdf ]
  • Automated Conjecture Making in Number Theory using HR, Otter and Maple (JSC 2005) [ pdf ]
  • Automatic Generation of Classification Theorems for Finite Algebras (IJCAR 2004) [ pdf ]
  • Automatic Generation of Classification Theorems for Finite Algebras (ARW 2004) [ pdf ]
  • ILP for Mathematical Discovery (ILP 2003) [ pdf ]
  • The Homer System (CADE 2003) [ pdf ]
  • Making Conjectures about Maple Functions (AISC/Calculemus 2002) [ pdf ]
  • The NumbersWithNames Program (AI+M 2002) [ pdf ]
  • Automated Theory Formation for Tutoring Tasks in Pure Mathematics (CADE 2002) [ pdf ]
  • Semi-Automated Discovery in Zariski Spaces (A Proposal) (ARW 2002) [ pdf ]
  • Mathematics - A New Domain for Datamining (IJCAI 2001) [ pdf ]
  • Automatic Invention of Integer Sequences (AAAI 2000) [ pdf ]
  • On the Notion of Interestingness in Automated Mathematical Discovery (IJHCS 2000) [ pdf ]
  • Automated Discovery in Pure Mathematics (ARW 1999) [ pdf ]
  • Refactorable Numbers - A Machine Invention (JIS 1999) [ pdf ]

 

5. Applications of ATF and Combined Reasoning to Other Domains

While pure mathematics has many advantages, other application domains also stretch the limits of AI systems and their combinations. In order to address the generic nature of the AI systems we have built, we have looked at various non-mathematical applications of ATF. In addition to the projects below, through the supervision of masters projects, we have looked at the usage of HR for musical anomaly detection, for discovery tasks in the gene ontology, for the analysis of board games, and for the discovery of software invariants. The following papers describe some of our projects in this area:

  • Using automated theory formation to discover invariants of Event-B models (Rodin 2010) [ pdf ]
  • Towards the Automatic Invention of Simple Mixed Reality Games (AISB 2009) [ pdf ]
  • Automatic Invention of Fitness Functions, with application to Scene Generation (EvoMusArt 2008) [ pdf ]
  • Boosting Descriptive ILP for Predictive Learning (ILP 2006) [ pdf ]
  • Predictive and Descriptive Approaches to Learning Game Rules from Vision Data (IBAAI 2006) [ pdf ]
  • Automated Puzzle Generation (AISB 2002) [ pdf ]
  • Automated Theory Formation Applied to Mutagenesis Data (ACBW 2002) [ pdf ]

 

6. Improvement of AI Techniques

Given that our overall research goal is to improve the application of AI systems to intelligent tasks, it was sensible for us to question whether combined reasoning systems can improve upon stand-alone systems at standard tasks. Through our experiments with combined reasoning systems, we have shown in many cases that (a) combined reasoning systems can be more flexible in application than stand alone systems (b) combined reasoning systems can be more effective at solving traditional problems than stand alone systems, and (c) combined reasoning systems can undertake intelligent tasks that no single system can attempt. The following papers describe some of our projects in this area:

  • Automatic Generation of Dynamic Investigation Problems (ARW 2010) [ pdf ]
  • Solving Mutilated Problems (ARW 2009) [ pdf ]
  • Prediction using Machine Learned Constraint Satisfaction Programs (ARW 2007) [ pdf ]
  • Expressing General Problems as CSPs (ECAI 2006) [ pdf ]
  • Automated Reformulation of Constraint Satisfaction Problems (ARW 2006) [ pdf ]
  • Automatic Generation of Implied Constraints (ECAI 2006) [ pdf ]
  • The TM System for Repairing Non-Theorems (ENTCS 2005) [ pdf ]
  • Machine Learning Case Splits for Theorem Proving (ARW 2005) [ pdf ]
  • Automatic Conjecture Modification (ARW 2004) [ pdf ]
  • A Grand Challenge of Theorem Discovery (CADE 2003) [ pdf ]
  • Integrating HR and tptp2x into MathWeb to Compare Automated Theorem Provers (CADE 2002) [ pdf ]
  • Automatic Generation of Benchmark Problems for Automated Theorem Proving Systems (AI+M 2002) [ pdf ]
  • Lakatos-style Automated Theorem Modification (ECAI 2004) [ pdf ]
  • Automated Theorem Generation: A Future Direction for Theorem Provers (IJCAR 2001) [ pdf ]
  • Constraint Generation via Automated Theory Formation (IPPCP 2001) [ pdf ]
  • Theory Formation Applied to Learning, Discovery and Problem Solving (MI 2000) [ pdf ]

 

7. Automating Graphic Design, Visual Arts and Video Game Design Processes

While the HR system provided a good platform for the study of how to automate mathematical and scientific creative processes, in order to further study computational creativity, we have also undertaken a number of projects aimed at automating processes in the creative industries. In particular, we have built The Painting Fool (www.thepaintingfool.com) as a software artist, which we intend will be taken seriously as a creative artist in its own right, one day. In order to facilitate the creative construction of scenes, we have pushed evolutionary and constraint solving techniques to the limit. We have also looked into various evolutionary art projects, and we have introduced a new browsing paradigm called Objet Trouve Computing, where the software drives the process as much as the user, but also learns the user's preferences along the way. We have also begun work in automating aspects of the design process for video games. The following papers describe some of our projects in this area:

  • Automated Collage Generation - With More Intent (ICCC 2011) [ pdf ]
  • The Painting Fool in New Dimensions (ICCC 2011) [ pdf ]
  • Ludic Considerations of Tablet-Based Evo-Art (EvoMusArt 2011) [ pdf ]
  • Stroke Matching for Paint Dances (CompAesthetics 2010) [ pdf ]
  • Capturing Player Experience with Post-Game Commentaries (CGAT 2010) [ pdf ]
  • Player classification using a meta-clustering approach (CGAT 2010) [ pdf ]
  • Evolving Pixel Shaders for the Prototype Video Game Subversion (AISB 2010) [ pdf ]
  • Evolving 3D Buildings for the Prototype Video Game Subversion (EvoGames 2010) [ pdf ]
  • Evolving Behaviour Trees for the Commercial Game DEFCON (EvoGames 2010) [ pdf ]
  • Experiments in Objet Trouve Browsing (ICCC 2010) [ pdf ]
  • Automated Collage Generation - With Intent (ICCC 2010) [ pdf ]
  • The Painting Fool Teaching Interface (ICCC 2010) [ pdf ]
  • Combining AI Methods for Learning Bots in a Real Time Strategy Game (IJIGT 2009) [ pdf ]
  • Evolving Approximate Image Filters (EvoMusArt 2009) [ pdf ]
  • Evolving Simple Art-based Games (EvoGames 2009) [ pdf ]
  • Emotionally Aware Automated Portrait Painting (DIMEA 2008) [ pdf ]
  • Amelie's Progress Gallery/Imaginations #1 (CA 2008) [ pdf ]
  • Experiments in Example based Image Filter Retrieval (CMIA 2008) [ pdf ]
  • Experiments in Constraint Based Automated Scene Generation (IJWCC 2008) [ pdf ]
  • Case-based Player Simulation for the Commercial Strategy Game DEFCON (CGames 2007) [ pdf ]
  • Towards a General Framework for Program Generation in Creative Domains (IJWCC 2007) [ pdf ]

 

8. Addressing Questions of Computational Creativity

A number of researchers are taking a longer view, and addressing broader questions in computing, such as the notion of whether a computer can exhibit creative behaviour. Only in recent years has AI software reached a level of complexity and ability that this question can be addressed in a concrete rather than a purely theoretical way. This is a field we have been involved in via research, organisation and participation in various workshops and conferences, since 1999. Given that the HR system undertakes some of the more creative tasks in pure mathematics (such as inventing concepts and making conjectures), we have used HR (and other systems) to look at various notions connected to computational creativity. In more recent work, we have addressed the issues raised by The Painting Fool project, to further our understanding of computational creativity in an artistic rather than a scientific domain. The following papers describe some of our projects in this area:
  • Computational Creativity Theory: The FACE and IDEA models (ICCC 2011) [ pdf ]
  • Computational Creativity Theory: Inspirations behind the FACE and IDEA models (ICCC 2011) [ pdf ]
  • On Impact and Evaluation in Computational Creativity: A discussion of the Turing Test and an Alternative Proposal (AISB 2011) [ pdf ]
  • Computational Creativity: Coming of Age (AIMag 2009) [ pdf ]
  • Bridging the gap between argumentation theory and the philosophy of mathematics (FoS 2009) [ pdf ]
  • Seven Catchy Phrases for Computational Creativity Research (Dagstuhl 2009) [ pdf ]
  • Creativity versus the Perception of Creativity in Computational Systems (AAAI Spring 2008) [ pdf ]
  • Creative Logic Programming (IJCAI 2003) [ pdf ]
  • A Mathematical Theory of Creativity (A Grand Challenge) (GCW 2002) [ pdf ]
  • Lakatos and Machine Creativity (ECAI 2002) [ pdf ]
  • The Effect of Input Knowledge on Creativity (ICCBR 2001) [ pdf ]
  • Evaluating Machine Creativity (ICCBR 2001) [ pdf ]
  • Artificial Intelligence and Scientific Creativity (AISBQ 1999) [ pdf ]

 

Research Collaborators

I've been very fortunate to work with a number of very good researchers, including the following co-authors (in surname alphabetical order):

  • Eduardo Alonso
  • Robin Baumgarten
  • Cameron Browne
  • Alan Bundy
  • Paul Cairns
  • John Charnley
  • Stephen Clark
  • Michael Cook
  • Stephen Cresswell
  • Louise Dennis
  • Lydon Drake
  • Jad El-Hage
  • Andreas Franke
  • Alan Frisch
  • Pablo Gervas
  • Yi Gao
  • Jeremy Gow
  • Gudmund Grov
  • Marcus Guhe
  • Ferdinand Hoermann
  • Andrew Howlett
  • Marc Hull
  • Sophie Huczynska
  • Andrew Ireland
  • Ning Jiang
  • Anna Krzeczkowska
  • Daniel Kudenko
  • John Lee
  • Andrew Lim
  • Chong-U Lim
  • Maria Teresa Llano Rodriguez
  • Ramon Lopez de Mantaras
  • Derek Magee
  • Andrew Martin
  • Roy McCasland
  • Andreas Meier
  • Ian Miguel
  • Paul Miller
  • Luc Moreau
  • Mark Morris
  • Stephen Muggleton
  • Maria Nika
  • Ramon Otero
  • Maja Pantic
  • Azalea Raad
  • Ramin Ramezani
  • Daniel Ramirez-Cano
  • Graeme Ritchie
  • Stefan Rueger
  • Paulo Santos
  • Michael Schroeder
  • Murray Shanahan
  • Alan Smaill
  • Volker Sorge
  • Kostas Stathis
  • Graham Steel
  • Oliviero Stock
  • Geoff Sutcliffe
  • Pedro Torres
  • Michel Valstar
  • Toby Walsh
  • Daniel Wagner
  • Dan Winterstein
  • Jurgen Zimmer