Voordrachten en sprekers

Wiskunde voor goede kunstmatige intelligentie: een persoonlijke zoektocht

Er is tegenwoordig veel aandacht voor kunstmatige intelligentie, en dan niet alleen voor de spannende nieuwe technische mogelijkheden, maar ook voor de risico's van het gebruik ervan. Om risico's te beperken geeft regelgeving in de EU burgers bijvoorbeeld al een `recht op uitleg' van geautomatiseerde beslissingen. Tegelijk staat de EU experimenten toe met auto's die zelfstandig rijden terwijl de bestuurder niet oplet (voorlopig tot 60 km/u).

In de geschiedenis van de kunstmatige intelligentie heeft de wiskunde van begin af aan een fundamentele rol gespeeld, juist ook om de mogelijkheden en beperkingen van de techniek te begrijpen. Wel is die rol van wiskunde in de loop van de tijd flink veranderd. Aanvankelijk stond de wiskundige logica aan de basis van de kunstmatige intelligentie. Formele specificatie van een intelligent systeem in een transparante, voor mensen begrijpelijke vorm was de standaard. Geleidelijk aan groeide het inzicht dat de klassieke logica niet afdoende was voor de ontwikkeling van kunstmatige intelligentie. Dat leidde tot nieuwe wiskundige modellen (zoals niet-monotone logica en Bayesiaanse netwerken) die kunnen omgaan met onzekerheid, onvolledige informatie en inconsistentie. Tegenwoordig wordt gezocht naar wiskundige methoden die het verantwoord gebruik van data-gedreven kunstmatige intelligentie (machine leren) ondersteunen.

In deze lezing vertel ik over mijn persoonlijke tocht door wiskunde en kunstmatige intelligentie. Wat heeft de onvolledigheidsstelling van de logicus Gödel met kunstmatige intelligentie te maken? Wat heeft de niet-monotone logica ons gebracht? Kunnen we met Bayesiaanse netwerken causale kennis ontdekken? Is de wiskunde klaar voor het tijdperk van machine leren?

Ik zal betogen dat nieuwe wiskunde nodig is voor de ontwikkeling van hybride systemen waarin mens en machine elkaars kwaliteiten versterken, en dat argumentatielogica een goede kandidaat is. Presentatie.

Finding Mathematical Proofs Using Computers

Voordracht in het Engels.

In the 1960s, researchers were dreaming of the day where mathematicians would simply type in the formulas they want to prove and computers would do the rest. This day has not come to pass yet, but there has been a lot of progress in the past six decades on finding mathematical proofs automatically, using computer programs called automatic theorem provers. In this talk, I will give an introduction to these automatic provers, explaining how they work via small examples. I will focus on two technologies called resolution and superposition. I will also explain how automatic provers can be used in tandem with so-called interactive theorem provers to allow a fruitful collaboration between humans and computers. Presentation.