How to validate artificial intelligence
One of the challenges with robots based on artificial intelligence is to ensure that the robot does not suddenly do anything unexpected that can have major consequences. Researchers from SDU are working on creating a new method for validating artificial intelligence.
Robots, which are based on artificial intelligence, generally use trial and error. This means that the robot tries different options until it finds the best solution. This is, for example, how some self-driving vacuum cleaners work, when they move across the floor until they hit an object. Afterwards they change course and remember that here was an object that they should not drive into again.
This way of functioning works fine when it comes to cleaning the floor. But when it comes to more critical systems, such as in relation to air transport or medical diagnosis, there is no room for error.
Luís Cruz-Filipe is an assistant professor at the Department of Mathematics and Computer Science, and he develops computer programs that are used to validate artificial intelligence. His research is part of the "machine-assisted proofs" field and involves putting artificial intelligence into a formula.
Equations too long to be written down
Machine-assisted proof works by constructing a logical statement which lines out all the possible actions of a robot to ensure nothing goes wrong. This means that the statement acts as a kind of "safety net" for the robot not to go astray.
These statements can be long and complicated. In fact, they are often so complicated that even if the researcher himself cannot write it down on paper. The reason for this is that the computer gets some input to start out with and from these inputs, it is possible to create a mathematical setup, which can thus examine all the possible scenarios a robot could get into.
By using machine-driven proofs, it can be checked whether a robot can potentially get into a situation that will be risky or directly harmful. For example, it might be if an aircraft's autopilot should choose a wrong route that could have fatal consequences. This scenario will appear before-hand when using the method of machine-assisted proofs, so the programing of the aircraft can be corrected in due time.
Previously overlooked research
Computer-driven mathematics like what Luís Cruz-Filipe works on, does not have a long history behind it. The field is relatively new, according to Luís Cruz-Filipe, and its practical applications have arisen approx. 15 years ago. He has worked with it himself for the past 5 years and believes that the area is becoming more and more prevalent among researchers within computer science.
In the summer of 2018, Luís Cruz-Filipe was part of the expert panel at ICM2018, the most important international conference for mathematicians. The conference was held in Rio De Janeiro. The ICM is held every four years and it is not yet published where the next ICM will be held.
Photo: Luís Cruz-Filipe, Assistant Professor, IMADA.