Sztuczna inteligencja w dowodzeniu twierdzeń 1000-2M19SID
1. Problemy sztucznej inteligencji w systemach interaktywnego wspomagania dowodzenia
2. Wybór istotnych przesłanek metodami klasycznymi uczenia maszynowego
3. Głębokie sieci neuronowe w dowodzeniu twierdzeń
4. Rachunki logiczne używane w automatycznym dowodzeniu i ich własności praktyczne
5. Ewaluacja stanów dowodowych w różnych rachunkach
6. Wewnętrzne kierowanie przeszukiwaniem przestrzeni dowodów
7. Uczenie ze wzmocnieniem w dowodzeniu twierdzeń
8. Cechy dowodu oparte o własności semantyczne i modele logiczne
9. Metody generatywne w dowodzeniu
Rodzaj przedmiotu
Efekty kształcenia
Wiedza:
1. Zna problemy sztucznej inteligencji w dowodzeniu twierdzeń
2. Rozumie trudności w zaaplikowaniu klasycznych metod sztucznej inteligencji do wnioskowania.
3. Zna podstawowe rachunki automatycznego wnioskowania
4. Umie charakteryzować dowody interaktywne i automatyczne
Umiejętności: Po ukończeniu kursu potrafi zaproponować i zaaplikować metody sztucznej inteligencji do problemu związanego z dowodzeniem automatycznym.
Kompetencje: Rozumie potrzebę dostosowania istniejących metod sztucznej inteligencji do specyfiki dowodzenia i potrafi dokonać takich dostosowań.
Kryteria oceniania
Egzamin pisemny
Literatura
A. Alemi et al. DeepMath - Deep Sequence Models for Premise Selection
J. Harrison: Handbook of Practical Logic and Automated Reasoning
D. Selsam et al.: NeuroSAT - Learning a SAT Solver from Single-Bit Supervision
K. Krstovski, D. Blei: Equation Embeddings
Więcej informacji
Więcej informacji o poziomie przedmiotu, roku studiów (i/lub semestrze) w którym się odbywa, o rodzaju i liczbie godzin zajęć - szukaj w planach studiów odpowiednich programów. Ten przedmiot jest związany z programami:
Dodatkowe informacje (np. o kalendarzu rejestracji, prowadzących zajęcia, lokalizacji i terminach zajęć) mogą być dostępne w serwisie USOSweb: