analiza aiqbench
This research addresses the limitations of LLMs in handling complex constraint satisfaction problems by integrating them with symbolic solvers like Z3 through a reinforcement learning framework. The approach combines synthetic data generation and tool-aware rewards to enhance verifiable reasoning capabilities across both in-domain and out-of-domain logic tasks. This work represents a significant step toward bridging the gap between flexible natural language understanding and rigorous formal verification.
SAT-RL: Training Language Models for Logical Reasoning with Symbolic Solvers
arXiv:2610.14402v1 Announce Type: new Abstract: Large language models (LLMs) have achieved strong performance in mathematical and logical reasoning, yet they still suffer from the curse of complexity and struggle as problem difficulty increases with the number of constraint interactions and the size of the search space. In contrast, satisfiability solvers such as Z3 provide scalable and verifiable reasoning through constraint solving under formal theories, but lack the flexibility to interpret natural-language problem descriptions. In this work, we propose SAT-RL, a reinforcement-learning (RL) framework that trains LLMs to interact with symbolic solvers through multi-turn tool execution. SAT-RL leverages synthetic data generation with verifiable solutions, supervised warm-up on solver-augmented traces, and solver-grounded reinforcement learning with tool-aware rewards. Experiments show that SAT-RL substantially improves symbolic reasoning with tools on both in-domain and out-of-domain logic tasks. Our code is available on https://github.com/sunjia72/SAT-RL.
Abstract:Large language models (LLMs) have achieved strong performance in mathematical and logical reasoning, yet they still suffer from the curse of complexity and struggle as problem difficulty increases with the number of constraint interactions and the size of the search space. In contrast, satisfiability solvers such as Z3 provide scalable and verifiable reasoning through constraint solving under formal theories, but lack the flexibility to interpret natural-language problem descriptions. In this work, we propose SAT-RL, a reinforcement-learning (RL) framework that trains LLMs to interact with symbolic solvers through multi-turn tool execution. SAT-RL leverages synthetic data generation with verifiable solutions, supervised warm-up on solver-augmented traces, and solver-grounded reinforcement learning with tool-aware rewards. Experiments show that SAT-RL substantially improves symbolic reasoning with tools on both in-domain and out-of-domain logic tasks. Our code is available on this https URL.
Artificial Intelligence (cs.AI); Symbolic Computation (cs.SC)
arXiv:2610.14402 [cs.AI]
(or arXiv:2610.14402v1 [cs.AI] for this version)
https://doi.org/10.48550/arXiv.2610.14402 Focus to learn more arXiv-issued DOI via DataCite (pending registration)
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.
Text integral sub licența deschisă a publicației · 232 cuvinte
Subiecte conexe
Frontier Risk Report (February to March 2026)
METR · 19 mai 2026
Informe de riesgos de la IA de frontera (febrero–marzo de 2026)
METR · 19 mai 2026
Frontier AI Risk Report (February–March 2026)
METR · 19 mai 2026
Lessons From the Leaderboard: What 5,000+ Kagglers Taught Us About Improving AI Reasoning
NVIDIA · 14 iul. 2026