用大模型自动把物理运动问题转为形式化逻辑，成功率70%。
Can Large Language Models Autoformalize Kinematics?
- 给大模型输入自然语言描述，生成微分博弈逻辑公式
- 70%的问题能正确生成可验证的形式模型
- 适合想用大模型做系统形式化验证的开发者
自主式信息物理系统（如机器人和自动驾驶汽车）若能使用形式方法可靠地推理其控制决策，将获益良多。然而，在解决问题前需先准确表述问题，这要求构建系统的正式物理模型，传统上需人类专家完成，成为瓶颈。本文实验研究大语言模型（LLMs）是否可自动化这一过程。设计了一个包含20个本科物理运动问题的基准测试集，每个问题中，模型需根据自然语言描述生成微分博弈逻辑（dGL）形式模型。模型通过语法检查并基于解析器反馈迭代修正，再通过符号执行dGL公式来验证其语义正确性，即能否恢复原物理问题的解。最终在5次采样中取得70%的成功率。分析失败案例，指明未来改进方向。本工作为从自然语言到带连续动态的混合博弈逻辑的模型自形式化提供了首个定量基准。
原文摘要 · Abstract (English)
Autonomous cyber-physical systems like robots and self-driving cars could greatly benefit from using formal methods to reason reliably about their control decisions. However, before a problem can be solved it needs to be stated. This requires writing a formal physics model of the cyber-physical system, which is a complex task that traditionally requires human expertise and becomes a bottleneck. This paper experimentally studies whether Large Language Models (LLMs) can automate the formalization process. A 20 problem benchmark suite is designed drawing from undergraduate level physics kinematics problems. In each problem, the LLM is provided with a natural language description of the objects' motion and must produce a model in differential game logic (dGL). The model is (1) syntax checked and iteratively refined based on parser feedback, and (2) semantically evaluated by checking whether symbolically executing the dGL formula recovers the solution to the original physics problem. A success rate of 70% (best over 5 samples) is achieved. We analyze failing cases, identifying directions for future improvement. This provides a first quantitative baseline for LLM-based autoformalization from natural language to a hybrid games logic with continuous dynamics.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。