Bonjour,
Des erreurs à corriger rapidement svp, en fin de mail.
Priorités aux articles à partir de 2012.
Merci d'avance,
Bonne journée,
Théo
* il manque le champ "lrdeteam" dans ces entrées :
[cid:a5d1f0e8-b81f-4064-9104-dcf92ed72efb]
* il manque le champ "month" dans ces entrées :
[cid:4971bfb5-148c-4915-98c8-011b53c63207]
* ces entrées n'ont pas de type précis (article, inproceedings, etc.) :
[cid:2e657714-4b02-467a-afc4-8f59ec0d8995]
* ces entrées n'ont pas d'entrée "lrderank" :
[cid:9cbd010c-85c2-452e-bb45-600fdadd8925]
______________________
Perms mailing list -- perms(a)ml.lre.epita.fr
https://lists.lrde.epita.fr/postorius/lists/perms.ml.lre.epita.fr//
________________________________
De : akheireddine <akheireddine(a)lrde.epita.fr>
Envoyé : mercredi 6 décembre 2023 10:45
À : Annonces du LRDE <annonce(a)lrde.epita.fr>
Objet : [Lrde] [Lrde Annonce] Soutenance de thèse de Anissa Kheireddine
Bonjour,
J'ai le plaisir de vous inviter à la soutenance de ma thèse intitulée :
"Contributions au Bounded model-checking basé sur SAT
La soutenance sera présentée en français.
Elle aura lieu le mardi 19 décembre 2023 à partir de 10h00 (heure de
Paris),
en Amphi 401, EPITA, 14-16 Rue Voltaire, 94270 Le Kremlin-Bicêtre.
Vous êtes cordialement invité au pot qui suivra.
Composition du jury:
Rapporteur: Vijay Ganesh, Professeur, GT, Georgia Institute of
Technology.
Rapporteur: Ahmed Bounekkar, Maître de Conférences, ERIC,
Université Claude Bernard Lyon 1.
Examinatrice: Laure Petrucci, Professeure, LIPN, Université Sorbonne
Paris Nord.
Examinatrice: Emmannuelle Encrenaz, Professeure, LIP6, Sorbonne
Université.
Directeur: Souheib Baarir, Enseignant-Chercheur, LRE, EPITA.
Encadrant: Étienne Renault, SiPearl.
Résumé :
Les systèmes informatiques sont devenus omniprésents dans notre vie
quotidienne. Garantir la fiabilité
et la robustesse de ces systèmes est une nécessité absolue. La
Vérification de Modèles (Model Checking)
est l'une des approches dédiées à cette fin. Son objectif est de prouver
l'absence de défaillances ou
d'identifier d'éventuelles erreurs.
Le model checking se décline en plusieurs techniques. Parmi celles-ci,
on trouve la Vérification de
Modèles Bornée (Bounded Model Checking - BMC), une technique qui repose
sur la satisfiabilité
booléenne (SAT). L'idée centrale derrière le BMC est de vérifier qu'un
modèle, limité à des exécutions
bornées par un entier k, satisfait sa spécification, définie comme un
ensemble d'expressions logiques
temporelles. Dans cette approche, les comportements du système sont
exprimés sous forme de problèmes SAT.
Contrairement à d'autres méthodes de vérification formelle, le BMC basé
sur SAT n'est généralement pas
sensible au problème de l'explosion de l'espace d'états, ce qui peut
poser problème lors de la conception
de systèmes impliquant des millions de variables et de contraintes.
Cependant, le compromis réside dans
la complexité temporelle, car les problèmes SAT sont connus pour être
NP-complets.
Au cours des dernières décennies, d'importantes avancées ont été
réalisées dans la résolution séquentielle
de problèmes SAT. Ces développements se sont principalement concentrés
sur l'utilisation d'informations
dynamiques, acquises lors du processus de résolution (par exemple,
l'apprentissage de clauses binaires) ou
d'informations statiques, extraites de la structure inhérente du
problème SAT (par exemple, la structure
en communauté). Toutefois, moins d'attention a été accordée aux
informations structurelles du problème
initial. Par exemple, lorsque qu'un problème BMC est réduit à une
formule booléenne, des données
cruciales sont perdues lors de la traduction. Comme le souligne cette
thèse, la réintégration de ces
informations perdues peut considérablement améliorer le processus de
résolution. Ce travail explore des
moyens d'améliorer la résolution de problèmes BMC basés sur SAT, tant
dans des contextes séquentiels que
parallèles, en exploitant et en valorisant les informations pertinentes
extraites des caractéristiques
inhérentes du problème. Cela peut impliquer l'amélioration
d'heuristiques génériques existantes ou la
décomposition efficace de la formule en partitions.
Cordialement,
Anissa Kheireddine
______________________
Annonce mailing list -- annonce(a)lrde.epita.fr
https://lists.lrde.epita.fr/postorius/lists/annonce.lrde.epita.fr//
______________________
Lrde mailing list -- lrde(a)lrde.epita.fr
https://lists.lrde.epita.fr/postorius/lists/lrde.lrde.epita.fr//
______________________
Current mailing list -- current(a)ml.lre.epita.fr
https://lists.lrde.epita.fr/postorius/lists/current.ml.lre.epita.fr//
______________________
Permanents mailing list -- permanents(a)ml.lre.epita.fr
https://lists.lrde.epita.fr/postorius/lists/permanents.ml.lre.epita.fr//
______________________
Perms mailing list -- perms(a)ml.lre.epita.fr
https://lists.lrde.epita.fr/postorius/lists/perms.ml.lre.epita.fr//
Bonjour aux « Parisien.ne.s »,
Théo m’a chargée de vous signaler que j’ai commandé des cartons
pour le futur déménagement (la date n’est pas encore connue).
Ils sont dans mon bureau. J’ai surtout commandé des cartons de
format « livre », mais aussi des formats « standard ».
Passez me voir rapidement pour vous en procurer, car tout le monde
doit se tenir prêt à bouger (quand on aura un go, il faudra être réactif).
Qui dit « déménagement », dit « faire le tri » :
Beaucoup de choses méritent d'aller à la poubelle ! C’est le moment de s’en
dessaisir, ainsi vous aurez besoin de moins de cartons ;-)
Attention toutefois, le matériel électronique obsolète sera jeté à part pour être
recyclé !
Merci et bonne journée,
Daniela
Bonjour,
Je vous annonce que le prochain séminaire de l'axe ML sera donné par Julien Perez, qui a rejoint le LRE et l'équipe IA début novembre.
Ci-dessous, le titre et l'abstract du talk
Merci de bien vouloir remplir le framadate suivant : https://framadate.org/ctE9bGR4XuGYzRoy
Au plus tard le vendredi 24 novembre, afin de fixer rapidement un créneau pour cet évènement.
Title: Safe Skill Discovery in Unsupervised Reinforcement Learning and Alignment in Code LLMs.
Abstract:
This presentation addresses the question of safety and alignment in statistical sequential decision models. The first part of the talk will focus on safety-centric skill discovery using unsupervised reinforcement learning and its application to robotic manipulation, as presented at ICRA'23. We introduce the novel problem of Safety-Aware Skill Discovery, which aims to learn, in a task-agnostic fashion, a repertoire of reusable skills that are inherently safe for composing solutions to downstream tasks. We present a computationally tractable algorithm that learns a latent-conditioned skill policy maximizing intrinsic rewards, regulated by a safety-critic capable of modeling any user-defined safety constraints. Utilizing the pretrained safe skill repertoire, hierarchical reinforcement learning can solve multiple downstream tasks without explicit consideration of safety during training and testing. We evaluate our algorithm on a collection of force-controlled robotic manipulation tasks in simulation, demonstrating promising performance in downstream tasks while satisfying safety constraints.
As an opening, in the second part of the talk, I will introduce the recent progress of Code LLM and the emerging alignment requirements. This section serves as a discussion, emphasizing the necessity of alignment in code-based Language Model Models (LLMs) and the imperative safety considerations inherent in this domain.
Bonne fin de journée,
[Une image contenant texte, clipart, signe Description générée automatiquement]
Idir Benouaret
Enseignant-Chercheur
[https://lh6.googleusercontent.com/dCYVl9pmYNgg1wBndkYtELRR9DX8RRY5d_e4N2Xhk…]
[https://lh4.googleusercontent.com/O8lm18dZZ188g_iBNOmO2UX8qPx8zNmCfFbItUDzk…]
[https://lh4.googleusercontent.com/iJejRKKnVTGA2lyz-eMOKQvI9vVP-ftzUIqzCoeoR…]
[https://lh6.googleusercontent.com/J3eMugeLIjhhZigE4aw44kR3o5SCCOf3J7YJfPDTC…]
[https://lh3.googleusercontent.com/2nPXgKhjFiG8S9uTa2TTXP1-CcUjZnjdJ5CVAd3_f…]
[Une image contenant texte, clipart Description générée automatiquement]
+33 4 28 29 37 63
[https://lh6.googleusercontent.com/hGLtorzP2LwpWN7a7qPxHUf-Ufq7UmoJXpduyzZWG…]
______________________
Current mailing list -- current(a)ml.lre.epita.fr
https://lists.lrde.epita.fr/postorius/lists/current.ml.lre.epita.fr//
______________________
Permanents mailing list -- permanents(a)ml.lre.epita.fr
https://lists.lrde.epita.fr/postorius/lists/permanents.ml.lre.epita.fr//
______________________
Perms mailing list -- perms(a)ml.lre.epita.fr
https://lists.lrde.epita.fr/postorius/lists/perms.ml.lre.epita.fr//
Bonjour,
Nous travaillons actuellement sur la rédaction d'un guide pour bien remplir le .bib et donc déclarer vos publications.
En attendant, petit rappel de 3 règles importantes :
* la clef de l'article est 1er_auteur.année.acronyme_conf_journal et ce même si le 1er auteur n'est pas du labo
* quand vous soumettez vos changement, si la pipeline casse (ça devient rouge), merci de corriger ou d'envoyer un mail pour demander de l'aide, mais pas de partir en laissant en l'état
* une moulinette automatique crée l'annonce sur le site web, merci de vérifier que tout est ok sur le site du LRE après le passage de cette moulinette
Bonne journée
Elodie
______________________
Current mailing list -- current(a)ml.lre.epita.fr
https://lists.lrde.epita.fr/postorius/lists/current.ml.lre.epita.fr//
______________________
Permanents mailing list -- permanents(a)ml.lre.epita.fr
https://lists.lrde.epita.fr/postorius/lists/permanents.ml.lre.epita.fr//
______________________
Perms mailing list -- perms(a)ml.lre.epita.fr
https://lists.lrde.epita.fr/postorius/lists/perms.ml.lre.epita.fr//