作者位次 #2/3ACL 2026Poster· Natural Language Processing
F ormal S cience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean
Jordan Meadows · Lan Zhang · Andre Freitas
摘要
Formalising informal mathematical reasoning into formally verifiable code is a significant challenge for large language models. In scientific fields such as physics, domain-specific machinery ( e.g. Dirac notation, vector calculus) imposes additional formalisation challenges that modern LLMs and...