Sztuczna inteligencja w dowodzeniu twierdzeń
Informacje ogólne
Kod przedmiotu: | 1000-2M19SID |
Kod Erasmus / ISCED: |
11.3
|
Nazwa przedmiotu: | Sztuczna inteligencja w dowodzeniu twierdzeń |
Jednostka: | Wydział Matematyki, Informatyki i Mechaniki |
Grupy: |
Przedmioty obieralne dla informatyki Przedmioty obieralne na studiach drugiego stopnia na kierunku bioinformatyka |
Punkty ECTS i inne: |
(brak)
|
Język prowadzenia: | angielski |
Rodzaj przedmiotu: | monograficzne |
Skrócony opis: |
Systemy automatycznego dowodzenia stają się coraz istotniejszym narzędziem pracy matematyków i informatyków, zaś uczenie maszynowe jest coraz częściej aplikowaną metodą wzmacniania systemów dowodowych. Celem kursu jest zapoznanie się z praktyczną i teoretyczną wiedzą z zakresu sztucznej inteligencji w dowodzeniu twierdzeń. |
Pełny opis: |
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 |
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 |
Efekty uczenia się: |
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ń. |
Metody i kryteria oceniania: |
Egzamin pisemny |
Właścicielem praw autorskich jest Uniwersytet Warszawski.