Évaluer les connaissances dans les cours de raisonnement automatisé

Cet article parle d'une méthode pour tester les connaissances des étudiants dans un cours qui se concentre sur le Raisonnement Automatisé. Le principal outil utilisé est l'assistant de preuve Isabelle, qui aide les étudiants à apprendre à travailler avec des Preuves Formelles en logique. L'objectif du cours est d'améliorer la compréhension des preuves formelles par les étudiants, en particulier avec Isabelle.

#Aperçu du cours

À l'Université technique du Danemark, un cours de niveau Master sur le raisonnement automatisé est proposé. Ce cours est optionnel et vaut 5 ECTS. Il apprend aux étudiants le théorème prouvant automatiquement et de manière interactive, avec Isabelle comme élément central du processus d'enseignement. Le cours aide progressivement les étudiants à apprendre à prouver des théorèmes et à comprendre la logique derrière eux.

#Objectifs d'apprentissage

Les étudiants doivent atteindre plusieurs objectifs d'apprentissage pendant le cours :

1. Expliquer les concepts de base présentés dans le cours.
2. Exprimer formellement des théorèmes mathématiques et des propriétés des systèmes informatiques.
3. Utiliser des systèmes de preuve par déduction naturelle.
4. Relier la logique du premier ordre, la logique d'ordre supérieur et la théorie des types.
5. Construire des preuves formelles dans des styles procéduraux et déclaratifs.
6. Utiliser des systèmes informatiques pour le raisonnement automatisé.
7. Évaluer la fiabilité des assistants de preuves et des outils associés.
8. Communiquer clairement et précisément les solutions aux problèmes.

Avant de commencer le cours, il est conseillé aux étudiants d'avoir un certain bagage en logique et en programmation fonctionnelle. Des cours précédents en informatique et en ingénierie fournissent ce savoir de base. Cependant, comme les prérequis ne sont que recommandés, pas obligatoires, certains étudiants peuvent ne pas être totalement familiers avec tous les sujets nécessaires.

#Évaluation de l'apprentissage des étudiants

Tout au long du cours, les étudiants doivent réaliser des devoirs et passer un examen final. Six devoirs sont donnés pendant le cours pour aider à évaluer leur compréhension, et ceux-ci contribuent à leur note globale. De plus, un examen écrit de deux heures a lieu à la fin du cours. Cet examen teste les étudiants sur leurs connaissances en logique et leur capacité à prouver des théorèmes en utilisant Isabelle.

#Structure de l'examen

L'examen comprend une variété de problèmes conçus pour évaluer différents aspects des connaissances des étudiants. Chaque problème se compose de deux questions, et les sujets incluent :

1. Prouver des théorèmes dans Isabelle sans automatisation.
2. Vérifier des programmes fonctionnels simples dans Isabelle/HOL.
3. Utiliser des preuves par déduction naturelle.
4. Appliquer des preuves par calcul des séquences.
5. Écrire des preuves générales dans Isabelle/HOL avec le langage Isar.

Les étudiants peuvent résoudre les problèmes dans n'importe quel ordre, ce qui leur permet de commencer par des questions plus faciles pour prendre confiance avant d'attaquer les plus difficiles.

#Conception de problèmes et exemples

#Preuves Isabelle sans automatisation

Le premier problème teste la compréhension des étudiants en logique d'ordre supérieur. Les étudiants doivent prouver la validité de déclarations logiques simples directement en utilisant Isabelle. Pour s'assurer que les étudiants n'utilisent pas d'outils automatisés comme Sledgehammer, une version de la logique d'ordre supérieur sans automatisation est fournie.

#Vérification de programmes fonctionnels

Le deuxième problème évalue les compétences de programmation et de preuve des étudiants dans Isabelle/HOL. Les étudiants reçoivent des programmes simples à mettre en œuvre et doivent prouver des propriétés sur ces programmes. Cette tâche vise à vérifier leur capacité à exprimer des concepts formellement, même sous pression d'examen.

#Déduction naturelle et calcul des séquences

Les deux problèmes suivants impliquent des systèmes de déduction naturelle et de calcul des séquences. Ces systèmes simplifient le processus de preuve et aident les étudiants à comprendre la logique classique du premier ordre. Les étudiants utilisent des outils externes conçus pour traduire leurs preuves en Isabelle, ce qui facilite l'accomplissement de cette tâche.

#Preuves générales dans Isabelle/HOL avec Isar

Le dernier problème teste la capacité des étudiants à construire des preuves structurées en utilisant le langage Isar. Ici, les étudiants reçoivent une preuve partiellement complétée avec des erreurs qu'ils doivent corriger pour la terminer. Ce format vise à aider les étudiants à prouver des propriétés complexes sans qu'ils aient à trouver la preuve de zéro.

#Mise en œuvre de l'examen et expérience des étudiants

Le format de l'examen a bien fonctionné pour le cours, qui comptait 41 étudiants inscrits. Parmi eux, 36 ont réussi, montrant que l'examen a effectivement testé les résultats d'apprentissage des étudiants. L'examen permet l'utilisation de toutes les aides, y compris l'accès à Internet, tout en maintenant une supervision stricte.

#Processus de notation

Un des avantages d'utiliser Isabelle pour l'examen est qu'une grande partie de la notation peut être faite automatiquement. Isabelle vérifie la justesse des preuves des étudiants, nécessitant seulement quelques vérifications manuelles pour s'assurer que les étudiants n'ont pas altéré incorrectement les définitions. Cette automatisation simplifie le processus de notation, en particulier pour les classes plus nombreuses.

#Défis et observations

Bien que la notation soit en grande partie automatisée, certains défis demeurent. Les étudiants peuvent mal comprendre les devoirs et soumettre des preuves ou des définitions incorrectes. Il n'est pas rare qu'il y ait des variations de qualité, surtout si les étudiants font face à des contraintes de temps pendant l'examen. Cependant, la corrélation globale entre la performance aux devoirs et les résultats de l'examen a été positive.

#Retours des étudiants

Après l'examen, les étudiants ont soumis des évaluations sur leur expérience. La plupart des étudiants ont estimé que l'examen correspondait au contenu du cours et aux objectifs d'apprentissage, mais certains ont exprimé des confusions sur certaines méthodes de preuve. D'autres ont suggéré qu'il serait bien d'inclure plus de problèmes de difficulté moyenne dans les examens futurs.

#Directions futures pour l'amélioration

L'équipe du cours reconnaît la nécessité d'améliorer continuellement le format de l'examen et la conception des problèmes. Un domaine de focus est d'ajuster la difficulté des questions pour s'assurer qu'elles soient appropriées sans être trop difficiles.

#Directives pour la conception des problèmes

Développer des directives claires pour la création de problèmes d'examen est essentiel. Cela implique de comprendre comment différents étudiants perçoivent la difficulté et d'examiner les erreurs courantes commises lors de la résolution de problèmes. Des recherches supplémentaires peuvent être nécessaires pour affiner ces directives.

#Alternatives aux examens écrits

Une autre direction potentielle est d'explorer des alternatives aux examens écrits traditionnels. Des options comme les évaluations par projet ou les examens oraux pourraient fournir des perspectives différentes sur la compréhension des étudiants, bien qu'elles présentent leurs propres défis, surtout à mesure que la taille des classes augmente.

#Conclusion

L'utilisation de l'assistant de preuve Isabelle pour enseigner le raisonnement automatisé s'est avérée efficace à l'Université technique du Danemark. Le format de l'examen permet une évaluation complète tout en tirant parti des capacités d'Isabelle pour la notation. Les retours continus des étudiants et les pratiques réflexives aideront à améliorer le cours dans de futures itérations, garantissant que les étudiants soient bien préparés à s'engager avec la logique formelle et les compétences en raisonnement automatisé.