Notre cœur de métier est le développement de systèmes critiques, principalement pour le ferroviaire, l’industrie ou l’énergie.
Un système critique est un système pour lequel une défaillance peut avoir des conséquences graves en termes de vies humaines, d’impact financier ou environnemental.
Nous recherchons de nouveaux collaborateurs motivés par les challenges techniques et l’envie d’apprendre dans un environnement stimulant et innovant.
Notre croissance offre de réelles opportunités d’évolution dans une structure à taille humaine.
Votre mission
Systerel développe et commercialise la suite de vérification formelle Systerel Smart Solver (S3). Les outils de S3, basés sur le langage HLL (High Level Language), permettent de modéliser des systèmes critiques et d’effectuer des analyses de type SAT-based Model-Checking sur ces modèles. Leur utilisation principale est de prouver mathématiquement que le système analysé respecte un ensemble de propriétés de sécurité permettant de considérer que ce système ne contient pas de bug critique.
La stratégie de preuve repose sur l’induction. Pour effectuer une telle preuve, il est souvent nécessaire d’ajouter des propriétés intermédiaires, appelées lemmes, qui permettent de renforcer le pas d’induction. Le moteur d’analyse S3 peut alors prouver ces Lemmes de Renforcement de l’Induction (LRI) puis les utiliser pour prouver la propriété. La recherche des LRI est consommatrice en temps et nécessite une connaissance approfondie des outils S3 et du système analysé.
L’objectif de ce stage est de mettre à disposition des utilisateurs un pipeline IA qui les assiste dans le travail de recherche des LRI en proposant des lemmes candidats. Ces candidats seront évalués par la suite S3 pour trouver ceux qui sont vrais, inductifs et permettent de prouver la propriété.
Vous aurez pour missions de :
- Mettre en place un environnement de test de la recherche de LRI sur la base du corpus existant,
- Construire et améliorer un pipeline IA de recherche de LRI,
- Documenter l’ensemble des itérations et du travail réalisé.
Vous serez assisté par des experts en méthodes formelles et serez encadré par un ingénieur au fait des techniques d’AI générative.
Compétences et expériences demandées
Pour ce stage, vous êtes :
- Étudiant en dernière année d’école d’ingénieur ou à l’université avec une spécialisation en IA,
- Intéressé par les langages formels et la logique mathématique,
- À l’aise avec le langage Python et les librairies du type LangChain, LlamIndex,
- À l’aise avec les concepts et les techniques d’IA génératives (LLM, RAG, base de données vectorielle, LLM-as-a-Judge, …)
- Rigoureux, curieux, autonome et force de proposition.
Type de contrat, durée & avantages
Convention de stage – Durée : 6 mois
Chez Systerel, nous proposons à nos stagiaires sur Aix-en-Provence :
- Une rémunération brute totale pouvant atteindre 1 300€ (dont jusqu’à 300€ de participation aux frais de logement sous conditions et justificatifs),
- Jusqu’à 5 jours de congés,
- Des tickets restaurant,
- La prise en charge de 50% de l’abonnement transports en commun,
- La possibilité de faire du télétravail.
Vous souhaitez
- Participer à des projets innovants,
- Développer des compétences recherchées et en évolution permanente,
- Bénéficier d’un encadrement de qualité,
- Vous épanouir au sein d’une entreprise portant des valeurs d’excellence, de haute technicité et de vraies valeurs humaines.
Alors n’hésitez plus à nous faire parvenir votre candidature !
Lieu
Aix-en-Provence.
Référence de l’offre
STAGE_PDT_LEMMES_A
Des questions ?
Écrivez-nous à drh@systerel.fr
Systerel est engagée dans une politique en faveur de l’égalité hommes-femmes et de l’emploi des travailleurs en situation de handicap.