Informatics Research Methodologies

Literature Survey Suggestions

The following are only suggested topics. You are not restricted to them. They are organised by research area to assist your search.

Each of the topics represent significant recent successes in their areas. Some are small enough that most of the major papers could be covered in a few weeks. Some are too large for all the major papers to be read, but a smaller subset could be identified. The proposers names are given in parentheses after the topic name. If you are stuck for initial references then these people might be able to give you some pointers.

• Automated Reasoning
  
  
• Machine Learning
  
  
• Planning
  
  
• Vision
  
  
• Miscellaneous
  
  

Automated Reasoning

• Saturation-Based Theorem Proving Methods. (Alan Bundy) Ganzinger, Bachmir and others have had considerable success in applying ideas from orderings in term rewriting to resolution and paramodulation. The paramodulation work was covered by Mark Longair in 1998-9, but the resolution work is still available for survey.
• Integration with CAS. (Alan Bundy) There is a lot of current interest in integrating Computer Algebra Systems (CAS) with Automatic Theorem Provers (ATP). This interest comes from both the CAS and ATP communities. For instance, Clark built an inductive theorem prover on top of Mathematica resulting in a powerful system, Analytica. The ATP community is interested in harnessing the powerful computational abilities of CASs for solving subproblems, analogous to (and sometimes being) decision procedures. The CAS community is interested in using ATPs to establish the preconditions of CAS method and also of verifying their correctness. The Calculemus workshop series is a good starting point.
• Cover Set Induction. (Alan Bundy) Kapur and Zhang invented cover sets as a method of constructing induction rules to prove a conjecture. The technique builds an induction rule whose well-founded order is a reduction order, like recursive path order, but customised to the conjecture. It thus adapts some of the most successful aspects of inductionless induction to explicit induction proofs.
• PVS. (Alan Bundy) PVS is a newish theorem prover developed by Rushby at SRI in California. It has rapidly become the state of the art theorem prover for formal verification of systems. It builds-in a wide variety of techniques including decision procedures, model checkers and tactics. These combine to provide a powerful system in which quite difficult proofs can be rapidly constructed. Lots of people are turning to PVS as the prover of choice for their applications.
• Isabelle. (Alan Bundy) Isabelle is a generic theorem prover written by Paulson at Cambridge. By "generic" I mean that it can be readily adapted to a wide variety of different logics. A lot of energy has gone into the engineering with the result that it is a popular choice for people who need a theorem prover to explore a new logic, but without the hassle of building their own.
• Interactive Theorem Proving. (Alan Bundy) There is a widespread interest in interactive theorem proving, where the user guides either the whole proof or the key steps. This is too large a topic in itself for a literature survey, but there are a number of topics within it that could be focussed on. There is now an annual conference, UITP (User Interfaces for Theorem Provers) with TP interaction as its sole topic. The proceedings for UITP might suggest a theme. An example is "proof by pointing" in which applications of rules of inference are uniquely associated with each part of the current goal, so that the entire proof is conducted by mouse click.

Machine Learning

• New Rule Discovery Methods. (Peter Ross) In the practical world of data mining, people wish to discover sets of rules that in some way `summarise' a big set of data. Long-established methods use inductive algorithms based on ideas such as entropy, so that (assuming the data consists of a big set of vectors) one first finds the most relevant/result-indicative field x_i and then splits the data into subsets according to the value of x_i, and proceeds recursively. The output is a tree, and paths from the root to the tips each describe a rule of the form

    if x_i has value v_i and x_j lies in the range [a,b] and ..
    then outcome = o_n
  

  However, such a set of rules can be cumbersome and insufficiently concise for practical purposes; after all, the set of such rules does give a precise result for every member of the original data set, and can be a large set.

  Often, users might like something smaller but less precise: a set of fuzzy rules that doesn't classify everything in the original training set perfectly, or a set of rules that reaches a classification by a point-scoring process: add 3 for the presence of this feature, deduct 5 for the presence of that (compound) feature, and so on; if the final total is positive then accept else reject. For example, this is how a US Patriot missile station decides which aircraft to target :-(, there being a requirement that the set of rules is small and very fast to apply so that the electronics can continuously monitor many hundreds of aircraft simultaneously. Yet other approaches use different rule formats, eg "if at least N of the following M conditions apply: [..,..,..,...], the result is X"

  Survey the state of the art. Pay attention to matters such as efficiency, accuracy of the final rule set, scalability to huge data sets (eg millions of mortgage applications). Part of the problem for you will be discovering appropriate search keywords and appropriate conference proceedings to look at. You might like to begin by inspecting www.kdnuggets.com, an on-line newsletter about data mining that contains many links to commercial systems and vendors although not so many research activities.

• Particle Filters (Chris Williams) Consider the problem of tracking a moving object. This involves representing the posterior distribution at each time step, and updating this information at the next time step as new observations arrive. For a linear-Gaussian model this can be accomplished analytically using the Kalman filter, but new methods are needed in the case that the dynamical system is non-linear or the noise non-Gaussian. A recent area of research is the "particle filter" method, where the distribution is represented by a sample of points from it. Blake and Isard used this method in their "Condensation" algorithm for tracking, and it has also been developed in the statistical literature, e.g. by Kitagawa. The particle filter method has the power to deal with multimodality, which is a problem with EKF (extended Kalman filter) approaches which are based on linearizations of the non-linear problem. Interesting questions arise when carrying out parameter estimation with this model (using operations analagous to the forward-backward algorithm for HMMs). Note that the object being tracked might not be a physical object, but could be e.g. parameters in a system changing over time.
• ICA: Independent Components Analysis (Chris Williams) Factor analysis models visible data in terms of a linear combination of latent (or hidden) sources, where the sources have independent Gaussian distributions. Recently this model has been generalized to allow non-Gaussian sources and called ICA. One application (called blind source separation) is to the separation of k linearly-mixed sources into the k original sources. There is also a development by Attias called independent factor analysis. There has been quite a lot of work and several meetings on this topic over the last few years.
• Active Learning (Chris Williams) The usual supervised machine learning problem is that you are given some training data and asked to build a predictor. But what if you could make specific queries, i.e. ask for the outupt corresponding to the input x which you choose. How would this help learning, and what x's should you request?
• Boosting (Chris Williams) There has been a lot of interest in boosting over the last few years. Here, a "simple" learner (e.g. a perceptron) is trained on a dataset. The examples it labels incorrectly are then weighted more strongly, and the classifier is then trained again. This is repeated, and the n classifiers so produced are then combined. The original algorithm is due to Freund and Shapire, but there are many later developments. A statistical view of boosting has been given by Friedman.

Planning

• Application of genetic programming to AI planning. (John Levine) Genetic programming is a recent technique (Koza, 1992) for automatic programming based on the induction of programs by evolutionary means. It has been applied to a variety of tasks, including motion planning in robots and AI planning in general (Banzhaf et al, 1998, p343). This survey would summarise the key work in genetic programming applied to AI planning and could attempt to summarise any recent GP techniques which are particularly applicable for the task of finding plans.
• GraphPlan and SATplan. (John Levine) planning competitions have been held at the last 2 AIPS conferences (1998 and 2000). The STRIPS planning competition has been dominated by two approaches: GraphPlan (Blum and Furst 1995) and SATplan (Kautz and Selman 1992, 1996). Daniel Weld summarises the two approaches in a paper written in 1998 (published in 1999). The purpose of this survey would be summarise the key influential papers for the two approaches and would bring Weld's survey up to date, especially to take account of the AIPS-2000 competition results.
• Mixed-Initiative and Advisable Planning Systems. (John Levine) some real world planning problems are too difficult to solve automatically, or are such that the machine needs to be given guidance or advice in order to construct an acceptable solution. This survey would look at the areas of mixed-initiative planning (e.g. James Allen's work on TRAINS and TRIPS) and advisable planning (e.g. Karen Myers work at SRI) and compare the two approaches.
• Applications of AI planning. (John Levine) in an article in Knowledge-Based Systems Vol 13 (2-3), Ruth Aylett describes some real world applications of AI planning technology, such as the Optimum-AIV system used by the European Space Agency for planning the integration of equipment into the Ariane rocket. This survey would summarise and give details of the AI planning techniques used in these and other applications of AI planning.
• Plan visualisations. (John Levine) users of planning systems need to see the plans the machine is creating, either to evaluate them as an end product, to put the plan into action, or to suggest the next step in creating or modifying an unfinished plan. This survey should summarise the key work in presenting visualations of plans, including the use of natural language generation to produce documents from plans.
• Plan evaluation. (John Levine) modern approaches to planning often seek to produce the shortest plan (in terms of number of steps), rather than the best plan. However, there are many other ways to evaluate a plan: the cost of the plan, the time taken to perform the plan, the brittleness of the plan (how likely is plan failure and how easy is it to recover?), and others. This survey would summarise work done in the automatic evaluation of plans, and comment on the domain independence of the various metrics proposed.
• Distributed (Multi-Agent) Planning. (John Levine) when people work on large planning problems, they often break the problem into pieces and work on sub-problems individually, later bringing the solutions to the sub-problems together. Doing this by machine involves distributed multi-agent planning. This survey would summarise work done in this area and attempt to characterise the types of planning problem for which this technique is useful.

Vision

• Colour constancy. (Bob Fisher) Color constancy is the ability of humans to perceive approximately the same colour for a surface, independent of the illumination on the surface (which actually greatly affects the light reflected from the surface, which we in turn observe). No satisfactory machine vision approach to color constancy had been developed before 1990, but recent work, particularly by Finlayson and Funt, suggests this problem is close to being solved.
• Structure from motion, with and without uncalibrated cameras (eg. handheld camcorders). (Bob Fisher) The confluence of 1) better understanding of stereo and projective geometry, 2) more computational power and 3) image sequences from camcorders has now meant that people can construct 3D scene models from either calibrated or uncalibrated cameras. This is the most exciting area of computer vision in the past 5 years. Key researchers are: Zisserman, Hartley, Maybank, Faugeras, Zhang.
• Deformable shape models. (Bob Fisher) The utility of rigid 2D geometric models was exploited to exhaustion in the 1980's, but many 2D objects, or 2D projections of 3D objects do not have constant shape. Consequently, a lot of research has taken place into methods that represent families of shapes with slight, but systematic variations. The most famous approach is by Cootes, who showed how to represent the natural variations by the first few principal components of the distribution of shape variation. Variations on this concept have now appeared in many 2D, 3D and appearance-based problems.

Miscellaneous

• DNA Computing. (Peter Ross) This field is still small enough to survey. The original work was done by Leonard Adleman of USC, who showed that it was possible to solve tiny travelling-salesman problems by getting fragments of DNA to combine into longer fragments, eventually producing a complete solution. The topic is made possible by the fact that you can now specify a short DNA sequence, say ACTGGCTTAA, and for a few dollars you can get a test tube full of such fragments made to order almost at once. His idea was that you might represent a city by a half-length of such a fragment, say ACTGG or GAATT (whose DNA complement is the other half of the the above string, namely CTTAA), so that above fragment represents the possible step from city ACTGG to city GAATT. Two strings, such as the one above and another such as GAATTCCGGT, would then tend to combine to produce a long fragment of double-helix

      ..ACTGGCTTAA
             |||||
             GAATTCCGGT..
  

  representing a two-step fragment that might, or might not, be part of the shortest tour. In general, single-step molecular fragments are so tiny and can be so abundant that a huge space of possible solutions can be explored, effectively in parallel - although, of course, not with perfect reliability.

  Since then the field of DNA computing has spawned a lot of interest, adapting and generalising the idea to tasks such as large-scale propositional reasoning. Survey the state of the art; pay attention to questions of combinatorics, scalability, speed and reliability for solving large practical problems, as compared with more conventional computational techniques. You will find various websites devoted to DNA computing; the main ones [private opinion] may not turn up in the first few shown by your favourite search engine. There is no single journal for the topic yet. Do not confuse Leonard Adleman (USC) with Leonard Adelman (GMU) :-)