Last Updated: 2020-12-24
Explainable AI is about describing an otherwise opaque system; the description and the model are separate pieces of information. And that description will only be an approximation unless it is exactly equivalent to the model.
With formal AI, the explanation is the source code and data that makes up the solution itself. In terms of accuracy, this is the best possible outcome because they are the same object.
Having the source code and data to each AI also provides benefits that go beyond the mere understanding of models, such as safety, control and the ability to study and combine AI solutions directly.
A formal AI solution can be thought of as a single unit that combines programs with data in a convenient distribution.
Programs are separated from data so that they can be specialized, and to allow the maximization of human understanding for the algorithms and data structures that are used to implement the AI solution.
A separate data portion is required in order to achieve the most efficient programs. In some cases, data requirements may be extensive. Such quantities of data may require specialized external databases.
Short answer: Yes, if the formal AI produced is made from the tools that are maintained and/or recommended by the Formal AI Institute.
Long answer: It depends on the license and who is creating the tools that are being used to produce the formal AI in question.
Our mission is to ensure that formal AI methods become commonplace, but we can not guarantee that the parties that adopt and/or use these ideas and technologies will follow our same philosophy towards free and open source software and/or hardware.
The tools created and maintained by the Formal AI Institute will always be under a free and/or open source license, and clauses will be added, if necessary, to ensure that the source code and data generated by these tools can be used for commercial purposes, including their use within proprietary products and services. Such clauses may not hold true for tools created elsewhere.
To understand these issues requires knowing at least an overview of how formal AI works:
Each formal AI that is produced is created by one or more formal AI tools. The output of these tools are formal AI solutions, each of which may include source code and data files. Though, for simplicity, we may refer to all of this information as data, as source code is itself a form of data.
Formal AI tools may be embedded in the solutions it generates. This would allow for self-replicating formal AI systems that continuously improve after deployment. This is why it is important for there to be a distinction between the output of formal AI tools and the tools themselves.
On the one hand, our intent is to maximize the choices available to producers of formal AI, and the logical choice is to embrace the proliferation of proprietary products and services that are based on formal AI methods.
On the other hand, the Formal AI Institute strongly encourages producers to share their improvements to formal AI tooling. That way we can all work together to accelerate progress in artificial intelligence.
There is reason to be optimistic, as many organizations are already involved in supporting free and open source software of all kinds. And we believe their support will be vital to ensuring the maximum distribution and use of formal AI technology.
We believe it can. Formal AI tools will produce solutions that contain computer programs and data. These programs can be expressed in languages that have powerful type systems. Types can then be used to specify the exact behavior of each formal AI solution.
Producers of formal AI may wish to encode laws, rules and values into their AI. Types will enable producers to perform this encoding in a very precise way, and with the full force of constructive mathematics at their disposal.
A type is like a blueprint that tells us how a program should be built. However, there is at least one major difference between types and blueprints: we can mechanically verify that programs adhere to their types in a way that is correct by construction.
By contrast, we can only know a building or device follows its blueprint by testing and measurement up to some error tolerance.
Under a type-directed framework, programs are composed of fundamental building blocks that are mathematically guaranteed to be correct.
This correctness also applies to how the building blocks of programs are allowed to be put together.
The overall process ensures that programs are either built according to plan or not at all.
A legal type will encode one or more laws, rules and/or regulations by constraining the behavior of a program.
A moral type is exactly like a legal type, except that it is intended to capture ethical principles, moral values and cultural norms.
There are many situations where social program behaviors are expected that are not otherwise covered by laws and regulations. Moral types are meant to provide a conceptual template for such scenarios.
It is highly likely that more categories of types will be created to handle the social and behavioral details of formal AI implementations.
Ultimately, all of these distinctions collapse to just being types, and they will all operate on the same principle of constraining the behavior of programs and data.
The Formal AI Institute will not be involved in any political or legislative activities. Formal AI is a value neutral technology, and each user of this technology will be responsible for designing and specifying their own types.
In this context, values refer to any law, rule or custom belonging to a culture, organization or individual.
For a technology to be value neutral it must be possible to design it with complete precision. This is because the values in a technology are determined by its design, which includes the data it uses.
Any technology that lacks the ability for us to fully understand its design is incapable of being value neutral, even if it is highly adaptable.
A technology may also have values that change when its data changes. For example, a video game may be rated for one age group in a single-player mode, but unrated when connected to other players over the Internet.
Allowing technology to change its values based on new information is a design choice. There are solutions that may allow new data to be constrained to a particular set of values, but that is beyond the scope of this answer.
There are several properties that make formal AI a value neutral technology:
It is possible to know exactly how each formal AI is constructed.
The data that is used during the operation of each formal AI can also be known exactly.
Any given approach to AI may have implicit values, but formal AI is not limited to a single approach.
Formal AI will never be limited to a single approach because it is actually a form of automated computer programming, and programming is a most general activity.
The space of all possible computer programs is vast beyond comprehension, and all of its solutions are available to formal AI programs, including the methods and tools that are used to construct them.
Every algorithm and data structure we can realize is entailed in the space of all possible programs, including the answers to general AI — if it can be constructed at all.
Limiting data in this way may require new data serialization formats that support the most powerful type systems, but it is possible. Regardless, any data that is used by a formal AI program will be constrained by the types that specify the program itself. It is just a matter of ensuring that there is a sufficient number of types to cover the use cases of the data that is used.
Assisting in this process is the fact that the data portion of formal AI is required to be analyzable, which will allow producers the ability to verify, filter and modify the data to suit their needs. Further, this data is not used one time and then discarded, but is part of the formal AI solution itself; it remains transparent and analyzable unless obfuscated for deployment.