Robots that reason: cognitive robots
Professor Lin Fangzhen (Croucher Senior Research Fellowship 2006) is Professor of Computer Science at the Hong Kong University of Science and Technology. Lin currently works on: cognitive robotics, answer set programming, computational social choice theory, computer-aided theorem discovery, proofs and their applications in game theory, social choice theory, and software engineering.
At the Hong Kong University of Science and Technology, Professor Fangzhen Lin is exploring the cognitive capabilities of computers and uncovering the ways in which the computational power of an AI can benefit humanity. Lin’s research has resulted in the development of computer-aided theorem discovery programs (CATDP) that have successfully been able to rediscover some simple theorems from a set of mathematical parameters. This AI technique, called knowledge representation, is able to find potential hypotheses, given input from a specific domain. A set of data can then be generated within the domain, and the potential hypotheses derived by the program can then be tested. This identifies the plausible hypotheses pulled from the program’s domain.
At the end of this theorem proving process, either an automated theorem prover or a human being is used to finally prove or disprove the hypothesis. Thus far, Lin has met with huge success; Lin has applied this technology to AI planning, helping to create sequences of actions for agents (robots) within a certain set of parameters (the domain).
The computer aided theorem discovery has also been applied to game theory and social choice theory studies; game theory being the study of mathematical models of conflict and cooperation between intelligent rational decision-makers. Looking at game theory and social choice domain, the question becomes, “what are the patterns?”, as these patterns can lead to new hypotheses and, with further proofing, valid theorems.
CATDP was not only able to rediscover some simpler, already known theories proven by humans, but it also uncovered new theorems, which were as yet unproposed. One of the program’s successes involved reasserting the validity of Arrow’s impossibility theorem; one of the prevailing theorems in social choice theory, which concerns a voting block’s satisfaction with an elected official. In short, the theorem states that when given three or more choices, no voting system will result in a satisfied population, a dictatorship being the exception.
Machine learning in AI
Machine learning is a huge area of interest in the field of AI recently. Machine learning is an unpredictable area, unlike CATDP. Progress in this area can be slow, but has huge potential. With CATDP, a set of parameters are established within the domain for the program, and based on certain inputs, will yield certain outputs. Machine learning is less clear, when putting in information we can’t be sure as to the outcome. CATDP has clear variables. Take, for example, a robot moving across the room. It has a very clear set of possible actions, and each step from one side of the room to the other is clearly defined.
With a smaller room, there are fewer possible routes of action for the robot, and a more clearly defined path. In a similar way, CATDP is able to rule out dead ends and narrow its search within a clearly defined system; the program is able to discover and identify patterns within a specified domain.
CATDP application in cybersecurity
CATDP has potential in screening and scanning other computer programs for flaws or bugs. By first changing a program’s source code into simple order logic (a translation of sorts), CATDP is able to search for patterns which figure out what an unknown program does, which has the potential to aid cybersecurity. Lin’s program is in a prototype implementation phase, available open-source, Lin hopes that this prototype can act as an experimental phase on smaller programs.
In an increasingly digital world, where apps and third party extensions link seamlessly together with personal social media such as Facebook, Skype, and WeChat, there is a growing need for effective cybersecurity and a means of validating third-party programs. Lin’s goal is to create a industry standard system which translates and analyses source code to check for potentially malicious add-ons and code.
In a substantial computer system, it would be mathematically infeasible for human beings to check every aspect of code for potentially compromised sections. Therefore, a computer program such as CATDP, which can analyse code to the extent that it is able to pick out and identify patterns, would greatly simplify debugging and security checking processes.
Programs like this are already in use today.; Facebook has a system for checking any software run through its platform. This helps to cull any programs that could harm its users, however, Facebook’s program is arguably narrow-point, applying solely to software used in association with Facebook. Lin hopes to develop the use of CATDP even further, spreading it to a wider range of applications, including giving software an extra line of protection.
Lin obtained his Bachelor of Science from Fuzhou University in 1983, his Master’s of Science from Beijing University in 1986, and his PhD from Stanford University, USA, in 1991. He has since worked as a research scientist at the Department of Computer Science, Stanford University, 1991-1992, and the Department of Computer Science, University of Toronto, 1992-1996, and currently, the Hong Kong University of Science and Technology. In 2006, Lin won a Croucher Senior Research Fellowship for his work in Cognitive Robotics.
To view Prof Lin’s Croucher profile, please click here.