# Can Large Language Models Autoformalize Kinematics?

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 9 of its 29 references that are in the map.
- First posted on arXiv 26 Sep 2025.

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

- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [NL2TL: Transforming Natural Languages to Temporal Logics using Large Language Models](https://mlsanity.com/paper/2305.07766/) (2023)
- [LLMs for Mathematical Modeling: Towards Bridging the Gap between Natural and Mathematical Languages](https://mlsanity.com/paper/2405.13144/) (2024)
- [Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency](https://mlsanity.com/paper/2410.20936/) (2024)
- [Data-Efficient Learning of Natural Language to Linear Temporal Logic Translators for Robot Task Specification](https://mlsanity.com/paper/2303.08006/) (2023)
- [CESAR: Control Envelope Synthesis via Angelic Refinements](https://mlsanity.com/paper/2311.02833/) (2023)
- [Differential Game Logic](https://mlsanity.com/paper/1408.1980/) (2014)
- [Pegasus: Sound Continuous Invariant Generation](https://mlsanity.com/paper/2005.09348/) (2020)
- [Oracular Programming: A Modular Foundation for Building LLM-Enabled Software](https://mlsanity.com/paper/2502.05310/) (2025)

## Built on by (most cited first, 1 of 1)

- [Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiability](https://mlsanity.com/paper/2607.09366/) (2026)

## Abstract (arXiv)

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.