Projet long 2025-26 : roadmap

[ocots]

Extension d'un langage dédié à la résolution de problèmes de contrôle optimal

Projet long Sciences du Numérique
ENSEEIHT — 3ᵉ Année Sciences du Numérique
Date : Octobre 2024

---

Responsables

• Olivier Cots — olivier.cots@toulouse-inp.fr, enseignant-chercheur à l’INP-ENSEEIHT de Toulouse
• Guillaume Dupont (@gdupont1) — guillaume.dupont@toulouse-inp.fr, enseignant-chercheur à l’INP-ENSEEIHT de Toulouse

---

Entreprise / Laboratoire

INP-ENSEEIHT-IRIT (UMR CNRS 5505)

---

Mots-clés

Julia, Domain-Specific Language, Traduction des Langages, Contrôle Optimal.

---

Contexte

Le langage Julia est un langage impératif dynamique moderne pourvu d’un système de types particulièrement raffiné et d’une syntaxe épurée héritée de Python et influencée par Lisp. Comme pour Lisp, le langage permet la manipulation de ses propres structures comme citoyens de première classe sous la forme de macros — des fonctions qui prennent de la syntaxe en entrée et fournissent de la syntaxe en sortie. Cela facilite la définition d’extensions au langage, et donc l’intégration directe de langages de modélisation domain-specific.

Depuis début 2023, des chercheurs du laboratoire IRIT de Toulouse et des collaborateurs du Centre Inria Université Côte d’Azur développent un ensemble de packages Julia dédiés au contrôle optimal. Ces packages, regroupés sous le nom control-toolbox, ont été présentés aux conférences JuliaCon 2023, 2024 et 2025. L’un des retours les plus positifs de ces conférences concerne la simplicité d’écriture des problèmes. La modélisation, très proche de la formulation mathématique, permet aux utilisateurs d’écrire et de résoudre rapidement leurs problèmes.

La macro @def appartient au package CTParser.jl. Du point de vue du développeur, le code de cette macro est considérablement simplifié grâce aux capacités d’introspection et de manipulation du code offertes par Julia. L’arbre syntaxique est généré directement par le langage, puisque seule de la syntaxe Julia pure est autorisée. Une analyse syntaxique, effectuée à l’aide du package MLStyle.jl, est ensuite réalisée au cœur de la macro pour étendre la syntaxe du langage avec de nouveaux mots-clés (comme state pour déclarer les variables). Enfin, une passe sémantique permet de générer le problème dans un format prêt à être résolu.

---

Objectifs

Ce projet long vise à étendre et améliorer ce langage dédié (ou Domain-Specific Language, DSL) pour la résolution de problèmes de contrôle optimal. Les étudiants devront travailler sur les axes suivants :

1. Certains collaborateurs (LossControl.jl) souhaitent utiliser notre package pour définir des problèmes qui ne rentrent pas dans la classe actuellement modélisable.
   → Introduire un mécanisme d’annotations permettant à un utilisateur externe d’étendre la syntaxe et de définir sa propre sémantique.

2. Le package ModelingToolkit.jl fait aujourd’hui référence pour la modélisation symbolique sous Julia.
   → Permettre son intégration afin d’utiliser ce framework pour la modélisation de nos problèmes.

3. Le DSL est suffisamment simple pour être compris et utilisé par un modèle de langage (LLM) (documentation).
   → Développer une solution capable de transformer du langage naturel en code formel basé sur notre DSL, à l’instar de l’approche décrite dans cet article.

---

Compétences / connaissances minimales requises

• Bonnes connaissances en langages impératifs (afin de se familiariser rapidement avec Julia)
• Connaissances de base en traduction et conception de langages (analyse syntaxique et sémantique)
• Aucune connaissance spécifique en théorie du contrôle optimal n’est requise

[ocots]

💡 Recommandations pour contribuer

Avant toute contribution, lisez attentivement la documentation suivante :
👉 Developer Guide

Ce guide est indispensable pour comprendre comment développer efficacement dans l’écosystème control-toolbox.
Il explique comment cloner un dépôt, configurer votre environnement de développement, exécuter les tests unitaires et construire la documentation.

---

📘 Aperçu du Developer Guide

1. Cloner le dépôt

   • Copiez l’URL du dépôt (SSH ou HTTPS) et exécutez :

     cd ~/dev
     git clone the-url-you-have-copied

   • Exemple :

     cd ~/dev
     git clone git@github.com:control-toolbox/MyAwesomePackage.jl.git

2. Installer VSCode

   • Installez Visual Studio Code et l’extension Julia.

3. Exécuter les tests unitaires

   • Dans VSCode :

     using Pkg
     Pkg.activate(".")
     Pkg.test()

   • 👉 Consultez la page Unit Testing pour écrire vos propres tests.

4. Construire la documentation

   • Dans le terminal :

     using Pkg
     Pkg.activate("docs")
     Pkg.develop(path=pwd()); include("docs/make.jl"); Pkg.rm("MyAwesomePackage")

   • Ouvrez docs/build/index.html pour visualiser la documentation.
   • Voir aussi Documenter.jl.

---

🧩 Processus de contribution

Une fois votre environnement prêt, suivez le flux de travail standard :

Issue → Branche → Modification → Commit & Push → PR (draft) → Review

---

1. 🪪 Choisir une issue

• Rendez-vous sur la page Issues du dépôt.
• Sélectionnez une tâche existante ou créez-en une nouvelle.

  Chaque contribution doit être associée à une issue.

---

2. 🌱 Créer une branche depuis l’issue

• Depuis la page de l’issue, cliquez sur “Create a branch”.
  Cela crée automatiquement une branche liée à cette issue.

  

---

3. 🧰 Mettre à jour le code

• Clonez ou forkez le dépôt si nécessaire, puis basculez sur la nouvelle branche.
• Apportez vos modifications (ex. supprimer une ligne, corriger un bug, ajouter une fonctionnalité).
• Faites un commit clair avec un message explicite, puis poussez :

  git add .
  git commit -m "Fix typo in documentation"
  git push

---

4. 🔀 Créer une Pull Request (PR)

• Sur GitHub, créez une Pull Request à partir de votre branche.
• Convertissez-la en draft pour signaler que le travail est en cours.
  Cela évite tout merge prématuré et indique aux reviewers que la PR n’est pas encore prête.

---

5. 👀 Demander une relecture

• Choisissez un reviewer, par exemple @ocots ou @jbcaillau.
• Mentionnez-le dans un commentaire :

  @ocots please make a review
  

---

Important

📖 À lire absolument avant toute contribution :
👉 Developer Guide
Vous y trouverez :

• Comment cloner un dépôt et exécuter les tests unitaires
• Comment construire la documentation avec Documenter.jl
• Comment organiser votre environnement VSCode
• Les bonnes pratiques de développement du projet

Note

🔍 Exemple concret :

• Pull Request #652 – OptimalControl.jl

Tip

🧠 Outils utiles :

• Julia in VSCode
• Documenter.jl

---

✅ En résumé

1. Lire le Developer Guide
2. Créer une issue et une branche dédiée
3. Modifier le code et pousser les changements
4. Ouvrir une PR en draft
5. Demander une relecture à un reviewer

[ocots]

Quick meeting with @jbcaillau on 2025-11-04.

• MTK
• Comparison of models in OptimalControlProblems. See NLPModels.consistent_nlps.
• Transformations at the DSL level + formal verifier. Coupling AI + formal methods.
  • Test case: multi-phase, build an example with 2 arcs and have an AI learn it.
  • More complex test case: Loss control.

[ocots]

See comment https://github.com/orgs/control-toolbox/discussions/68#discussioncomment-14825843 and replies.

[ocots]

@joseph-gergaud You can follow these steps.

[ocots]

DSL transformations via LLM:

• https://control-toolbox.org/OptimalControl.jl/stable/manual-ai-llm.html
• https://control-toolbox.org/OptimalControl.jl/stable/rdnopa-2025.html#Syntax-matters
• https://claude.ai/share/8f821909-1419-439f-b03d-a0c0b024dc43

[ocots]

Réunion @jbcaillau @gdupont1 @ocots 13/11/2025

Priorité 1 : OptimalControl DSL ↔ MTK. A clarifier ce qu'est un problème de contrôle optimal en MTK.

Remarque : il est possible d'utiliser un LLM pour générer le compilateur. Avant cela, faire des use cases des transformations.

Autres possibilités :

• Vérification formelle via Coq (pas Lean). Etant donnée une paire de problèmes et la nature de la transformation, vérifier "l'équivalence".
• Avoir un SLM pour faire la transformation de langage naturel vers formel.

[ocots]

Il y a aussi : transformation du problème en suivant des règles, au niveau abstrait DSL.

[ocots]

Réunion 14/11/2025

Participants : @ade4569 @alegoupil @loxim3 @Lupylune @gdupont1 @ocots

• Phase 1 : fin ?
• Il y a 5 pistes :
  • OptimalControl DSL ↔ MTK
  • Vérification après transformation du problème en suivant des règles, fait par un LLM (demande de faire des cas d'usage, des exemples) ou par un utilisateur
  • Transformation du problème en suivant les règles
  • SLM
  • Système d'annotations pour étendre le DSL

[ade4569]

• Fin de la phase 1 : fin de la semaine 5
• Détails des pistes :
  • Traduction de OptimalControl DSL à MTK (Modeling Toolkit) et réciproquement, en particulier sur les problèmes d’optimisations (par exemple, les paramètres sont au préalable définis dans MTK, ce qui n’est pas le cas dans notre DSL)
  • Vérifier si le problème après transformation est bien équivalent au problème attendu
  • Outil permettant la transformation (modélisation) des problèmes de contrôle optimal en DSL (OptimalControl) en respectant les règles liées aux problèmes d’optimisation
  • Développer un Small Language Model spécialisé dans la transformation de problèmes de contrôle optimal en suivant des règles
  • Ajouter un système d’annotations au DSL permettant de répondre à des demandes plus spécifiques de transformation (des paramètres qui ne sont pas inclus par exemple) qui ne sont pas réalisables dans le cadre actuel du DSL

[ocots]

Réunion 02/12/25

• Fournir un ensemble de règles de transformation de problèmes de contrôle optimal : voir page 23 (29 du pdf) de cours contrôle optimal N7.
• Pattern matching : voir MLStyle.jl

[jbcaillau]

hi @ade4569 @alegoupil @loxim3 @Lupylune @gdupont1 @ocots

regarding pattern matching, please consider Moshi.jl that is supposed to be a refactor of MLStyle.jl

see also: control-toolbox/CTParser.jl#77

[ocots]

@ade4569 @alegoupil @loxim3 @Lupylune Pour aider à formaliser le vérificateur, un peu de lecture : https://chatgpt.com/share/692f1f78-697c-8000-a962-956c9a931268

[ocots]

Note de synthèse pour l’implémentation d’un vérificateur de transformation d’OCP

Cette note fournit un point de départ sur l’implémentation d’un vérificateur de transformations de problèmes de contrôle optimal (OCP) définis via la macro @def d’OptimalControl.jl. Elle résume les concepts clés, l’architecture logicielle recommandée, les outils Julia à utiliser, et des exemples illustratifs.

---

1. Contexte et objectif

Lorsqu’on manipule des problèmes de contrôle optimal, il est fréquent de vouloir :

1. Transformer un problème P (par exemple changer l’intervalle de temps de [t0, tf] à [0,1]).
2. Vérifier qu’un problème transformé Q est équivalent à P après transformation, sans nécessairement résoudre le problème.

Le but du vérificateur V(T, P, Q, M) est de tester l’équivalence symbolique et structurelle entre Q et la transformation attendue T(P) :

• Les noms des variables peuvent changer (q → X, u → U) sans affecter la validité.
• Les expressions algébriques peuvent être réécrites (0.5*u^2 ≡ u^2/2).
• Les contraintes, dynamiques et coûts doivent rester équivalents.

---

2. Concepts clés

2.1 Problème de contrôle optimal (OCP)

Un OCP est défini par :

• un intervalle de temps [t0, tf],
• des états x(t) et contrôles u(t),
• des dynamiques : dx/dt = f(t, x, u),
• un coût de type Mayer, Lagrange ou Bolza :

$$J(x, u) = g(x(t_0), x(t_f)) + \int_{t_0}^{t_f} f^0(t, x, u) dt$$

• des contraintes sur les états, contrôles ou combinaisons.

2.2 Transformation T

Une transformation peut être :

• Rescaling du temps : [t0, tf] → [a, b]

$$\tau = \frac{t-t_0}{t_f-t_0} (b-a) + a$$

• Renaming des variables : alpha-renaming
• Modification équivalente des expressions symboliques

On définit T comme un objet contenant les paramètres nécessaires à la transformation.

2.3 Modifications autorisées (ModSet)

Pour rendre le vérificateur tolérant, on définit un ensemble de règles :

• allow_alpha : autorise le renaming des variables
• allow_AC : permet de normaliser les expressions commutatives et associatives
• allow_symbolic : simplification symbolique via Symbolics.jl
• allow_numeric_tolerance : test d’équivalence numérique avec tolérances atol et rtol

---

3. Architecture logicielle recommandée

1. IR minimal de l’OCP :
   Définir un type OCP avec : states, controls, dynamics, cost, constraints.

2. Fonction principale :

   V(T::TransformSpec, P::OCP, Q::OCP, M::ModSet) -> Bool

   • Génère expected = T(P) symboliquement.
   • Normalise P, expected et Q selon ModSet.
   • Déduit un alpha-renaming si autorisé.
   • Compare dynamiques, coût et contraintes.
   • Retourne un booléen + rapport détaillé.

3. Sous-fonctions importantes :

   • build_expected_TP(P, T) : applique la transformation attendue.
   • normalize_ocp(ocp, M) : applique AC-normalization et simplification symbolique.
   • infer_alpha_map(P, Q) : identifie un mapping variables P → Q.
   • expr_equiv(e1, e2, sigma, M) : test d’équivalence symbolique ou numérique.
   • compare_dynamics, compare_constraints : vérification détaillée des composants.

---

4. Outils Julia utiles

1. OptimalControl.jl : définir les problèmes via @def.
   Documentation

2. Symbolics.jl : simplification et manipulation symbolique d’expressions mathématiques.
   Documentation

3. MLStyle.jl : pattern matching sur les AST Julia pour reconnaître et transformer des expressions.
   Documentation

4. DataFrames.jl (optionnel) : organiser et inspecter états, contrôles et variables.

---

5. Exemple minimal

using OptimalControl, Symbolics, MLStyle

# Problème original
P_ir = OCP(2.0, 5.0, [:q, :v], [:u], Dict(:q => :(v), :v => :(u)), :(0.5*u^2), [])

# Transformation T : temps → [0,1]
T = TransformSpec(0.0, 1.0)

# Problème transformé Q avec renaming
Q_ir = OCP(0.0, 1.0, [:X, :V], [:U], Dict(:X => :(V), :V => :(U)), :(0.5*U^2), [])

# Modifications autorisées
M = ModSet(true,true,true,false,1e-8,1e-6)

# Vérification
(all_ok, report) = V(T, P_ir, Q_ir, M)
println("Vérification réussie ? ", all_ok)
println("Rapport :", report)

Résultat attendu : all_ok == true

---

6. Bonnes pratiques

• Toujours créer un IR minimal pour votre OCP, indépendant des noms des variables.
• Normaliser les expressions avant comparaison pour éliminer les différences purement syntaxiques.
• Documenter les transformations autorisées et les tolérances numériques dans ModSet.
• Utiliser Symbolics pour les simplifications et MLStyle pour le pattern matching sur AST.
• Tester votre vérificateur sur plusieurs cas : renaming, réécriture d’expression, changement d’intervalle.

---

7. Extensions possibles

• Comparer des contraintes multi-variables avec réordonnancement toléré.
• Ajouter des tests numériques pour valider l’équivalence approximative des dynamiques.
• Étendre le vérificateur à d’autres transformations T (p. ex. changement d’ordre des états, normalisation des contraintes, transformation affine du contrôle).

---

Cette synthèse fournit un cadre prêt à l’emploi pour implémenter et tester le vérificateur de transformations de problèmes de contrôle optimal dans vos stages.

[ocots]

Réunion du 27/01/2026

Présents : @gdupont1, @ade4569 @alegoupil @loxim3 @Lupylune, @ocots

CR : to be done.

Ressources :

• Exemple de problème de contrôle optimal avec MTK : Goddard

[alegoupil]

CR:

1. SLM

• Pour entraîner un SLM de manière efficace, il faudrait démarrer avec environ 1000 exemples.
• Ces exemples pourraient être augmentés progressivement au fur et à mesure pour observer l’évolution de la performance.
• L’entraînement serait réalisé directement sur un SLM existant, plutôt que de former un modèle from-scratch.
• À clarifier : travailler uniquement sur une classe spécifique de problèmes ou généraliser.

2. Modélisation en MTK

• Un problème potentiel est la perte d’information lors de la modélisation.
• À regarder : SCMIL exemple en MTK du problème de Goddard, chercher d’autres sources potentiellement récentes sur les problèmes de contrôle optimal en MTK.

3. Vérifications des transformations

• Il serait pertinent de s’intéresser à des outils théoriques tels que : semi-groupes, symétries, semi-covariance.
• Pour la Backward semantic, on devrait utiliser des transfo atomiques, qui modifient le moins de paramètres possibles à la fois

Rajouter des sources notamment pour les SLM (définitions, informations du nombre d’exemples, ou pour d’autres éléments théoriques)

[jbcaillau]

@gdupont1, @ade4569 @alegoupil @loxim3 @Lupylune, @ocots salut à tous et merci pour cette première analyse. sur la partie formelle, intéressant de savoir prouver la correction des transfos réalisées, par ex. à l’aide d’outils de preuve comme coq ou lean.

[ocots]

Exemple de preuve en lean obtenue par une IA : article et code.