DEVELOPPEMENT MACHINE LEARNING POUR LA PREUVE MATHEMATIQUE DE LOGICIEL

Objectif du stage : Développement en Machine Learning pour la preuve mathématique de logiciel

CLEARSY est une PME Française fondée en 2001 par les ingénieurs auteurs de l’industrialisation de l’outil de modélisation formelle appelé Atelier B, utilisé pour spécifier, concevoir, valider les systèmes et réaliser les logiciels critiques (comme le pilote automatique du métro de la ligne 14 à Paris).
L’activité est majoritairement orientée vers le secteur ferroviaire, énergie (nucléaire) et défense.

Société à taille humaine sur 4 sites en France, en pleine croissance (150 personnes), nous développons et déployons nos systèmes dans le monde entier depuis plus de 10 ans, nous avons notamment pu travailler à Sao Paolo / Stockholm / Caracas / New York / Hiroshima / Honolulu…)

Les équipes CLEARSY interviennent dans toutes les phases d’un projet, de la spécification à la réalisation de systèmes « clé en main » tout en garantissant un respect le plus strict des exigences de sûreté.
Clearsy recherche aujourd’hui des ingénieurs passionnés par le challenge technique et qui ont appris à apprendre pour venir renforcer ces équipes techniques.

Cette citation reflète bien nos valeurs : Steve Jobs – Cela n’a pas de sens d’embaucher des gens intelligents et de leur dire quoi faire ; nous embauchons des gens intelligents pour qu’ils nous disent ce qu’il faut faire

La suite logicielle Atelier B (https://www.atelierb.eu/) permet le développement de logiciels sûrs grâce à la modélisation formelle (langage B, https://www.atelierb.eu/methode-formelle/) de logiciels et de leur preuve mathématique. Cette preuve s’appuie sur des outils spécifiques (theorem prover, model checker) qui doivent permettre de démontrer qu’une formule logique est vraie sous certaines hypothèses. Ces formules logiques, appelées obligations de preuve (ou PO), sont obtenues automatiquement à partir du contenu des modèles B. Leur démonstration nécessite une intervention humaine conséquente si des interactions avec ces outils de preuve sont nécessaires (dans le cadre formel de B, la preuve automatique est indécidable).

Objectif:
Dans le cadre d’un projet de R&D européen (https://www.clearsy.com/recherche-et-developpement/aidoart/), CLEARSY souhaite utiliser l’IA et plus particulièrement l’apprentissage automatique pour faciliter la preuve de ces formules mathématiques. A partir d’une base de données publique de formules mathématiques issues de projets B industriels (https://github.com/CLEARSY/apero), il s’agit de déterminer comment les techniques d’apprentissage peuvent permettre de réduire le temps de preuve.

Déroulement:
Après une phase d’analyse du cadre technique et technologique et des données d’entrée, il s’agit de:

• Proposer une ou plusieurs stratégies d’utilisation de l’IA (prétraitement des données, approche, algorithme, paramétrisation).
• Démontrer par un POC (preuve de concept) la faisabilité du projet sans interaction avec l’outil Atelier B (classification supervisée de PO).
• Interfacer une solution d’apprentissage automatique avec l’outil Atelier B (Machine Learning).
• Eventuellement intégrer une solution DevOps de traitement de preuve.

Compétences recherchées :

• Python-DevOps (Github / Gitlab)
• IA pratique
• Autonomie, Force de proposition
• Travail en équipe

Localisation : Aix en Provence
Durée : 6 mois
Niveau : Bac +5

Pour postuler merci d’envoyer un Cv et une Lettre de motivation à l’adresse stages-ingenieurs@clearsy.com