Verifiable artificial intelligence. A case study in emergency hospital patients risk assessment

Abstract

Intelligent software systems are increasingly being used in critical domains like the medical health care. Artificial Intelligence in general, and Machine Learning in particular, pose new challenges to Verification, a crucial step of the critical systems development process. Formal Methods, such as Model Checking, are well known techniques that allow for proving properties in critical systems. Current work assesses the usage of Model Checking to perform verification in an emergency hospital patients risk assessment use case. The proposed approach is a framework that contemplates verification steps during both design and run time. In concrete, at design-time, it is able to check a model for invalid end states, non-determinism and accordance with a priori knowledge. Online verification focus on verifying the confidence of a classification (forecasting) for a specific instance, based on a tailored distance measure that checks the closeness to the model decision boundaries. This last phase of verification is also considered as ensemble strategy in a scenario of combining more than one classifier. Experimentation was done on three available risk assessment models (the Risk Scores GRACE, PURSUIT and TIMI) with real data of 460 hospital patients. Verification at design-time for the three models (a) confirmed the inexistence of invalid end states for the whole operation input space nor (b) non-determinism for the available test set, and (c) provided confirmation of compliance with a priori knowledge statements. Online verification (performed for GRACE) successfully divided the available instances (patients) into two groups, Confident and Not-confident about the risk assessment, where (a) the performance in comparison to the baseline improved for the Confident group and degraded for the Not-confident one, and (b) the execution statistics of the model checker proved its efficiency to perform verification at run time. The ensemble strategy was evaluated in two scenarios that considered different overall usage ratios for the verified GRACE model (based on the online verification parametrisation), along with several complementary classifiers. PURSUIT, one of the domain dependent Risk Scores, and a trained Decision Tree Classifier provided the best match to complement GRACE in the classification of instances not-confidently assessed. Based on the results, the proposed framework succeeds in using Model Checking for verification to increase trust on intelligent systems decisions, made in critical domains.

Sistemas de software inteligentes são cada vez mais usados em domínios críticos como o setor da saúde. A Inteligência Artificial em geral e Aprendizagem Máquina em particular, colocam novos desafios à Verificação, um passo crucial no processo de desenvolvimento de software crítico. Métodos Formais, como Model Checking, são técnicas bem conhecidas que permitem provar propriedades de sistemas críticos. O presente trabalho avalia a utilização de Model Checking para realizar verificação num caso de estudo de avaliação de risco em pacientes de emergência hospitalar. A abordagem proposta é uma estrutura que contempla verificação quer na fase de desenho, quer na fase de execução (em linha) do sistema. Em concreto, durante a fase de desenho, é capaz de verificar um modelo para a existência de estados finais inválidos, não-determinismo e a conformidade com conhecimento a priori. A verificação em linha foca-se em avaliar a confiança da classificação (ou previsão) para uma dada instância, baseada numa medida de distância adaptada que indica a proximidade às fronteiras de decisão do modelo. Esta última fase de verificação é ainda considerada como estratégia de ensemble para um cenário de combinação de mais do que um classificador. A experimentação foi realizada em três modelos de avaliação de risco disponíveis (Escalas de Risco GRACE, PURSUIT e TIMI) com dados reais de 460 pacientes hospitalares. A verificação em fase de desenho para os três modelos (a) confirmou a inexistência de estados finais inválidos, nem (b) de não-determinismo para os dados testados, (c) confirmando também concordância com as declarações de conhecimento a priori. A verificação em linha (realizada para o GRACE) dividiu com sucesso as instâncias disponíveis (pacientes) em dois grupos, Confiante e Não Confiante em relação à avaliação de risco, onde (a) o desempenho em relação à execução de controlo melhorou para o grupo Confiante e degradou para o Não Confiante, e (b) as estatísticas de execução do Model Checker provam a sua eficiência para realizar verificação em linha. A estratégia ensemble foi avaliada em dois cenários, considerando rácios de utilização diferentes para o modelo verificado GRACE (baseados na parametrização da verificação em linha), combinados com vários classificadores complementares. PURSUIT, um dos modelos de escalas de risco restritos ao domínio, e um Classificador de Árvore de Decisão treinado nos dados foram os que melhor complementaram o modelo GRACE na classificação de instâncias sem confiança na avaliação de risco. Com base nos resultados, a abordagem proposta tem sucesso em usar Model Checking na verificação para aumentar a confiança nas decisões de sistemas inteligentes, tomadas em ambientes críticos.