Neuro-symbolic framework uses LLMs for 92% accurate strategy synthesis

Reasoning about strategic interactions in multi-agent systems (MAS) is computationally expensive, with traditional strategy synthesis methods often struggling to scale. In a new paper on arXiv, researchers Marco Aruta, Vadim Malvone, Aniello Murano, Domenico Parente, and Luca Rizzuti propose a neuro-symbolic framework that integrates large language models (LLMs) into the model-checking pipeline. The LLM acts as a strategy-generation oracle, proposing candidate strategies that are then formally validated by a standard MAS model checker. This generate-and-certify architecture uses LLM guidance to navigate large combinatorial strategy spaces while preserving formal soundness: generated strategies are accepted only when certified by the verifier.

The framework was instantiated for bounded strategic reasoning in NatATL (a strategic logic for multi-agent systems) and comes with the first NatATL strategy-synthesis dataset, consisting of 4,211 instances. Experiments with an open-weight Qwen3-32B model show that the certified pipeline achieves 92% accuracy on strategy-synthesis outcomes. This work demonstrates a practical compromise between the speed of neural models and the reliability of formal verification, opening new pathways for trustworthy AI in autonomous systems, game theory, and multi-agent coordination.