Compiler l'intention en preuve sémantique

Réflexion en cours. Le fil part d’un bug : un système qui avait spec, golden dataset, tests et jury LLM, et qui a quand même accepté une liste vide comme un empty-state valide. Comment ne plus perdre le sens de l’intention entre la phrase et le comportement observé ?

Le fil directeur

• compiler-intention-en-preuve : le récit d’ensemble.

Le rôle du LLM

• llm-compilateur-semantique

Poser le sens

• couche-semantique
• analyse-ontologique
• competency-questions

Compiler et contraindre

• dsl-et-ir
• policies-semantiques
• monde-ferme-vs-owl

Prouver

• inference-data-tests
• alloy-contre-modeles
• semantic-proof-graph
• evolution-ontologique