Intent formalization

Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents (arxiv 2603.17150). Pose l’intent gap : l’écart entre ce que veut l’utilisateur et ce que fait réellement le code généré.

La thèse : la formalisation d’intention (traduire automatiquement les besoins en langage naturel vers des specs formelles vérifiables) est la clé de la fiabilité. Spectre de solutions, des tests légers jusqu’aux specs en logique formelle (Dafny, Verus) avec synthèse de code prouvé correct. Points clés :

• les LLM savent générer des specs significatives qui capturent une vraie intention ;
• des métriques automatisées de solidité et de complétude pour juger une spec ;
• TiCoder : une interaction utilisateur minimale fait passer la correction du code de 40% à 84%.

C’est le cadre théorique de la validation sémantique sans oracle de vérité. Relie opa/cue (les specs) au monde agentique de forge.

À creuser : les métriques solidité/complétude de specs, applicables à la validation de forge ? Liés : webtestpilot, opa, cue, forge