Position: XAI needs formal notions of explanation correctness

The use of machine learning (ML) in critical domains such as medicine poses risks and requires regulation. One requirement is that decisions of ML systems in high-risk applications should be human-understandable. The field of "explainable artificial intelligence" (XAI) seemingly addresses this. However, in its current form, XAI is unfit to provide quality control for ML; it itself needs scrutiny. Crucially, popular XAI methods cannot reliably answer important questions about ML models, their training data, or a test input. We recapitulate results demonstrating that various popular XAI methods systematically attribute importance to input features that are independent of the prediction target. This limits their utility for purposes such as model and data (in)validation or improvement as well as scientific discovery. The fundamental reason for this limitation is that current XAI methods do not address well-defined problems and are not evaluated against objective criteria of explanation correctness. Researchers should formally define the problems they intend to solve first and then design methods accordingly. This will lead to notions of explanation correctness that can be theoretically verified and objective metrics of explanation performance that can be assessed using ground-truth data.