Compiler intention en preuve

Reflexion en cours, je pense a voix haute.

Le vrai problème, je crois, ce n’est pas de transformer une spec en tests. C’est de préserver le sens de l’intention sur toute la chaîne :

intention humaine
→ concepts métier
→ règles sémantiques
→ obligations vérifiables
→ données discriminantes
→ tests générés
→ observations réelles
→ preuve

Le bug qui me hante

Spec banale : « un utilisateur consulte les données de son organisation active ». Le système avait tout : une spec, un golden dataset, des tests, un jury LLM, une interface bien rendue. Et pourtant il a accepté ça :

liste vide → empty state valide → feature OK

Alors que la sémantique complète disait l’inverse : Alice membre de Org A, Org A contient A1 et A2, Alice consulte Org A, donc Alice doit voir exactement A1 et A2. Le LLM a jugé l’interface localement (« ça a l’air d’un empty state correct ») au lieu d’exécuter la logique fonctionnelle. Tout le reste découle de là.

L’idée

Arrêter de demander au LLM si la feature paraît correcte. Lui demander de compiler ce que “correcte” signifie, puis faire exécuter cette définition par des mécanismes déterministes. Le LLM devient un llm-compilateur-semantique, pas un oracle.

La chaîne que j’imagine, de la phrase au verdict :

• couche-semantique : poser les niveaux de sens, du vocabulaire à la preuve.
• analyse-ontologique : quelles choses existent, quelles relations changent le comportement.
• competency-questions : les questions auxquelles le modèle doit savoir répondre.
• dsl-et-ir : abaisser tout ça en DSL lisible puis IR calculable, par passes contrôlées.
• policies-semantiques : opa/Rego comme linter de la formalisation, pas du test.
• monde-ferme-vs-owl : raisonner en monde fermé pour le test, pas en open-world OWL.
• inference-data-tests : dériver les données attendues par exécution, pas par le LLM.
• alloy-contre-modeles : chercher les mondes que l’oracle laisse passer à tort.
• semantic-proof-graph : tracer toute la dérivation, de la ligne de spec au verdict.
• evolution-ontologique : chaque bug enrichit le modèle, pas seulement les tests.

Les statuts de preuve

Un test vert ne suffit plus. Une clause traverse des niveaux : EXTRACTED, ONTOLOGY_ALIGNED, DISAMBIGUATED, FORMALIZED, SEMANTICALLY_VALIDATED, ANSWERABLE, INSTANTIATED, GENERATED, EXECUTED, PROVEN, et enfin DISCRIMINATING (les contre-modèles plausibles sont rejetés). C’est ce dernier cran qui me paraît être la vraie preuve.

Formulation que je garde sous le coude

La Forge utilise le LLM comme compilateur sémantique pour transformer une intention en modèle ontologique et opérationnel explicite. Ce modèle est contraint par des policies déterministes, abaissé en IR exécutable, instancié sur des données discriminantes, puis relié par un graphe de provenance aux observations runtime qui prouvent ou invalident chaque propriété.

À creuser : est-ce que tout cet édifice tient pour une feature CRUD réelle de forge, ou est-ce que je sur-ingénie un cas (le bug RLS) qui se règle plus simplement ? Où est le seuil de rentabilité ? Liés : llm-compilateur-semantique, intent-formalization, webtestpilot, forge