Resumen: Los Proversos del teorema interactivo (PTI) requieren formalización manual, que es intensiva en mano de obra y exige conocimiento experto. Si bien la formalización automatizada ofrece una solución potencial, enfrenta dos desafíos principales: alucinación modelo (por ejemplo, predicados indefinidos, mal uso de símbolos e incompatibilidad de la versión) y la brecha semántica causada por premisas ambiguas o faltantes en las descripciones del lenguaje natural. Para abordar estos temas, proponemos CRAMF, un marco de formalización matemática impulsada por la recuperación de la recuperación. CRAMF mejora la autoformalización basada en LLM al recuperar las definiciones formales de conceptos matemáticos centrales, proporcionando fundamento contextual durante la generación de código. Sin embargo, la aplicación de la generación de recuperación aumentada (RAG) en este entorno no es trivial debido a la falta de bases de conocimiento estructuradas, la naturaleza polimórfica de los conceptos matemáticos y la alta precisión requerida en la recuperación formal. Introducimos un marco para construir automáticamente una base de conocimiento de definición de concepto de Mathlib4, la biblioteca matemática estándar para el Lean 4 Theorem Prover, indexando más de 26,000 definiciones formales y más de 1,000 conceptos matemáticos centrales. Para abordar el polimorfismo conceptual, proponemos el aumento de consultas contextuales con señales de nivel de dominio y aplicación. Además, diseñamos una estrategia de recuperación híbrida de doble canal con Reranking para garantizar una recuperación de definición precisa y relevante. Los experimentos en Minif2F, ProGNNet y nuestro recién propuesto de referencia AdvancedMath muestran que CRAMF puede integrarse sin problemas en las autoformalizantes basadas en LLM, produciendo mejoras consistentes en la precisión de la traducción, alcanzando hasta 62.1% y un promedio de 29.9% de mejora relativa.
Publicado Originalme en export.arxiv.org El 11 de agosto de 2025.
Ver Fuente Original
