Can I verify my multi-agent RL system?
Turn-based Multi-Agent Reinforcement Learning Model Checking
This paper proposes a new method for verifying that turn-based multi-agent reinforcement learning (TMARL) agents behave as expected within complex, stochastic game environments. It combines TMARL with a formal verification technique called model checking, which uses mathematical models to rigorously prove system correctness against specified properties (expressed in Probabilistic Computation Tree Logic - PCTL).
Key points for LLM-based multi-agent systems: This method can verify complex behaviors beyond simple reward maximization, offering a way to ensure LLMs in multi-agent settings adhere to specific interaction protocols or avoid undesired outcomes. The "joint policy wrapper" concept is relevant, as it provides a way to model the combined behavior of multiple LLM agents interacting in a turn-based fashion, even if they have different internal architectures or training processes. The scalability analysis provides insights into the practical limitations of applying formal verification to increasingly complex multi-agent LLM systems.