Erfahrungen mit der Erstellung formaler Beweise mit LLMs

▶︎ Thema: Erfahrungen mit der Erstellung formaler Beweise mit LLMsIn den letzten Jahren hat sich KI/LLM rasant entwickelt, sie kann nicht nur Texte und Bilder, sondern auch stabilen Code erzeugen. Vor einigen Monaten begannen hochmoderne Modelle wie GPT 5.4 und Claude Opus 4.6, relativ komplexe formale mathematische Beweise zu generieren, selbst für komplexe Korrektheit von Transformationen der Zwischenrepräsentation von Compilern, einfach indem sie eine ähnliche Beweis-"Vorlage" bereitstellen, um entsprechend formulierte formale Beweise zu erstellen.Dieser Vortrag wird die Erfahrungen mit der Verwendung der GPT 5-Serie und Agda zur Erstellung von abhängig typisierten Programmen und formalen Theorembeweisen erkunden, wobei demonstriert wird, wie Sprachmodelle durch die Zusicherungen von Theorembeweisern mathematisch fundierte Beweise der Korrektheit generieren, die nahezu fehlerfrei sind.▶︎ Referent: Chen Liang-Ting, ein Forschungsassistent an der Academia Sinica, der gerne verschiedene neue Dinge ausprobiert. Zu seinen aktuellen Interessen gehören Typentheorie, kategoriale Modelle und Beweise mit computativer Signifikanz.*Dieses Mal beginnt die Veranstaltung früher! Sie beginnt um sieben Uhr!----------------Die Veranstaltung ist kostenlos, und Spenden an den Veranstaltungsort g0v sind willkommen. Einfach hereinkommen.Sie sind herzlich eingeladen, für交流、交朋友！