Ce Qui Se Passe en Pratique

Prenons un exemple concret. Vous développez un système de détection de défauts pour une ligne de production industrielle. Vous entraînez un réseau de neurones, vous le vérifiez avec un outil de bound propagation (IBP ou CROWN/LiRPA), et vous prouvez que les perturbations inférieures à un certain seuil ne modifieront pas la classification.

Problème résolu ? Pas exactement.

Votre vérification suppose une sémantique précise des opérations : que signifie exactement une convolution ? Comment sont gérés les bords du tenseur ? Quel modèle d'arrondi utilisez-vous pour les calculs en virgule flottante ?

Dans la pratique, ces détails sont souvent implicites. Le framework PyTorch exécute avec une certaine sémantique. Votre outil de vérification utilise potentiellement une abstraction différente. Et le code déployé en production ? Personne ne garantit vraiment qu'il correspond à l'un ou l'autre.

Les Conventions Implicites Qui Cachent des Pièges

Les sources d'incohérence sont nombreuses :

• Sémantique des opérateurs : PyTorch peut changer d'implémentation entre versions
• Layout des tenseurs : row-major vs column-major peut varier
• Prétraitement : les normalisations sont souvent externalisées
• Virgule flottante : IEEE-754 n'est pas toujours respecté strictement

Dans des systèmes non-critiques, ces variations sont acceptables. Dans des contextes safety-critical (avionique, médecine, énergie), elles sont inadmissibles.

TorchLean comble ce gap en ancrant tout dans une seule sémantique formelle, prouvée et exécutable.

L'Idée Fondamentale

TorchLean repose sur un principe simple mais puissant : le modèle appris est un objet mathématique au même titre qu'une fonction ou un nombre réel. Pas une boîte noire exécutable, mais une entité définie formellement avec laquelle on peut raisonner.

Concrètement, TorchLean propose :

1. Une API vérifiée style PyTorch avec modes eager et compilé
2. Un IR SSA/DAG partagé avec tags d'opérateurs
3. Une sémantique Float32 explicite via un kernel IEEE-754 binaire32 exécutable
4. Des preuves de bound propagation avec certificats vérifiables

Tout cela vit dans Lean 4, un proof assistant puissant qui garantit la correction des preuves.

Pourquoi Lean 4 ?

Lean n'est pas choisi au hasard. C'est un theorem prover moderne qui combine :

• Un langage de programmation fonctionnel (ce qui permet d'écrire du code exécutable)
• Un système de preuves formelles (ce qui permet de prouver des théorèmes)
• Un meta-language puissant (ce qui permet de raisonner sur le code lui-même)

Cette combinaison est exactement ce qu'il faut pour formaliser des réseaux de neurones. Vous pouvez exécuter le réseau (comme en Python) et en même temps raisonner dessus (comme en mathématiques formelles).

1. API Vérifiée avec Modes Eager et Compilé

TorchLean reproduit l'API PyTorch familière mais avec une différence fondamentale : chaque opération est définie formellement. Vous écrivez du code qui ressemble à PyTorch, mais ce code a une sémantique mathématique précise.

Le framework supporte deux modes d'exécution :

• Mode eager : exécution immédiate, utile pour le debug et l'exploration
• Mode compilé : génération d'un graphe de calcul optimisé

Les deux lowers vers un IR SSA/DAG op-tagged partagé. C'est ce même IR qui est utilisé pour l'exécution et pour la vérification. Plus besoin de vérifier un modèle abstrait puis d'espérer que l'implémentation correspond.

2. Sémantique Float32 Explicite

C'est ici que TorchLean se distingue. Au lieu d'utiliser une abstraction floue des nombres réels, TorchLean implémente un kernel exécutable IEEE-754 binary32 avec des modèles d'arrondi proof-relevant.

Concrètement, cela signifie :

• Chaque opération Floating-point est modélisée précisément
• Les preuves utilisent le vrai comportement Float32
• Les coins sombres (NaN, infinis, dénormalisés) sont gérés formellement

Fini les surprises où une preuve mathématique s'effondre à cause d'un overflow non prévu.

3. Bound Propagation avec Certificats

TorchLean intègre des techniques de bound propagation directement dans l'écosystème Lean :

• IBP (Interval Bound Propagation) : approche classique, rapide mais conservative
• CROWN/LiRPA : approche par relaxation linéaire, plus précise

Chaque résultat de bound propagation produit un certificat vérifiable. Ce n'est pas une estimation : c'est une preuve formelle que certaines propriétés sont garanties.

Robustesse Certifiée

La première application majeure est la vérification de robustesse. Étant donné un réseau et une entrée, peut-on garantir que toute perturbation inférieure à un seuil ne changera pas la classification ?

TorchLean permet de le prouver formellement. Le certificat généré est vérifiable par Lean lui-même. C'est-à-dire : la preuve que le réseau est robuste est mécanisée, revisitable et infalsifiable.

PINNs et Bornes Résiduelles Physiques

Les Physics-Informed Neural Networks (PINNs) intègrent des connaissances physiques dans l'entraînement du réseau. L'idée est de minimiser non seulement l'erreur sur les données, mais aussi la violation des équations physiques.

TorchLean permet de borner explicitement les résidus de ces équations physiques. Vous pouvez prouver, par exemple, que votre réseau de neurones satisfait certaines équations différentielles avec une précision garantie. Utile pour la simulation, le contrôle, ou tout système où la physique doit être respectée.

Contrôleurs Neuronaux Lyapunov

Dernière application majeure : la vérification de contrôleurs neuronaux style Lyapunov.

Un contrôleur Lyapunov est un contrôleur dont on peut prouver la stabilité via une fonction de Lyapunov. Avec des contrôleurs neuronaux, la vérification devient complexe car le réseau lui-même est non-linéaire.

TorchLean permet de vérifier formellement qu'un contrôleur neuronal respecte les critères de stabilité Lyapunov. C'est crucial pour la robotique, les systèmes de contrôle industriels, ou tout système où une instabilité peut avoir des conséquences dangereuses.