Cet article présente une méthode d'automatisation de la notation des examens de physique combinant un système de calcul formel, un solveur SMT et un système de réécriture de termes. Un modèle de langage à grande échelle (LLM) est utilisé pour supprimer les erreurs des réponses des étudiants et les réécrire dans un format lisible par machine. L'exactitude de ces réponses est ensuite évaluée à l'aide de techniques automatisées de démonstration de théorèmes (résolution SMT et système de réécriture de termes adapté aux problèmes de physique). Le système est évalué à l'aide de plus de 1 500 réponses réelles d'étudiants de l'Olympiade australienne de physique de 2023. Une description détaillée du développement du système de réécriture de termes et de la détermination de ses propriétés de finalité et de confluence est notamment fournie.
