Jaxon’s Chief Data Scientist describes Domain-Specific AI Language or “DSAIL” as “a formal specification language within a formal reasoning system that uses formal methods.” But what does that actually mean since it’s clearly not wearing a tux and going to the opera? Let’s break it down.
Formal methods are techniques used to model complex systems as mathematical entities. In other words, formal methods are the math that allow us to analyze a system and be sure that it’s doing what it should. By building a mathematically rigorous model of a complex system, it is possible to verify the system’s properties in a more thorough fashion than empirical testing, thereby contributing to the robustness and reliability of the system. Using formal methods also brings machine learning engineering in line with other forms of engineering, which have their own formal methods for mathematical analysis.
Crucial to applying formal methods is the underlying model of computation (MoC) that describes, mathematically, how units of computations, communications, and memory are organized and used for formal language reasoning and verification. The MoC plays a crucial role in providing the framework necessary to integrate formal language reasoning, natural language reasoning, and large language models (LLMs), and apply formal methods to analyze and verify the system and its responses.
DSAIL, which underlies Jaxon, is a formal, domain-specific language (DSL), which means that it has well-defined rules, has been designed to express computations, and can be expressed using mathematical notations. It takes English, a highly subjective, variable, and inconsistent natural human language, and translates it, via a compiler, into formal language: something easily understood by computers and able to be rigorously analyzed and verified (e.g. fact-checked to avoid hallucinations and errors). More specifically, the DSAIL compiler parses the language into a Boolean satisfiability problem.
A Boolean satisfiability problem is a way to formally determine the validity of a statement and find a feasible solution to a given reasoning problem (e.g. a user’s request) while ensuring responses are not contradictory, wrong, or straight-up nonsense. This technique integrates formal language reasoning with natural language reasoning (what LLMs do) and is a crucial line of defense that Jaxon uses against hallucinations.
Jaxon also applies formal methods for automated model checking and constraint satisfaction problems. Model checking is a formal verification technique that involves verifying certain properties of a system by conducting an exhaustive search of all possible states that the system could enter during its execution (when it’s being used, not murdered). This comprehensive search allows the system to be sure that the given property being checked will remain valid across all possible states. The underlying assumption is that it is a good solution to the given problem if it will work in all cases.
Constraint satisfaction problems are a formal way to ensure that a user is getting what they’re asking for from Jaxon. If a user imparts constraints onto the system, based on business needs, the use case, or any other reasons, those constraints must be honored by the given solution and adhered to. Solvers to constraint satisfaction problems formally ensure that this is the case, again providing some guardrails for the creative solutions that LLMs may come up with.
There are a lot of details that go into Jaxon’s use of formal methods (and a lot of really complicated mathematical formulas), but they all serve the purpose of providing guardrails for (sometimes overly) creative responses generated by LLMs so that the final responses can be trusted. These formal methods quantify, for a computational system, how to reason about generated responses, much as a human fact-checker might, and ensure that they are factual, satisfy any relevant constraints, and work in all cases that apply to the given problem.
Want to learn more? Contact us and let’s get started!
