Resumen: Presentamos LeanTutor, un sistema de tutoría basado en un modelo de lenguaje grande (LLM) para pruebas de matemáticas. Leandutor interactúa con el estudiante en lenguaje natural, verifica formalmente las pruebas matemáticas escritas por el estudiante en Lean, genera los próximos pasos correctos y proporciona la orientación de instrucción apropiada. LeanTutor está compuesto por tres módulos: (i) un autoformalizador/comprobante de prueba, (ii) un generador de siguiente paso y (iii) un generador de retroalimentación del lenguaje natural. El primer módulo se autoformaliza fielmente las pruebas de los estudiantes en Lean y verifica la precisión de prueba a través de la compilación de código exitosa. Si la prueba tiene un error, se identifica el paso incorrecto. El módulo de generador del siguiente paso genera una táctica lean válida para pruebas incorrectas a través de la generación de candidatos basada en LLM y la búsqueda de pruebas. El módulo del generador de retroalimentación aprovecha los datos Lean para producir una pista de lenguaje natural motivado pedagógicamente para el usuario estudiantil. Para evaluar nuestro sistema, presentamos Peanobench, un conjunto de datos escrito por humanos derivado del juego de números naturales, que consta de 371 pruebas aritméticas de maní, donde cada paso de prueba del lenguaje natural se combina con la táctica lógicamente equivalente correspondiente en Lean. El autoformalizador formaliza correctamente el 57% de las tácticas en las pruebas correctas e identifica con precisión el paso incorrecto en el 30% de las pruebas incorrectas. Al generar sugerencias de lenguaje natural para pruebas erróneas, Leantutor supera a una línea de base simple sobre la precisión y las métricas de relevancia.
Publicado Originalme en rss.arxiv.org El 10 de junio de 2025.
Ver Fuente Original
