Thèse en complexité de la preuve et compilation de connaissances (H/F)

Référence : UMR8188-FLOCAP-003

  • Fonction publique : Fonction publique de l'État
  • Employeur : Centre national de la recherche scientifique (CNRS)
  • Localisation : 62307 LENS (France)

Partager la page

Veuillez pour partager sur Facebook, Twitter et LinkedIn.

  • Nature de l’emploi Emploi ouvert uniquement aux contractuels
  • Nature du contrat Non renseigné
  • Expérience souhaitée Non renseigné
  • Rémunération Fourchette indicative pour les contractuels 2200€ brut par mois. € brut/an Fourchette indicative pour les fonctionnaires Non renseignée
  • Catégorie Catégorie A (cadre)
  • Management Non renseigné
  • Télétravail possible Non renseigné

Vos missions en quelques mots

Sujet de thèse :
L'objectif original de la complexité de la preuve est de prouver que P est différent de NP en montrant qu'il n'y a pas de preuves courtes pour coNP. À cette fin, des systèmes de preuves fortes pour différents problèmes, en particulier SAT ont été introduit dans le but de montrer qu'en général, il n'existe pas de preuves courtes et efficacement vérifiables pour le problème en question.

Une autre orientation, plus récente, de la complexité de la preuve provient de l'observation que de nombreux algorithmes génèrent implicitement des preuves de correction, souvent une forme de représentation de l'exécution de l'algorithme sur une instance. Ainsi, la compréhension des preuves générées permet de mieux comprendre l'algorithme considéré et ses limites. Cette approche est également utile pour vérifier l'exactitude des résultats des solveurs mettant en œuvre l'algorithme : l'écriture explicite de la preuve générée permet de vérifier l'exactitude avec un vérificateur de preuve indépendant qui, étant moins complexe qu'un solveur complet, est aujourd'hui souvent vérifié de manière formelle. Cela permet de vérifier l'exactitude des résultats générés par le solveur, ce qui permet de lui faire confiance dans les applications critiques. Cette approche est la plus développée dans la résolution SAT pour le système de preuve DRAT et ses variantes, mais il existe également des approches similaires pour les solveurs pseudo-booléens, QBF et le problème de comptage propositionnel #SAT (entre autres).

Ces dernières années, les structures de données utilisées en compilation de connaissances ont trouvé des applications dans le domain de la complexité de la preuve. Ce domaine étudie systématiquement différentes représentations des fonctions booléennes. Les plus importantes de ces représentations sont les circuits connus sous le nom de DNNF (decomposable negation normal form) et leurs différentes sous-classes. Ces sous-classes correspondent essentiellement à différents algorithmes de comptage. Cette observation a conduit à l'introduction de DNNF certifiées comme format de preuve pour #SAT.

L'idée de la thèse proposée est d'étudier plus largement la compilation de connaissances dans un contexte de complexité de la preuve. Quelques exemples de questions sont les suivants : quels systèmes de preuves pour #SAT peuvent être vus comme des preuves sous forme de DNNF ? Les séparations connues entre les différentes classes de DNNF peuvent-elles être étendues aux systèmes de preuves ? Quelles restrictions ou extensions naturelles des DNNF donnent des systèmes de preuves utiles ? Au-delà du comptage, quels autres problèmes se prêtent à une analyse à l'aide de techniques de compilation de connaissances ? On sait par exemple que les DNNF peuvent être utilisée dans des algorithmes pour QBF et MaxSAT. Cela donne-t-il une nouvelle perspective sur ces problèmes ? Cela conduit-il à des algorithmes utiles ?


Le travail
Voir plus sur le site emploi.cnrs.fr...

Profil recherché

Contraintes et risques :
Pas de risques particuliers.

Niveau d'études minimum requis

  • Niveau Niveau 7 Master/diplômes équivalents
  • Spécialisation Formations générales

Langues

  • Français Seuil

Qui sommes-nous ?

Le Centre national de la recherche scientifique est un organisme public de recherche pluridisciplinaire placé sous la tutelle du ministère de l’Enseignement supérieur, de la Recherche et de l’Innovation.

C’est l’une des plus importantes institutions publiques au monde : 33 000 femmes et hommes (dont plus de 16 000 chercheurs et plus de 16 000 ingénieurs et techniciens), en partenariat avec les universités et les grandes écoles, y font progresser les connaissances en explorant le vivant, la matière, l’Univers et le fonctionnement des sociétés humaines.

En savoir plus sur l'employeur

À propos de l'offre

  • Le Centre national de la recherche scientifique est l’une des plus importantes institutions publiques au monde : 34 000 femmes et hommes (plus de 1 000 laboratoires et 200 métiers), en partenariat avec les universités et les grandes écoles, y font progresser les connaissances en explorant le vivant, la matière, l’Univers et le fonctionnement des sociétés humaines. Depuis plus de 80 ans, y sont développées des recherches pluri et interdisciplinaires sur tout le territoire national, en Europe et à l’international. Le lien étroit que le CNRS tisse entre ses missions de recherche et le transfert vers la société fait de lui un acteur clé de l’innovation en France et dans le monde. Le partenariat qui le lie avec les entreprises est le socle de sa politique de valorisation et les start-ups issues de ses laboratoires (près de 100 chaque année) témoignent du potentiel économique de ses travaux de recherche.

  • Vacant
  • Chercheuse / Chercheur

Des offres d'emplois recommandées pour vous