ExplainabilityTransparencyAccountabilitycs.AI
On Quantifying Literals in Boolean Logic and Its Applications to Explainable AI
Adnan Darwiche, Pierre Marquis
August 23, 2021
Journal of Artificial Intelligence Research
33 citations
3 influential
Key Takeaways
-
Literal quantification offers finer-grained control than traditional variable quantification in Boolean logic, meaning it can distinguish between different states of the same variable (true vs. false), providing more precise analysis tools for understanding AI system behavior.
-
Universal literal quantification has practical applications to explainable AI, though the paper focuses primarily on developing the theoretical framework; this suggests potential for creating more rigorous methods to verify and explain AI decision-making processes.
-
The researchers identified specific classes of Boolean formulas and circuits where quantification can be computed efficiently, indicating that these explainability techniques may be computationally feasible for real-world AI systems rather than remaining purely theoretical.
-
This work refines quantified Boolean logic by treating literal quantification as a fundamental primitive rather than deriving it from variable quantification, which the authors argue better captures the logical structure needed for explainability applications in AI.
Abstract
Quantified Boolean logic results from adding operators to Boolean logic for existentially and universally quantifying variables. This extends the reach of Boolean logic by enabling a variety of applications that have been explored over the decades. The existential quantification of literals (variable states) and its applications have also been studied in the literature. In this paper, we complement this by studying universal literal quantification and its applications, particularly to explainable AI. We also provide a novel semantics for quantification, discuss the interplay between variable/literal and existential/universal quantification. We further identify some classes of Boolean formulas and circuits on which quantification can be done efficiently. Literal quantification is more fine-grained than variable quantification as the latter can be defined in terms of the former. This leads to a refinement of quantified Boolean logic with literal quantification as its primitive.