用大模型自动把游戏描述转成可求解的逻辑代码
Autoformalization of Game Descriptions using Large Language Models
- 用一次提示+求解器反馈让大模型自我修正逻辑代码
- 语法正确率达98%，语义正确率达88%
- 适合想用形式化方法分析现实博弈的人
博弈论是分析战略互动的强大框架，广泛应用于日常生活到国际政治。然而，将形式化推理工具应用于这些场景面临挑战，因为实际情境通常以自然语言描述。为此，我们提出一个博弈论场景的自动形式化框架，将自然语言描述转化为适合形式化求解器的逻辑表示。该方法采用单次提示（one-shot prompting）并结合求解器对语法正确性提供反馈，使大语言模型能够迭代优化生成的代码。我们在GPT-4o和自然语言问题描述数据集上进行评估，实现98%的语法正确率和88%的语义正确率。结果表明，大模型有望弥合真实战略互动与形式化推理之间的鸿沟。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。