Machine learning (ML) is a process that converts data into models that can be used to create AI solutions, and the most successful ML models have been based primarily on artificial neural networks. Despite being useful, these approaches have serious fundamental problems, not the least of which is that they produce automation that is difficult, even impossible, for us to fully understand.
Formal AI forgoes artificial neural networks and instead directly models its solutions as computer programs. These programs are written in text formats that are both human and machine readable. Just as we program software and hardware, so too will formal AI. Both the formal AI framework and the solutions it produces will be in source code form that we can understand, along with any needed data.
Each formal AI is a computer program, and with programming comes types and type systems. A type can be thought of as a blueprint that is used to automatically certify the behavior of a program.
The ability to certify program behaviors is one of the most important advantages of the formal AI approach. It makes it possible to precisely specify the laws, rules and regulations for each AI, as well as its values and societal norms. All of this information will be specified through what we call legal and moral types.
Program correctness for formal AI is defined completely in terms of types. This allows each implementation to be correct by its very construction; it either satisfies its blueprint or it will not be built at all. This is an extremely important property that affords a greater trust and reliability in the process.
Other approaches in AI rely almost exclusively on testing that can only take place after the solution has been created. This can lead to undetectable defects in automation, especially when combined with an inability to fully understand the system.
Instead of being trained, we prefer to say that a formal AI is constructed. This means that each formal AI is built up from simpler building blocks, each of which is mathematically guaranteed to conform to its type.
Types will also be used to improve — but not guarantee — the safety and security of formal AI, just as they do with ordinary programs. And it should be pointed out that every formal AI is also just an ordinary program, even though it may be of extraordinary sophistication.
Formal AI is a kind of computer programming, and, as a result of this, it will never be limited to any one set of approaches. This flexibility opens up the potential for the highest possible efficiency, as formal AI will be able to target any computing device or platform we can ever physically realize.
Current ML/AI approaches are also a form of automated programming, but they produce programs — opaque models — that we can not fully understand, and this problem will only get worse as data and model complexity increase. These opaque methods are constrained to the foundations upon which they are built, which are necessarily a subset of the very computer programming tasks they intrinsically rely upon, yet implicitly deny.
Through programming it is possible to take advantage of the unique features available to each platform or service. This is generally not possible with artificial neural networks because they impose their own structure onto the underlying model of computation. Formal AI can utilize any algorithm or data structure to get the job done, just like the most effective human programmers.
Efficient hardware for neural networks will never be as fast or efficient as the equivalent solutions made by engineering and/or programming the specialized hardware or software needed for each use of automation.
With formal AI it will be possible to use the least amount of resources to do the most amount of work. This will democratize access to automation by lowering the computational demands, making it more affordable. This also indirectly lowers the energy requirements by allowing the same solution to work with less powerful devices, which will lead to broader applications and increased scalability.
What can we learn from the most advanced ML/AI models? Whatever the answer, nothing can possibly compare to having the equivalent model in human understandable source code and data.
Having the source code and data will lead to AI that is highly modular and reusable. This means it will be possible to construct AI by combining the parts from previously created AI programs.
Imagine a global library of formal AI components as free and open source software and/or hardware. These could then be used to reduce or even eliminate the time that is needed to create new solutions, similar to how we increase productivity by reusing software through manual programming today.
The knowledge aspect is the most exciting frontier of formal AI, as it is a prelude to automated research. Each AI we create will have the potential to be a unique artifact that can be shared, studied and improved upon. This goes far beyond reproducibility. Formal AI will not only accelerate progress in artificial intelligence, but quite possibly the very things we automate.