Uniwersytet Warszawski - Centralny System Uwierzytelniania
Strona główna

Sztuczna inteligencja w dowodzeniu twierdzeń

Informacje ogólne

Kod przedmiotu: 1000-2M19SID
Kod Erasmus / ISCED: 11.3 Kod klasyfikacyjny przedmiotu składa się z trzech do pięciu cyfr, przy czym trzy pierwsze oznaczają klasyfikację dziedziny wg. Listy kodów dziedzin obowiązującej w programie Socrates/Erasmus, czwarta (dotąd na ogół 0) – ewentualne uszczegółowienie informacji o dyscyplinie, piąta – stopień zaawansowania przedmiotu ustalony na podstawie roku studiów, dla którego przedmiot jest przeznaczony. / (0612) Database and network design and administration Kod ISCED - Międzynarodowa Standardowa Klasyfikacja Kształcenia (International Standard Classification of Education) została opracowana przez UNESCO.
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
Przedmioty obieralne na studiach drugiego stopnia na kierunku bioinformatyka
Punkty ECTS i inne: (brak) Podstawowe informacje o zasadach przyporządkowania punktów ECTS:
  • roczny wymiar godzinowy nakładu pracy studenta konieczny do osiągnięcia zakładanych efektów uczenia się dla danego etapu studiów wynosi 1500-1800 h, co odpowiada 60 ECTS;
  • tygodniowy wymiar godzinowy nakładu pracy studenta wynosi 45 h;
  • 1 punkt ECTS odpowiada 25-30 godzinom pracy studenta potrzebnej do osiągnięcia zakładanych efektów uczenia się;
  • tygodniowy nakład pracy studenta konieczny do osiągnięcia zakładanych efektów uczenia się pozwala uzyskać 1,5 ECTS;
  • nakład pracy potrzebny do zaliczenia przedmiotu, któremu przypisano 3 ECTS, stanowi 10% semestralnego obciążenia studenta.

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

Przedmiot nie jest oferowany w żadnym z aktualnych cykli dydaktycznych.
Opisy przedmiotów w USOS i USOSweb są chronione prawem autorskim.
Właścicielem praw autorskich jest Uniwersytet Warszawski.
ul. Banacha 2
02-097 Warszawa
tel: +48 22 55 44 214 https://www.mimuw.edu.pl/
kontakt deklaracja dostępności USOSweb 6.8.0.0-931e56a2a (2022-09-30)