Cela faisait un certain temps que je n’avais eu le plaisir de retourner au château de Dagstuhl. C’est aussi un retour à de vieilles problématiques sur les compétitions et évaluations empiriques en raisonneemnt automatique cette semaine.
En parallèle de ma thèse (c’était les années 2000), je m’étais en effet interessé à cette problématique loin d’être anecdotique : une belle table de résultats expérimentaux peut changer du tout au tout l’acceptation d’un article scientifique.
Lors de ma thèse, je m’étais rendu compte que certains articles travaillaient sur des sous ensembles de problèmes, sur des métriques différentes, ce qui rendait à chaque fois l’évaluation objective des méthodes assez difficiles. J’avais alors créé SATEX, un site qui collectait les benchmarks et les solveurs et qui présentait de manière objective les résultats. Une sorte de Kaggle de SAT (mais très très rudimentaire).
Et puis, dès 2002, j’ai été pris dans le tourbillon des premières organisations de compétitions internationales de solveurs SAT. De grands moments scientifiques et humains !
Aujourd’hui, il reste quelques grands principes que l’on avait mis en place avec Daniel Leberre (et d’autres) sur les compétitions mais le paysage a beaucoup changé. Les problèmes demeurent pourtant : comment définir ce qui rend un problème intéressant à résoudre / à inclure dans des tables de résultats ? Comment rendre compte de la diversité des approches ? Comment lutter contre la complexification des algorithmes qui rend leur fonctionnement plus opaques à l’analyse ? Les solveurs SAT sont maintenant des objets d’une telle complexité qu’il devient très difficile de comprendre leur fonctionnement.
Cette semaine de workshop a montré combien les competitions sont un évènement important dans nos communautés scientifiques. Des efforts de fédérations entre compétitions sont probablement à faire. Des ponts entre les problèmes (admettant plusieurs formalisations / plusieurs solveurs) sont à construire entre les compétitions.
Avec toujours ce cadre incroyable de Dagstuhl et un plaisir fort de retrouver les acteurs de cette révolution silencieuse de l’IA.
Si vous ne connaissez pas Dagstuhl, sachez que c’est un lieu inégalé pour la recherche et le foisonnement d’idées. D’ailleurs, l’INRIA est l’un des principaux contributeurs de centre de Dagtuhl. Il est important de maintenir de tels centres !

Comme je le fais à chaque post sur Dagstuhl, jouez à “trouvez Charlie” dans les photos de mes participations passées à Dagstuhl
2022

2019

2017

2015

2014

2009
