Ervaringen met het Genereren van Formele Bewijzen met LLM's

▶︎ Onderwerp: Ervaringen met het Genereren van Formele Bewijzen met LLM'sIn de afgelopen jaren heeft AI/LLM zich snel ontwikkeld, in staat om niet alleen tekst en afbeeldingen te genereren, maar ook stabiele code. Een paar maanden geleden begonnen geavanceerde modellen zoals GPT 5.4 en Claude Opus 4.6 relatief complexe formele wiskundige bewijzen te genereren, zelfs voor complexe correctheid van transformaties van tussentijdse representaties van compilers, simpelweg door een vergelijkbare bewijs "sjabloon" te bieden om overeenkomstig geformuleerde formele bewijzen te produceren.Deze lezing zal de ervaring verkennen van het gebruik van de GPT 5-serie en Agda om afhankelijk getypeerde programma's en formele theorema-bewijzen te schrijven, en demonstreren hoe taalmotoren, door de waarborgen van theorema-bewijzers, wiskundig verantwoorde bewijzen van correctheid genereren die bijna foutloos zijn.▶︎ Presentator: Chen Liang-Ting, een assistent-onderzoeker aan de Academia Sinica, geniet van het uitproberen van verschillende nieuwe dingen. Zijn recente interesses omvatten type-theorie, categorische modellen en bewijzen met computationele betekenis.*Dit keer begint het evenement eerder! Het begint om zeven uur!----------------Het evenement is gratis, en donaties aan de locatie g0v zijn welkom. Loop gewoon naar binnen.Je bent welkom om te komen voor交流、交朋友！