Data i godzina: wtorek, 16 lipca 11:00 – 12:00
Prelegent: dr Bartosz Naskręcki (WMiI UAM)
Streszczenie: Dynamiczny rozwój metod sztucznej inteligencji opartych na dużych modelach językowych (LLM) otworzył nowe możliwości w dziedzinie automatycznego dowodzenia twierdzeń matematycznych. Chociaż standardowe modele, takie jak GPT-4 i Gemini, mają ograniczone zdolności w tym zakresie, to podejście hybrydowe łączące LLM z algorytmami weryfikującymi może znacząco zwiększyć ich skuteczność. W trakcie wykładu zaprezentuję strategie łączące „halucynacje” generowane przez LLM z procesami weryfikacji algorytmicznej. Przedstawię przypadki zastosowania takich strategii, jak AlphaGeometry i FunSearch, które potrafią formalnie dowodzić skomplikowane twierdzenia z zakresu geometrii euklidesowej i kombinatoryki. Przeanalizujemy również potencjalne kierunki rozwoju tej technologii oraz możliwości tworzenia syntetycznych danych treningowych, które mogą przyczynić się do dalszego postępu w tej dziedzinie.
Miejsce: B1-7/8 oraz online