Curriculum d'apprentissage en mathématiques formelles

Nous explorons l'usage de l'itération d'expert dans le contexte de la modélisation linguistique appliquée aux mathématiques formelles. Nous démontrons qu'avec un budget de calcul identique, l'itération d'expert — entendue comme une recherche de preuves entrelacée avec l'apprentissage — surpasse de façon significative une recherche de preuves seule. Nous observons également que, lorsqu'elle est appliquée à une collection de propositions formelles présentant une variété suffisante de niveaux de difficulté, l'itération d'expert parvient à identifier et à résoudre un curriculum de problèmes de difficulté croissante, sans nécessiter de preuves correctes associées. Enfin, en appliquant cette méthode à un ensemble de problèmes soigneusement sélectionnés manuellement, nous atteignons un état de l'art sur le benchmark miniF2F, en résolvant automatiquement plusieurs problèmes complexes issus des olympiades scolaires.