FormIDEAble: Safe and Socially-aware Autonomous Systems

Resumo Técnico do FormIDEAble: Sistemas Autônomos Seguros e Socialmente Conscientes

Definição do Problema
Agentes autônomos operando em ambientes sociocríticos (ex: resposta a emergências) devem coordenar-se com humanos sob condições de incerteza, enquanto aderem estritamente a restrições de segurança. As abordagens existentes enfrentam uma dicotomia: ou modelam a dinâmica social e o comportamento humano sem fornecer garantias formais de segurança, ou oferecem garantia formal ao abstrair comportamentos humanos complexos. Além disso, embora a "Arquitetura de Identidade para Sistemas Autônomos" (IDEA) utilize a teoria da identidade social para fomentar a cooperação, ela baseia-se em um raciocínio de equilíbrio que carece de garantias formais de que as restrições de segurança (como limites de tempo ou priorização de recursos) serão sempre satisfeitas. O desafio central é sintetizar estratégias de tomada de decisão que sejam simultaneamente conscientes do contexto social, formalmente verificáveis e capazes de lidar com a incerteza inerente às respostas humanas.

Metodologia
O FormIDEAble aborda este desafio modelando a interação entre humanos e agentes autônomos como um Processo de Decisão de Markov de Tempo Precificado (PTMDP). Este formalismo integra quatro aspectos críticos:

1. Controle: O agente autônomo seleciona entre ações controláveis.
2. Incerteza: As respostas humanas são modeladas como reações do ambiente probabilísticas e incontroláveis, capturando comportamentos socialmente motivados.
3. Tempo: As ações incorrem em atrasos, e prazos são impostos via restrições temporais.
4. Custo: As decisões acumulam custos que representam objetivos de desempenho (ex: tempo de evacuação, uso de recursos).

O problema de tomada de decisão é formulado como um problema de alcançabilidade com limite de custo. O objetivo é sintetizar uma estratégia $\sigma$ que minimize um custo esperado (ex: tempo) sujeito a uma restrição de segurança: a probabilidade de alcançar um estado de meta $G$ (satisfazendo requisitos de segurança) dentro de um limite de custo $B$ deve exceder um limiar $p$.

O framework é implementado como um loop MAPE-K (Monitor, Analisar, Planejar, Executar, Conhecimento):

• Monitoramento (Monitor): Detecta pontos de decisão e coleta dados contextuais (distâncias, disponibilidade de recursos) e estimativas de identidade social de um "Preditor de Identidade".
• Análise (Analyze): Um "Construtor de Jogo Formal" constrói um modelo PTMDP paramétrico usando padrões reutilizáveis para decisões do controlador e decisões adversariais (humanas) (observáveis e inobserváveis). Um "Solucionador de Jogo Formal" (usando Uppaal Stratego) computa a estratégia ótima.
• Planejamento e Execução (Plan & Execute): O "Seletor de Melhor Decisão" escolhe a ação com a maior probabilidade (menor custo esperado) prescrita pela estratégia, que é então executada pelo agente.

Principais Contribuições
O artigo introduz três contribuições primárias:

1. Formalização: Uma formalização da cooperação entre humano e agente autônomo socialmente consciente usando PTMDPs, capturando explicitamente a incerteza da identidade social.
2. Síntese de Estratégia: Uma abordagem inovadora que integra a incerteza da identidade social com garantias explícitas de segurança ao formular o problema como um problema de alcançabilidade com limite de custo sobre PTMDPs.
3. Evidência Empírica: Evidência experimental inicial demonstrando a eficácia da abordagem em um cenário de evacuação de emergência, destacando os compromissos (trade-offs) entre otimização e segurança.

Resultos Experimentais
Os autores avaliaram o FormIDEAble utilizando o ambiente de simulação IMPACT+ e o Uppaal Stratego contra quatro baselines: sem suporte, sempre chamando socorristas, sempre pedindo ajuda aos sobreviventes e a abordagem IDEA não formal.

• Desempenho vs. Baselines: Em cenários com recursos escassos de socorristas ($N_{fr}=9$), o FormIDEável reduziu significativamente o tempo total de evacuação ($T_{evac}$) em comparação ao IDEA e ao suporte apenas de sobreviventes, mantendo-se comparável à baseline de "sempre chamar o pessoal". Crucialmente, o FormIDEável reduziu consistentemente o número de chamadas para socorristas em comparação tanto com as baselines de suporte de pessoal quanto com o IDEA.
• Previsão de Segurança: O modelo formal demonstrou alta precisão em prever se os requisitos de segurança seriam atendidos, com precisão (precision) e revocação (recall) consistentemente acima de 93% em várias configurações.
• Otimização vs. Segurança: Nos experimentos com Uppaal Stratego, o FormIDEável sintetizou com sucesso estratégias que minimizaram a duração da tarefa. Quando metas de segurança específicas (ex: priorização de crianças ou teto de chamadas de socorristas) foram impostas, o sistema manteve altas probabilidades de satisfazer essas propriedades de alcançabilidade, frequentemente ao custo de um aumento modesto na duração da tarefa.
• Sobrecarga (Overhead): A síntese de estratégia introduziu um overhead de tempo de execução (wall-clock time) não negligenciável, mas modesto (média de <0,5s para configurações pequenas/médias e ~2,25s para complexas), sugerindo adequação para cenários que permitem tempo de deliberação limitado.

Significância e Alegações
O artigo posiciona o FormIDEável como uma fundação principista para a tomada de decisão socialmente consciente e formalmente assegurada. Sua significância reside em unir a ciência social (teoria da identidade social) e métodos formais (síntese de estratégia). Diferente de trabalhos anteriores que tratam segurança e dinâmica social isoladamente, o FormIDEável as integra para garantir que agentes autônomos possam cooperar com humanos sob incerteza sem violar restrições de segurança explícitas.

Os autores são modestos quanto ao escopo atual, observando que a avaliação é preliminar e baseia-se em simulação. Eles reconhecem que a abordagem atualmente requer esforço manual para instanciação de modelos e formalização de segurança. O artigo afirma fornecer os princípios fundamentais de modelagem e síntese, deixando a análise de escalabilidade abrangente, validação empírica mais ampla em diversos domínios sociocríticos e o desenvolvimento de ferramentas de nível superior para trabalhos futuros. A abordagem é apresentada como um passo em direção a sistemas autônomos que não são apenas seguros, mas também socialmente competentes e confiáveis.