Expériences de génération de preuves formelles avec LLMs

▶︎ Sujet : Expériences de génération de preuves formelles avec LLMsAu cours des dernières années, l'IA/LLM a évolué rapidement, capable de générer non seulement du texte et des images, mais aussi du code stable. Il y a quelques mois, des modèles à la pointe de la technologie comme GPT 5.4 et Claude Opus 4.6 ont commencé à générer des preuves mathématiques formelles relativement complexes, même pour la correction complexe des transformations de représentation intermédiaire des compilateurs, simplement en fournissant un "modèle" de preuve similaire pour produire des preuves formelles phrasées en conséquence.Cette présentation explorera l'expérience d'utilisation de la série GPT 5 et d'Agda pour écrire des programmes à types dépendants et des preuves de théorèmes formels, démontrant comment les modèles linguistiques, à travers les garanties des prouveurs de théorèmes, génèrent des preuves mathématiquement solides de correction qui sont presque parfaites.▶︎ Présentateur : Chen Liang-Ting, chercheur assistant à l'Académie Sinica, aime essayer diverses nouvelles choses. Ses intérêts récents incluent la théorie des types, les modèles catégoriques, et les preuves ayant une signification computationnelle.*Cette fois, l'événement commence plus tôt ! Il commence à sept heures !----------------L'événement est gratuit et les dons pour le lieu g0v sont les bienvenus. Entrez simplement.Vous êtes les bienvenus pour venir pour交流、交朋友！