MAPE-KV: Una Arquitectura Neuro-Simbólica Verificada para la Orquestación de Enjambres Robóticos

• Daniel Narváez UAI / UNP
• Néstor Balich UAI
• Gustavo Rossi UAI / UNLP

Resumo

Robotic swarm orchestration in the Edge–Cloud Continuum increasingly depends on adaptive planning, yet the use of LLMs introduces stochastic risk into safety-critical cyber-physical systems. We present MAPE-KV, an extension of the MAPE-K loop that inserts a formal verification gate in Lean 4 between planning and execution. The proposal aims to block unsafe plans ante hoc through explicit physical-safety and software-quality invariants. A preliminary proof of concept in the Ester Grid simulator with five robots showed that, in the evaluated scenario, the gate intercepted all unsafe plans observed before execution. This work should be read as an architectural proposal with initial feasibility evidence, not as exhaustive experimental validation.

Palavras-chave: Formal Verification, Robotic Swarms, Lean 4, LLMs, MAPE-K, Neuro-symbolic AI

Referências

Ahn, S., Choi, W., Lee, J., Park, J., and Woo, H. (2025). Towards reliable code-as-policies: A neurosymbolic framework for embodied task planning. arXiv preprint arXiv:2510.21302.

Al-Debagy, O. and Martinek, P. (2020). A metrics framework for evaluating microservices architecture designs. Journal of Web Engineering, 19(3–4):341–370.

Iglesia, D. G. D. L. and Weyns, D. (2015). Mape-k formal templates to rigorously design behaviors for self-adaptive systems. ACM Transactions on Autonomous and Adaptive Systems (TAAS), 10(3):1–31.

Moura, L. d. and Ullrich, S. (2021). The lean 4 theorem prover and programming language. In International Conference on Automated Deduction, pages 625–635. Springer.

Narváez, D., Battaglia, N., Fernández, A., and Rossi, G. (2025a). Descubrimiento automático de microservicios mediante modelos generativos y verificación formal. In XXXI Congreso Argentino de Ciencias de la Computación (CACIC) (Viedma, 6 al 10 de octubre de 2025), Viedma, Argentina. Universidad Nacional de Río Negro (UNRN).

Narváez, D., Battaglia, N., Fernández, A., and Rossi, G. (2025b). Designing microservices using ai: A systematic literature review. Software, 4(1):6.

Obi, I., Venkatesh, V. L., Wang, W., Wang, R., Suh, D., Amosa, T. I., Jo, W., and Min, B.-C. (2025). Safeplan: Leveraging formal logic and chain-of-thought reasoning for enhanced safety in llm-based robotic task planning. arXiv preprint arXiv:2503.06892.

Wang, L., Ames, A., and Egerstedt, M. (2016). Safety barrier certificates for heterogeneous multi-robot systems. In 2016 American control conference (ACC), pages 5213–5218. IEEE.

Zhu, H., Samizadeh, T., and Sofia, R. C. (2025). A codeco case study and initial validation for edge orchestration of autonomous mobile robots. arXiv preprint arXiv:2511.08354.