Autoformalization of Game Descriptions using Large Language Models
This addresses the problem of bridging natural language and formal reasoning in game theory for researchers and practitioners, though it is incremental as it builds on existing LLM and solver techniques.
The paper tackles the challenge of applying formal reasoning tools to game-theoretic scenarios expressed in natural language by introducing an autoformalization framework that translates descriptions into formal logic representations, achieving 98% syntactic and 88% semantic correctness using GPT-4o.
Game theory is a powerful framework for reasoning about strategic interactions, with applications in domains ranging from day-to-day life to international politics. However, applying formal reasoning tools in such contexts is challenging, as these scenarios are often expressed in natural language. To address this, we introduce a framework for the autoformalization of game-theoretic scenarios, which translates natural language descriptions into formal logic representations suitable for formal solvers. Our approach utilizes one-shot prompting and a solver that provides feedback on syntactic correctness to allow LLMs to refine the code. We evaluate the framework using GPT-4o and a dataset of natural language problem descriptions, achieving 98% syntactic correctness and 88% semantic correctness. These results show the potential of LLMs to bridge the gap between real-life strategic interactions and formal reasoning.