Resumen:Formalizar el razonamiento matemático informal en código formalmente verificable es un desafío importante para los modelos de lenguaje grandes. En campos científicos como la física, la maquinaria de dominio específico (textit{por ejemplo} notación de Dirac, cálculo vectorial) impone desafíos de formalización adicionales que los LLM modernos y los enfoques agentes aún tienen que abordar. Para ayudar a la autoformalización en los ámbitos científicos, presentamos FormalScience; una canalización agente humana independiente del dominio que permite a un único experto en un dominio (sin experiencia profunda en lenguaje formal) producir pruebas formales textit{sintácticamente correctas} y textit{semánticamente alineadas} de razonamiento informal a bajo costo económico. Aplicando FormalScience a la física, construimos FormalPhysics, un conjunto de datos de 200 problemas y soluciones de física de nivel universitario (LaTeX) (principalmente mecánica cuántica y electromagnetismo), junto con sus representaciones formales Lean4. En comparación con los puntos de referencia matemáticos formales existentes, FormalPhysics logra una validez formal perfecta y muestra una mayor complejidad de las declaraciones. Evaluamos modelos de código abierto y sistemas propietarios en una tarea de autoformalización de declaraciones en nuestro conjunto de datos mediante indicaciones de disparo cero, autorefinamiento con retroalimentación de errores y un novedoso enfoque agente de múltiples etapas, y exploramos las limitaciones de la autoformalización en los enfoques modernos basados en LLM. Proporcionamos la primera caracterización sistemática de la deriva semántica en la autoformalización de la física en términos de conceptos como el colapso de la notación y la elevación de la abstracción, que revela lo que el lenguaje formal verifica cuando la preservación semántica completa es inalcanzable. Lanzamos el código base junto con un sistema FormalScience interactivo basado en UI que facilita la autoformalización y la demostración de teoremas en dominios científicos más allá. esta URL http//github.com/jmeadows17/formal-science
Publicado originalmente en export.arxiv.org el 27 de abril de 2026.
Ver fuente original
