Este artículo presenta un método para automatizar la calificación de exámenes de física mediante la combinación de un sistema de álgebra computacional, un solucionador de SMT y un sistema de reescritura de términos. Se utiliza un modelo de lenguaje a gran escala (LLM) para eliminar errores en las respuestas de los estudiantes y reescribirlas en un formato legible por máquina. La precisión de estas respuestas se evalúa mediante técnicas automatizadas de demostración de teoremas (resolución de SMT y un sistema de reescritura de términos adaptado a problemas de física). El sistema se evalúa utilizando más de 1500 respuestas reales de estudiantes de la Olimpiada Australiana de Física de 2023. En particular, se proporciona una descripción detallada del desarrollo del sistema de reescritura de términos y el establecimiento de sus propiedades de finalidad y confluencia.
