Resumen: La autoformalización aborda la escasez de datos para la demostración automatizada de teoremas (ATP) al traducir problemas matemáticos del lenguaje natural a enunciados formales. Los esfuerzos en trabajos recientes pasan de impulsar directamente grandes modelos de lenguaje a entrenar un modelo formalizador de extremo a extremo desde cero, logrando avances notables. Sin embargo, el formalizador existente todavía tiene dificultades para generar consistentemente declaraciones válidas que cumplan con la validez sintáctica y la coherencia semántica. Para abordar este problema, proponemos el Autoformalizador con retroalimentación de herramientas (ATF), un enfoque novedoso que incorpora información sintáctica y de coherencia como herramientas en el proceso de formalización. Al integrar compiladores Lean 4 para correcciones de sintaxis y emplear un enfoque de múltiples LLM como jueces para la validación de la coherencia, el modelo puede refinar de forma adaptativa las declaraciones generadas de acuerdo con la retroalimentación de la herramienta, mejorando tanto la validez sintáctica como la coherencia semántica. La capacitación de ATF implica una fase de arranque en frío sobre datos de llamada de herramientas sintéticas, una fase de iteración de expertos para mejorar las capacidades de formalización y optimización de preferencias directas para aliviar revisiones ineficaces. Los resultados experimentales muestran que ATF supera notablemente a una variedad de modelos formalizadores de referencia, y su rendimiento superior está validado aún más por evaluaciones humanas. Un análisis posterior revela que el ATF demuestra excelentes propiedades de escala de inferencia. Además, abrimos Numina-ATF, un conjunto de datos que contiene 750.000 declaraciones formales sintéticas para facilitar los avances en la autoformalización y la investigación de ATP.
Publicado originalmente en export.arxiv.org el 8 de octubre de 2025.
Ver fuente original
