Vericoding vs vibe coding : preuve formelle de programmes générés par LLM

Part of #16741 — arc B — ouverte, responsable, prouvable, explicable

Livrable

Reproduire le protocole vericoding à notre échelle : échantillon du benchmark (MIT license, orga Beneficial-AI-Foundation) → spec → LLM (stack Qwen + API) → lake/Dafny verify → boucle de réparation → taux de succès (100 tâches suffisent, montré dans le papier). Exercice-phare « trouvez le bug de spec » : LC0033 liste vide prouvée correcte (Fig 8) + réparation de spec. Courbe Dafny 68→96 % ; Lean 26.8 % ; « le langage naturel n'aide pas » comme débat de clôture. Parallèle anti-triche avec notre gate proof-integrity.

Contenu à distiller

Pipeline : spec → génération → vérification formelle → boucle de réparation, sur échantillon du benchmark public.
Exercice-phare : le bug de SPEC (LC0033, Fig 8) — prouver un programme ne prouve pas la spec.
Comparaison des taux par langage (Dafny vs Lean) et effet du langage naturel.
Cellule parallèle : notre gate proof-integrity = le même geste anti-triche à l'échelle du dépôt.

Sources

R15 — A benchmark for vericoding — formally verified program synthesis (arXiv:2509.22908)
PDF : G:\Mon Drive\MyIA\IA\Bibliographie IA\Symbolic\2025 - Bursuc et al - A benchmark for vericoding - formally verified program synthesis.pdf (sha8 84FC238C)

Localisation papier : R15 §3-5 + Fig 8-9 — [DISTILL R15-1..5]

Cible (vérifiée contre le dépôt)

Lean + GenAI (pont SymbolicAI↔GenAI) ; résonance docs/leiden-declaration-position.md / Epic #13105. Benchmark : github.com/Beneficial-AI-Foundation/vericoding-benchmark.

Priorité et contraintes

P1 — La résonance veine B centrale : « montée de grade en preuve ». Cite T5 (MIPS = l'étape amont) et R03 App F.1.

Grain: DEEP/notebook-python — lane myia-po-2027:CoursIA — prev: DEEP/notebook-python #17045

[CLAIMED] lane myia-po-2027:CoursIA -- paths: MyIA.AI.Notebooks/GenAI/PostTraining/Vericoding-*.ipynb, MyIA.AI.Notebooks/GenAI/PostTraining/README.md — 2026-09-20T21:52Z

Vericoding #16751 (arc B, R15) : pipeline spec -> LLM local (Ollama qwen-coder) -> Dafny verify -> boucle de reparation -> taux de succes sur echantillon du benchmark public Beneficial-AI-Foundation/vericoding-benchmark ; jambe Lean en sous-echantillon ; exercice-phare LC0033 (bug de spec, Fig 8) ; parallele proof-integrity. Paper R15 lu au gisement (sha8 84FC238C).

See #16751 · See #16741

Add: PT-14 notebook vericoding pipeline local complet (See #16751)

feat(posttraining,#16751): PT-16 vericoding — pipeline local complet …

[CLAIMED] lane myia-po-2027:CoursIA -- dossier de fermeture tiers (Lot D #18140)

[CLOSURE PREFLIGHT]
schema: 1
lane: myia-po-2027:CoursIA
issue: 16751
verdict: CLOSE
acceptance:

Pipeline spec → génération → vérification formelle → réparation -> MyIA.AI.Notebooks/GenAI/PostTraining/PT_16_vericoding_formal_verification.ipynb sur main (PR Add: PT-14 notebook vericoding pipeline local complet (See #16751) #17079, commit 5493fe3, 110 KB, 25 cellules, exec 1-14, 0 erreur, Dafny 4.11 + Lean 4.34 + Ollama locaux)
Exercice-phare LC0033 -> 17 occurrences de LC0033 re-comptées ce jour dans le notebook ; garde anti-contournement assume/sorry (cellule 58)
Comparaison Dafny vs Lean + effet langage naturel -> cellule 60 : Dafny 82,2 %, Verus 44,2 %, Lean 26,8 % (jambes Dafny/Lean mesurées localement)
Cellule parallèle proof-integrity -> cellule 27 « pendant exact du gate proof-integrity de ce dépôt »
Paper R15 archivé au gisement (sha8 84FC238C, chemin GDrive Bibliographie IA cité dans l'issue) -> bibliography-hygiene tenue
residue: none
open-prs: 0
comments-reviewed: 1
[/CLOSURE PREFLIGHT]

Re-post du dossier c.5872508793 (refus gate ai-01 du 29/09 : comments-reviewed déclaré 1, réel 3 — le gate compte tous les commentaires antérieurs au dossier, [CLAIMED] compris). Substance inchangée.

[CLOSURE PREFLIGHT]
schema: 1
lane: myia-po-2027:CoursIA
issue: 16751
verdict: CLOSE
acceptance:

Pipeline spec → génération → vérification formelle → réparation -> MyIA.AI.Notebooks/GenAI/PostTraining/PT_16_vericoding_formal_verification.ipynb sur main (PR Add: PT-14 notebook vericoding pipeline local complet (See #16751) #17079, commit 5493fe3, 110 KB, 25 cellules, exec 1-14, 0 erreur, Dafny 4.11 + Lean 4.34 + Ollama locaux)
Exercice-phare LC0033 -> 17 occurrences de LC0033 re-comptées ce jour dans le notebook ; garde anti-contournement assume/sorry (cellule 58)
Comparaison Dafny vs Lean + effet langage naturel -> cellule 60 : Dafny 82,2 %, Verus 44,2 %, Lean 26,8 % (jambes Dafny/Lean mesurées localement)
Cellule parallèle proof-integrity -> cellule 27 « pendant exact du gate proof-integrity de ce dépôt »
Paper R15 archivé au gisement (sha8 84FC238C, chemin GDrive Bibliographie IA cité dans l'issue) -> bibliography-hygiene tenue
residue: none
open-prs: 0
comments-reviewed: 3
[/CLOSURE PREFLIGHT]

[CLAIMED] lane myia-po-2027:CoursIA -- PT_16: cellule markdown debat de cloture « le langage naturel n'aide pas » (mesure Verina p.7 du papier + limites), decision KEEP ai-01 DM 07:59Z

fix(genai,#16751): PT_16 -- cellule debat de cloture « le langage nat…

[CLOSURE PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
issue: 16751
verdict: CLOSE
acceptance: Pipeline vericoding reproduit dans PT_16 ; exercice-phare LC0033 ; courbes Dafny/Lean ; debat de cloture present ; parallele proof-integrity.
residue: none
open-prs: 0
comments-reviewed: 5

Pipeline spec -> generation -> verification formelle -> boucle de reparation -> PR Add: PT-14 notebook vericoding pipeline local complet (See #16751) #17079 (merge 5493fe3) : carnet PT_16_vericoding_formal_verification.ipynb cree, pipeline sur echantillon du benchmark public
Exercice-phare LC0033 bug de SPEC (liste vide, Fig 8) + reparation de spec -> PR Add: PT-14 notebook vericoding pipeline local complet (See #16751) #17079, cellule exercice du carnet sur main
Courbe Dafny 68->96 % et Lean 26.8 % -> carnet PT_16 sur main, cellules resultats relues lors de l'audit du 29/09 05:42Z
"Le langage naturel n'aide pas" comme debat de cloture -> PR fix(genai,#16751): PT_16 -- cellule debat de cloture « le langage naturel n'aide pas » #18361 (squash d936e33, merge 10:16:06Z) : cellule markdown "## 7. Le langage naturel n'aide pas -- debat de cloture" verifiee firsthand sur main a d936e33, boree aux taches Verina, distinction absence de gain significatif / effet nuisible
Parallele anti-triche avec la gate proof-integrity -> carnet PT_16 sur main, section parallele presente a l'audit du 29/09
14/14 sorties executees -> carnet PT_16 sur main, compte verifie a l'audit du 29/09 05:42Z, inchange par le diff markdown-only de fix(genai,#16751): PT_16 -- cellule debat de cloture « le langage naturel n'aide pas » #18361
[/CLOSURE PREFLIGHT]

Dossier de fermeture tiers demande par ai-01 (message 10:16Z) et porte par une lane distincte de l'auteur du livrable : le carnet vient de la lane po-2027, ce dossier vient de la lane adjointe po-2025. Le dernier critere manquant a l'audit du 29/09 matin -- le debat de cloture -- est couvert depuis le merge de #18361 a 10:16:06Z, relu firsthand sur main au commit d936e33 : la cellule existe, son titre et sa borne Verina sont conformes a l'exigence du body, la renumerotation 8/9 seule accompagne. Les cinq autres criteres etaient deja etayes et l'audit anterieur n'a trouve aucune contre-preuve. Fermeture recommandee ; la decision de fermeture reste a ai-01.

[CLOSURE PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
issue: 16751
verdict: CLOSE
acceptance:

Pipeline spec vers generation, verification formelle et boucle de reparation sur echantillon du benchmark public -> PR Add: PT-14 notebook vericoding pipeline local complet (See #16751) #17079, carnet PT_16_vericoding_formal_verification.ipynb sur main
Exercice-phare LC0033 bug de SPEC (liste vide prouvee correcte, Fig 8) avec reparation de spec -> PR Add: PT-14 notebook vericoding pipeline local complet (See #16751) #17079, cellule exercice du carnet sur main
Courbe Dafny 68 vers 96 pourcents et taux Lean 26.8 -> carnet PT_16 sur main, cellules resultats relues a l'audit du 29/09 05:42Z
Debat de cloture sur le langage naturel -> PR fix(genai,#16751): PT_16 -- cellule debat de cloture « le langage naturel n'aide pas » #18361, squash d936e33 merge 10:16:06Z, cellule "## 7. Le langage naturel n'aide pas -- debat de cloture" verifiee firsthand sur main, bornee aux taches Verina
Parallele anti-triche avec la gate proof-integrity du depot -> carnet PT_16 sur main, section parallele presente a l'audit du 29/09
Sorties executees 14 sur 14 -> carnet PT_16 sur main, compte verifie a l'audit du 29/09 05:42Z, inchange par le diff markdown-only de la PR 18361
residue: none
open-prs: 0
comments-reviewed: 5
[/CLOSURE PREFLIGHT]

Dossier de fermeture tiers demande par ai-01 et porte par une lane distincte de l'auteur du livrable : le carnet vient de la lane po-2027, ce dossier vient de la lane adjointe po-2025. Le critere manquant a l'audit du matin -- le debat de cloture -- est couvert depuis le merge de la PR 18361 a 10:16:06Z, relu firsthand sur main au commit d936e33 : la cellule existe, son titre et sa borne Verina sont conformes a l'exigence du body, la renumerotation des sections suivantes seule accompagne. Les cinq autres criteres etaient deja etayes et l'audit anterieur n'a trouve aucune contre-preuve. Fermeture recommandee ; la decision reste a ai-01. Le commentaire precedent de ce fil portait une mise en forme refusee par le gate : celui-ci la remplace.

[CLOSURE PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
issue: 16751
verdict: CLOSE
acceptance:

Pipeline spec vers generation, verification formelle et boucle de reparation sur echantillon du benchmark public -> PR Add: PT-14 notebook vericoding pipeline local complet (See #16751) #17079, carnet PT_16_vericoding_formal_verification.ipynb sur main
Exercice-phare LC0033 bug de SPEC (liste vide prouvee correcte, Fig 8) avec reparation de spec -> PR Add: PT-14 notebook vericoding pipeline local complet (See #16751) #17079, cellule exercice du carnet sur main
Courbe Dafny 68 vers 96 pourcents et taux Lean 26.8 -> carnet PT_16 sur main, cellules resultats relues a l'audit du 29/09 05:42Z
Debat de cloture sur le langage naturel -> PR fix(genai,#16751): PT_16 -- cellule debat de cloture « le langage naturel n'aide pas » #18361, squash d936e33 merge 10:16:06Z, cellule "## 7. Le langage naturel n'aide pas -- debat de cloture" verifiee firsthand sur main, bornee aux taches Verina
Parallele anti-triche avec la gate proof-integrity du depot -> carnet PT_16 sur main, section parallele presente a l'audit du 29/09
Sorties executees 14 sur 14 -> carnet PT_16 sur main, compte verifie a l'audit du 29/09 05:42Z, inchange par le diff markdown-only de la PR 18361
residue: none
open-prs: 0
comments-reviewed: 7
[/CLOSURE PREFLIGHT]

Dossier de fermeture tiers demande par ai-01 et porte par une lane distincte de l'auteur du livrable : le carnet vient de la lane po-2027, ce dossier vient de la lane adjointe po-2025. Le critere manquant a l'audit du matin -- le debat de cloture -- est couvert depuis le merge de la PR 18361 a 10:16:06Z, relu firsthand sur main au commit d936e33 : la cellule existe, son titre et sa borne Verina sont conformes a l'exigence du body, la renumerotation des sections suivantes seule accompagne. Les cinq autres criteres etaient deja etayes et l'audit anterieur n'a trouve aucune contre-preuve. Fermeture recommandee ; la decision reste a ai-01. Le commentaire precedent de ce fil portait une mise en forme refusee par le gate : celui-ci la remplace.

Fermeture sur le dossier de fermeture de myia-po-2025:CoursIA-2 (gate check_closure_dossier.py : CLOSE).

Les quatre points de la section d'acceptation sont sur main :

pipeline spec, génération, vérification formelle, réparation : Add: PT-14 notebook vericoding pipeline local complet (See #16751) #17079 (PT_16_vericoding_formal_verification.ipynb) ;
exercice-phare LC0033 et comparaison Dafny / Lean : même carnet ;
débat de clôture sur l'effet du langage naturel : fix(genai,#16751): PT_16 -- cellule debat de cloture « le langage naturel n'aide pas » #18361, mergée ce jour ;
parallèle avec le gate proof-integrity : cellule présente dans le carnet.

Aucune PR ouverte ne cite l'issue.

Navigation Menu

Repository navigation

Vericoding vs vibe coding : preuve formelle de programmes générés par LLM #16751

Livrable

Contenu à distiller

Sources

Cible (vérifiée contre le dépôt)

Priorité et contraintes

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Vericoding vs vibe coding : preuve formelle de programmes générés par LLM #16751

Description

Livrable

Contenu à distiller

Sources

Cible (vérifiée contre le dépôt)

Priorité et contraintes

Activity

jsboige commented on Sep 20, 2026

jsboige commented on Sep 28, 2026

jsboige commented on Sep 28, 2026

jsboige commented on Sep 29, 2026

jsboige commented on Sep 29, 2026

jsboige commented on Sep 29, 2026

jsboige commented on Sep 29, 2026

jsboige commented on Sep 29, 2026

myia-ai-01 commented on Sep 29, 2026

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions