Het artikel bespreekt de recente doorbraak van OpenAI met betrekking tot de Navier-Stokes-vergelijkingen, waarbij de nadruk niet ligt op het bewijs zelf, maar op het feit dat er een formeel bewijs in Lean 4 is geleverd.
De auteur benadrukt dat het handmatig formaliseren van wiskundige teksten voorheen extreem tijdrovend was (naar schatting 40 uur per pagina). OpenAI heeft dit proces drastisch versneld door een proces dat normaal honderdduizenden uren zou kosten in slechts 17 uur te voltooien. Deze efficiëntieslag maakt formele verificatie toegankelijk voor andere kritieke domeinen, zoals:
- Beveiligingsrichtlijnen
- Smart contracts
- Missiekritische algoritmen
In de bijbehorende discussie komen nuances naar voren, zoals het belang van infrastructuur (Prove2Me), het verschil tussen de correcte implementatie en de correcte specificatie (de 'specification gap'), en de werkelijke compute-kosten van het proces.
Het deel van Navier-Stokes waar niemand over praat
Onlangs zijn er al meer wiskundige vermoedens opgelost met behulp van AI, en deze werden eveneens vergezeld door formele bewijzen, in het bijzonder met gebruik van Lean 4.
Tot zeer kort geleden was het genereren van machine-verifieerbare formele bewijzen een uiterst tedious proces. In 2005 schreven Henk Barendregt en Freek Wiedijk:
"Om een indicatie te geven van hoeveel werk er nodig is voor formalisatie, schatten we dat het ongeveer één werkweek (vijf werkdagen van acht werkuren) duurt om één pagina uit een wiskundig studieboek voor bachelorstudenten te formaliseren."
Dat was de vuistregel: veertig uur per pagina. En dit in de context van studieboeken. Onderzoekspublicaties zijn veel compacter dan studieboeken. Bovendien is pagina 100 van een studieboek waarschijnlijk grotendeels afhankelijk van de inhoud van pagina 1 tot en met 99. Een zin in een onderzoeksartikel kan echter verwijzen naar alles wat ooit is gepubliceerd.
Stel dat een onderzoeksartikel 20 keer zoveel inspanning vereist om te formaliseren dan een pagina in een studieboek. Dan zou het formaliseren van het 166 pagina's tellende document van OpenAI 132.800 manuren kosten. OpenAI deed er 17 uur over om hun bewijs in Lean te verifiëren. Ik aarzel om het woord "revolutionair" te gebruiken, maar het verlagen van de kosten van iets met vier grootteordes is revolutionair.
Ik heb zelf AI gebruikt om formele bewijzen te genereren om mijn werk te controleren voor een klein blogbericht. Ik zou daar nooit aan hebben gedacht als ik iemand een weekloon had moeten betalen om mijn werk te controleren.
Formele verificatie is niet alleen van toepassing op de wiskunde. Je zou bijvoorbeeld formeel kunnen verifiëren dat een set beveiligingsrichtlijnen consistent is en dat ze, gegeven bepaalde aannames, hun doel bereiken. Je zou formeel kunnen verifiëren dat een smart contract een bepaalde maximale aansprakelijkheid oplegt. Je zou de correctheid van missiekritische algoritmen kunnen verifiëren. Deze problemen zijn eenvoudiger dan het formaliseren van wiskundig onderzoek, en het is makkelijker om het rendement op de investering te kwantificeren.
Discussie
Ross Het werk dat je beschrijft over beveiliging en beleid is een enorm, interessant en kansrijk gebied. Er is al werk verricht aan "geformaliseerd bug-vinden" door Google en AWS (bijv. S3 en DynamoDB prestatieverificatie, TPU-ontwerp), wat al meer dan tien jaar geleden begon. TLA+ werd veel gebruikt, en voor zover ik weet, maakt het gebruik van TLA+ het gebruik van LEAN lijken op een wandeling in het park.
Het werkt en is al jaren in gebruik. Maar (ruwweg gezegd) is "adversarial bug finding" niet de volledige verificatie waar jij over spreekt. Voor zover ik kan zien, is elke enkele van de formele verificatietools een variant van een SAT/SMT-solver. Fijn dat het nu "mainstream" is. Goede tijden.
Commenter U7 Dan Bernstein bespreekt in "Papers with computer-checked proofs" (oorspronkelijk geschreven in 2023) zijn ervaringen met bewijsassistenten en/of -checkers, en geeft enkele andere citaten over de verwachte tijd voor formalisatie (je gegevens uit 2005 zijn wat oud, maar liggen nog steeds in de buurt).
Theo Honohan Ik vind dit een vreemd perspectief. Het geformaliseerde bewijs is iteratief ontwikkeld in Lean met behulp van Prove2Me (https://prove2.me/), een soort gegamificeerde versie van eerdere blueprint-tools voor bewijzen, om een DAG (Directed Acyclic Graph) van bewezen en open subdoelen te coördineren en te onderhouden. De aankondiging van Anthropic stelt: "De inspanning slaagde toen we overstapten op het gebruik van Prove2Me". Voor die tijd streefden ze naar een Lean-bewijs, maar de LLM-agents konden niet bijhouden wat ze al hadden bewezen. Zonder een Lean-bewijs, hoe hadden ze het resultaat kunnen certificeren of er op enige manier zeker van kunnen zijn?
Het eigenlijke punt hier is, zoals steve@discuss.systems (op Mastodon) schreef: "De volledige prestatie is de infrastructuur die ons in staat stelt om LLM-output te valideren, beperkt tot (subdomeinen van) de wiskunde."
John Zhang De ineenstorting van de kosten is het interessante deel, maar ik denk dat de praktische bottleneck verschuift in plaats van verdwijnt. Formele verificatie beantwoordt de vraag: "Heb ik geïmplementeerd wat ik heb opgeschreven?". Het beantwoordt niet de vraag: "Heb ik het juiste opgeschreven?". Die specificatiekloof is precies waar het dure menselijke werk zit voor de use-cases die je noemt — consistentie van beveiligingsbeleid, aansprakelijkheidsplafonds voor smart contracts, missiekritische algoritmen. Gokopere bewijzen maken het echter veel gemakkelijker om te itereren op de stelling, waardoor die kloof in de praktijk kleiner wordt dan voorheen.
Het andere dat verandert: reviews worden "diffable". Twee bewijstoestanden, een gecontroleerd artefact waar je naar kunt wijzen, in plaats van een argument in proza dat elke keer opnieuw moet worden afgeleid wanneer iemand anders het leest.
Hein Het Lean-formalisatieproces van OpenAI voor NV kostte ongeveer 1 of 2 miljoen dollar aan rekenkracht (compute). Die dollarwaarde is ongeveer gelijk aan 10.000 menselijke wiskundige uren. Jouw schatting van "132.800 manuren" om het NV-bewijs te formaliseren zou ongeveer tien keer zoveel kosten als het betalen van de OpenAI LLM om het te formaliseren.
Het deel van Navier-Stokes waar niemand over praat
Onlangs zijn er al meer wiskundige vermoedens opgelost met behulp van AI, en deze werden eveneens vergezeld door formele bewijzen, in het bijzonder met gebruik van Lean 4.
Tot zeer kort geleden was het genereren van machine-verifieerbare formele bewijzen een uiterst tedious proces. In 2005 schreven Henk Barendregt en Freek Wiedijk:
"Om een indicatie te geven van hoeveel werk er nodig is voor formalisatie, schatten we dat het ongeveer één werkweek (vijf werkdagen van acht werkuren) duurt om één pagina uit een wiskundig studieboek voor bachelorstudenten te formaliseren."
Dat was de vuistregel: veertig uur per pagina. En dit in de context van studieboeken. Onderzoekspublicaties zijn veel compacter dan studieboeken. Bovendien is pagina 100 van een studieboek waarschijnlijk grotendeels afhankelijk van de inhoud van pagina 1 tot en met 99. Een zin in een onderzoeksartikel kan echter verwijzen naar alles wat ooit is gepubliceerd.
Stel dat een onderzoeksartikel 20 keer zoveel inspanning vereist om te formaliseren dan een pagina in een studieboek. Dan zou het formaliseren van het 166 pagina's tellende document van OpenAI 132.800 manuren kosten. OpenAI deed er 17 uur over om hun bewijs in Lean te verifiëren. Ik aarzel om het woord "revolutionair" te gebruiken, maar het verlagen van de kosten van iets met vier grootteordes is revolutionair.
Ik heb zelf AI gebruikt om formele bewijzen te genereren om mijn werk te controleren voor een klein blogbericht. Ik zou daar nooit aan hebben gedacht als ik iemand een weekloon had moeten betalen om mijn werk te controleren.
Formele verificatie is niet alleen van toepassing op de wiskunde. Je zou bijvoorbeeld formeel kunnen verifiëren dat een set beveiligingsrichtlijnen consistent is en dat ze, gegeven bepaalde aannames, hun doel bereiken. Je zou formeel kunnen verifiëren dat een smart contract een bepaalde maximale aansprakelijkheid oplegt. Je zou de correctheid van missiekritische algoritmen kunnen verifiëren. Deze problemen zijn eenvoudiger dan het formaliseren van wiskundig onderzoek, en het is makkelijker om het rendement op de investering te kwantificeren.
Discussie
Ross Het werk dat je beschrijft over beveiliging en beleid is een enorm, interessant en kansrijk gebied. Er is al werk verricht aan "geformaliseerd bug-vinden" door Google en AWS (bijv. S3 en DynamoDB prestatieverificatie, TPU-ontwerp), wat al meer dan tien jaar geleden begon. TLA+ werd veel gebruikt, en voor zover ik weet, maakt het gebruik van TLA+ het gebruik van LEAN lijken op een wandeling in het park.
Het werkt en is al jaren in gebruik. Maar (ruwweg gezegd) is "adversarial bug finding" niet de volledige verificatie waar jij over spreekt. Voor zover ik kan zien, is elke enkele van de formele verificatietools een variant van een SAT/SMT-solver. Fijn dat het nu "mainstream" is. Goede tijden.
Commenter U7 Dan Bernstein bespreekt in "Papers with computer-checked proofs" (oorspronkelijk geschreven in 2023) zijn ervaringen met bewijsassistenten en/of -checkers, en geeft enkele andere citaten over de verwachte tijd voor formalisatie (je gegevens uit 2005 zijn wat oud, maar liggen nog steeds in de buurt).
Theo Honohan Ik vind dit een vreemd perspectief. Het geformaliseerde bewijs is iteratief ontwikkeld in Lean met behulp van Prove2Me (https://prove2.me/), een soort gegamificeerde versie van eerdere blueprint-tools voor bewijzen, om een DAG (Directed Acyclic Graph) van bewezen en open subdoelen te coördineren en te onderhouden. De aankondiging van Anthropic stelt: "De inspanning slaagde toen we overstapten op het gebruik van Prove2Me". Voor die tijd streefden ze naar een Lean-bewijs, maar de LLM-agents konden niet bijhouden wat ze al hadden bewezen. Zonder een Lean-bewijs, hoe hadden ze het resultaat kunnen certificeren of er op enige manier zeker van kunnen zijn?
Het eigenlijke punt hier is, zoals steve@discuss.systems (op Mastodon) schreef: "De volledige prestatie is de infrastructuur die ons in staat stelt om LLM-output te valideren, beperkt tot (subdomeinen van) de wiskunde."
John Zhang De ineenstorting van de kosten is het interessante deel, maar ik denk dat de praktische bottleneck verschuift in plaats van verdwijnt. Formele verificatie beantwoordt de vraag: "Heb ik geïmplementeerd wat ik heb opgeschreven?". Het beantwoordt niet de vraag: "Heb ik het juiste opgeschreven?". Die specificatiekloof is precies waar het dure menselijke werk zit voor de use-cases die je noemt — consistentie van beveiligingsbeleid, aansprakelijkheidsplafonds voor smart contracts, missiekritische algoritmen. Gokopere bewijzen maken het echter veel gemakkelijker om te itereren op de stelling, waardoor die kloof in de praktijk kleiner wordt dan voorheen.
Het andere dat verandert: reviews worden "diffable". Twee bewijstoestanden, een gecontroleerd artefact waar je naar kunt wijzen, in plaats van een argument in proza dat elke keer opnieuw moet worden afgeleid wanneer iemand anders het leest.
Hein Het Lean-formalisatieproces van OpenAI voor NV kostte ongeveer 1 of 2 miljoen dollar aan rekenkracht (compute). Die dollarwaarde is ongeveer gelijk aan 10.000 menselijke wiskundige uren. Jouw schatting van "132.800 manuren" om het NV-bewijs te formaliseren zou ongeveer tien keer zoveel kosten als het betalen van de OpenAI LLM om het te formaliseren.
Groetjes,