Resumen: La autoformalización de pruebas, la tarea de traducir teoremas y pruebas del lenguaje natural a código verificable por máquina, es un paso crítico para integrar grandes modelos de lenguaje en flujos de trabajo matemáticos rigurosos. Los enfoques actuales se centran en producir código ejecutable, pero con frecuencia no logran preservar el significado semántico y la estructura lógica del argumento original escrito por humanos. Para abordar esto, presentamos ProofFlow, un canal novedoso que trata la fidelidad estructural como un objetivo principal. ProofFlow primero construye un gráfico acíclico dirigido (DAG) para mapear las dependencias lógicas entre los pasos de prueba. Luego, emplea un enfoque novedoso basado en lemas para formalizar sistemáticamente cada paso como un lema intermedio, preservando la estructura lógica del argumento original. Para facilitar la evaluación, presentamos un nuevo punto de referencia de 184 problemas de nivel universitario, anotados manualmente con soluciones paso a paso y gráficos de dependencia lógica, e introducimos ProofScore, una nueva métrica compuesta para evaluar la corrección sintáctica, la fidelidad semántica y la fidelidad estructural. Los resultados experimentales muestran que nuestro canal establece un nuevo estado del arte para la autoformalización, logrando un ProofScore de 0,545, superando sustancialmente las líneas de base como la formalización de prueba completa (0,123), que procesa toda la prueba a la vez, y la formalización de prueba por pasos (0,072), que maneja cada paso de forma independiente. Nuestro proceso, punto de referencia y métrica de puntuación son de código abierto para fomentar un mayor progreso en esta URL https.
Publicado originalmente en export.arxiv.org el 20 de octubre de 2025.
Ver fuente original
