# A Neuro-Symbolic Approach to Strategy Synthesis for Strategic Logics

arXiv: https://arxiv.org/abs/2606.17962 · HTML: https://mlsanity.com/paper/2606.17962/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 18 of its 51 references that are in the map.
- First posted on arXiv 16 Jun 2026.

## Builds on (most cited first, 18 of 18)

- [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022)
- [Reflexion: Language Agents with Verbal Reinforcement Learning](https://mlsanity.com/paper/2303.11366/) (2023)
- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (2021)
- [Competition-Level Code Generation with AlphaCode](https://mlsanity.com/paper/2203.07814/) (2022)
- [Large Language Models as Optimizers](https://mlsanity.com/paper/2309.03409/) (2023)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [Logical Reasoning in Large Language Models: A Survey](https://mlsanity.com/paper/2502.09100/) (2025)
- [LLMs as Planning Formalizers: A Survey for Leveraging Large Language Models to Construct Automated Planning Models](https://mlsanity.com/paper/2503.18971/) (2025)
- [Neuro-Symbolic Data Generation for Math Reasoning](https://mlsanity.com/paper/2412.04857/) (2024)
- [Decidability results for ATL* with imperfect information and perfect recall](https://mlsanity.com/paper/1805.12582/) (2018)
- [Natural Strategic Abilities in Voting Protocols](https://mlsanity.com/paper/2007.12424/) (2020)
- [MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications](https://mlsanity.com/paper/1402.2948/) (2014)
- [Reasoning about Human-Friendly Strategies in Repeated Keyword Auctions](https://mlsanity.com/paper/2201.09616/) (2022)
- [Multi-Valued Verification of Strategic Ability](https://mlsanity.com/paper/2310.20344/) (2023)
- [STV+Reductions: Towards Practical Verification of Strategic Ability Using Model Reductions](https://mlsanity.com/paper/2310.18418/) (2023)
- [Natural Strategic Ability in Stochastic Multi-Agent Systems](https://mlsanity.com/paper/2401.12170/) (2024)
- [A Model Checker for Natural Strategic Ability](https://mlsanity.com/paper/2410.14374/) (2024)
- [When Natural Strategies Meet Fuzziness and Resource-Bounded Actions (Extended Version)](https://mlsanity.com/paper/2512.20457/) (2025)

## Abstract (arXiv)

Reasoning about what agents can achieve through strategic interaction is a core challenge in Multi-Agent Systems (MAS). Logics for strategic ability, such as ATL, provide rigorous methods, but their adoption is often hindered by the computational cost of strategy synthesis. We introduce a neuro-symbolic framework that integrates large language models (LLMs) into the model-checking pipeline for MAS. 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. We instantiate the framework for bounded strategic reasoning in NatATL and introduce the first NatATL strategy-synthesis dataset, consisting of 4211 instances. Experiments with an open-weight Qwen3-32B model show that our certified pipeline achieves 92% accuracy on strategy-synthesis outcomes.