Artifact for Can Large Language Models Autoformalize Kinematics?

<p dir="ltr">This is the artifact provides the code to run the experiments for the paper:</p><p dir="ltr">Can Large Language Models Autoformalize Kinematics?. Aditi Kabra, Jonathan Laurent, Sagar Bharadwaj, Ruben Martins, Stefan Mitsch and André Platzer. FMCAD 2025.<br><br>Autonomous hybrid 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 hybrid system, which is a complex task that traditionally requires human expertise and becomes a bottleneck.</p><p><br></p><p dir="ltr">This artifact experimentally studies whether Large Language Models (LLMs) can automate the formalization process of hybrid systems via a 20 problem benchmark suite 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. This provides a quantitative baseline for LLM-based autoformalization from natural language to a hybrid games logic with continuous dynamics.</p>