Serwisy internetowe Uniwersytetu Warszawskiego Nie jesteś zalogowany | zaloguj się
katalog przedmiotów - pomoc

Sztuczna inteligencja w dowodzeniu twierdzeń

Informacje ogólne

Kod przedmiotu: 1000-2M19SID Kod Erasmus / ISCED: 11.3 / (0612) Database and network design and administration
Nazwa przedmiotu: Sztuczna inteligencja w dowodzeniu twierdzeń
Jednostka: Wydział Matematyki, Informatyki i Mechaniki
Grupy: Przedmioty monograficzne dla III - V roku informatyki
Przedmioty obieralne dla informatyki
Punkty ECTS i inne: 6.00
zobacz reguły punktacji
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

Zajęcia w cyklu "Semestr letni 2020/21" (zakończony)

Okres: 2021-02-22 - 2021-06-13
Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Ćwiczenia, 30 godzin więcej informacji
Wykład, 30 godzin więcej informacji
Koordynatorzy: Cezary Kaliszyk
Prowadzący grup: Sebastian Jaszczur, Cezary Kaliszyk
Lista studentów: (nie masz dostępu)
Zaliczenie: Egzamin
Przedmiot dedykowany programowi:

4EU+KURSY

Pełny opis:

Wykład odbędzie się zdalnie. Wykłady będą nagrywane i kolejne części udostępniane (najprawdopodobniej na platformie moodle) w poniedziałki.

Wykładowca będzie dostępny online aby odpowiadać na pytania do wykładu pół godziny przed ćwiczeniami, to jest w poniedziałki od 15:45.

Ćwiczenia będą odbywały się online (najprawdopodobniej przez zoom) w poniedziałki, zaczynając od drugiego tygodnia wykładów do końca semestru w godzinach 16:15-18:00.

Zajęcia w cyklu "Semestr letni 2021/22" (jeszcze nie rozpoczęty)

Okres: 2022-02-21 - 2022-06-15

Wybrany podział planu:


powiększ
zobacz plan zajęć
Typ zajęć: Ćwiczenia, 30 godzin więcej informacji
Wykład, 30 godzin więcej informacji
Koordynatorzy: (brak danych)
Prowadzący grup: (brak danych)
Lista studentów: (nie masz dostępu)
Zaliczenie: Egzamin
Opisy przedmiotów w USOS i USOSweb są chronione prawem autorskim.
Właścicielem praw autorskich jest Uniwersytet Warszawski.