A Logical Formalisation of a Hypothesis in Weighted Abduction: towards User-Feedback Dialogues
Shota Motoura, Ayako Hoshino, Itaru Hosomi, Kunihiko Sadamasa
TL;DR
The paper tackles theChallenge of fixed, application-specific weights in weighted abduction not aligning with user plausibility. It introduces extended hypotheses and hypothesis graphs within a many-sorted second-order logic framework and presents two user-feedback dialogue protocols, Basic and Simple, that iteratively refine hypotheses in response to user input. The authors prove halting and convergence properties for these protocols under reasonable restrictions, and they analyze their behavior for both hypotheses and hypothesis graphs, including ablation studies. The work advances a formal, interactive approach to hypothesis selection, with practical implications for domains requiring explainable, user-aligned abductive reasoning, while also identifying computational bottlenecks like subgraph isomorphism for real-world applications. The results offer a principled foundation for deploying user-guided abduction in domains such as plant operation, cybersecurity, and discourse analysis, along with avenues for future approximations and empirical validation.
Abstract
Weighted abduction computes hypotheses that explain input observations. A reasoner of weighted abduction first generates possible hypotheses and then selects the hypothesis that is the most plausible. Since a reasoner employs parameters, called weights, that control its plausibility evaluation function, it can output the most plausible hypothesis according to a specific application using application-specific weights. This versatility makes it applicable from plant operation to cybersecurity or discourse analysis. However, the predetermined application-specific weights are not applicable to all cases of the application. Hence, the hypothesis selected by the reasoner does not necessarily seem the most plausible to the user. In order to resolve this problem, this article proposes two types of user-feedback dialogue protocols, in which the user points out, either positively, negatively or neutrally, properties of the hypotheses presented by the reasoner, and the reasoner regenerates hypotheses that satisfy the user's feedback. As it is required for user-feedback dialogue protocols, we then prove: (i) our protocols necessarily terminate under certain reasonable conditions; (ii) they achieve hypotheses that have the same properties in common as fixed target hypotheses do in common if the user determines the positivity, negativity or neutrality of each pointed-out property based on whether the target hypotheses have that property.