lecE.tex

\documentclass{beamer}
\usetheme{Warsaw}
\useinnertheme{circles}
\useoutertheme[subsection=false]{smoothbars}
\usepackage[utf8x]{inputenc}
\usepackage[czech]{babel}
\usepackage[T1]{fontenc}
\usepackage{listings}
\usepackage{tikz}
\lstset{basicstyle=\tiny\ttfamily}
\logo{\includegraphics[height=0.5cm]{brmlab.pdf}}

\begin{document}

\AtBeginSection[]
{
  \begin{frame}
    \frametitle{Outline}
    \tableofcontents[currentsection]
  \end{frame}
}

\title{brmiversity: Umělá inteligence \\ a teoretická informatika}
\subtitle{Přednáška č. 14}
\author{Petr Baudiš $\langle${\tt pasky@ucw.cz}$\rangle$}
\institute{
	brmlab 2011\\
	\vskip 1ex
	\pgfdeclareimage[height=4ex]{ccbysa}{by-sa.pdf}
	\pgfuseimage{ccbysa}
}
\date{}
\frame{\titlepage}

\section{Umělá inteligence}

\subsection{}
\begin{frame}{Automatické plánování}
\begin{itemize}
\item Projekční problém: jak bude vypadat situace po dané posloupnosti akcí?
\item Plánovací problém: jaká posloupnost akcí vede k dané situaci?
\item Potřebujeme reprezentovat {\em akce, stavy, situace}
\vskip 3ex
\item Možnost 1: Budeme se dále pohybovat v logice a používat její dokazovací metody
\item Možnost 2: Navrhneme si vlastní algoritmy
\end{itemize}
\end{frame}

\subsection{}
\begin{frame}{Situační kalkulus}
\begin{itemize}
\item Jak v logice reprezentovat stavy měnící se v čase?
\item {\em Akce} jsou logické termy $Go(x,y)$, $Grab(g)$, $Release(g)$
\item {\em Situace} jsou logické termy $S_0$, $Result(a, s)$
\item Plovoucí (fluent) predikáty a funkce --- mění se s časem: $Holding(g,s)$
\item Pevné (rigid) predikáty a funkce
\item Pozor na skryté předpoklady! (Uzavřený svět, jednoznačnost jmen.)
\vskip 3ex
\item {\bf Plán:} Posloupnost akcí
\item $Result([a|seq],s) = Result(seq, Result(a,s))$
\end{itemize}
\end{frame}

\subsection{}
\begin{frame}{Reprezentace akce}
\begin{itemize}
\item Akci můžeme provést jen někdy a má nějaké efekty
\item {\bf Axiom použitelnosti:} $Preconds \Rightarrow Poss(a, s)$
\item {\bf Axiom efektu:} $Poss(a,s) \Rightarrow Changes$
\vskip 3ex
\item Problém rámce --- co se ve světě {\em nemění?}
\item Možnost 1: {\bf Axiom rámce:} $At(o,x,y) \land o \ne Agent \land \lnot Holding(o, Agent, s) \Rightarrow At(o,Result(Go(y,z),s))$
\item Možnost 2: {\bf Axiom následujícího stavu:} Když $Poss(a,s)$, fluent platí v $Result(a,s)$, právě když je efektem $a$, nebo platí v $s$ a $a$ jej nemění
\item Možnost 3: Predikáty $PosEffect(a, F_i)$ a $NegEffect(a, F_i)$
\end{itemize}
\end{frame}

\subsection{}
\begin{frame}{Plánování po vlastním}
\begin{itemize}
\item Dokazování v logice je stále zbytečně obecné a tedy složité
\item Inspirované, ale speciální řešení problému
\vskip 3ex
\item {\bf Stav:} Množina logických atomů, každý pravda či nepravda
\item Kompletně instanciované (bez proměnných); opět fluent a rigid
\vskip 3ex
\item {\bf Akce:} Plánovací operátor překlápející hodnoty atomů
\item Operátor $o$ je trojice $(name(o), precond(o), effects(o))$
\item Kompletně instanciované, $name$ bere parametry a ty dosazuje do $precond$ a $effects$
\vskip 3ex
\item Plánovací doména $\Sigma = (S, A, \gamma)$
\item Plánovací problém $P = (\Sigma, s_0, g)$
\item Plán $\pi = [a_1,a_2,\ldots]$; řeší $P \Leftrightarrow \gamma(s_0,\pi)$ splňuje $g$
\item Plán můžeme dopředně či zpětně ověřit
\end{itemize}
\end{frame}

\subsection{}
\begin{frame}{Plánovací algoritmy}
\begin{block}{Plánování v prostoru stavů}
\begin{itemize}
\item Dopředné plánování: backtracking z počátečního stavu
\item Zpětné plánování: backtracking z koncového stavu
\item Při zpětném plánování můžeme použít liftovanou verzi přechodu
\end{itemize}
\end{block}
\begin{block}{Plánování v prostoru plánů}
\begin{itemize}
\item Začneme s prázdným plánem a plnou sadou cílů $g$
\item Postupně přidáváme akce plnící ještě otevřené cíle
\item Opravujeme {\em kazy} částečného plánu a zachováváme jeho konzistenci řešením {\em hrozeb}
\end{itemize}
\end{block}
\end{frame}

\subsection{}
\begin{frame}{Constraint Satisfaction Problem}
\begin{itemize}
\item Splňování omezujících podmínek (CSP)
\item Máme problém s určitou {\em vnitřní strukturou}, která nám může pomoci najít řešení
\item Třeba Sudoku, barvení map nebo prostor plánů
\item Obecně: Množina proměnných a jejich domén a sada podmínek (extenzionálně nebo intenzionálně)
\item {\bf Stav:} Přiřazení hodnot proměnným
\item Konzistentní stav neporušuje podmínky, úplný stav má ohodnocené všechny proměnné
\end{itemize}
\end{frame}

\subsection{}
\begin{frame}{Řešení CSP}
\begin{itemize}
\item Backtracking --- zkoušíme různá ohodnocení; ale chytře!
\vskip 3ex
\item Obecné doporučení výběru proměnné: fail first
\item {\bf dom heuristika} --- přednostně proměnné s nejmenší doménou
\item {\bf deg heuristika} --- přednostně proměnné s nejvíce podmínkami
\vskip 3ex
\item Obecné doporučení výběru hodnoty: succeed first
\item Forward checking --- pohled o jeden krok vpřed
\item Propagace podmínek --- hranová konzistence, algoritmus AC-3
\item Globální podmínky
\end{itemize}
\end{frame}

\subsection{}
\begin{frame}{Otázky?}
\begin{center}
To je o umělé inteligenci vše!

\vskip 3ex

Samozřejmě mnoho restů \dots

Monte Carlo Markov Chains, Komputační lingvistika, Kálmanovy filtry pořádně, roboti v praxi, DSP\dots
\end{center}
\end{frame}

\section{Datové struktury}

\subsection{}
\begin{frame}{Třídění}
\begin{itemize}
\item Bubble sort --- prohazováním
\item Insertion a selection sort --- budováním nového setříděného pole
\item Quick sort --- pivot a dvě podpole
\item Merge sort --- rekurzivní slučování setříděných bloků; optimalizace hledáním běhů
\item Heap sort, A-sort --- pomocí vyvážené datové struktury
\vskip 3ex
\item Bogosort --- náhodná posloupnost
\item Bucket sort --- přihrádky dle rozsahu (``třídící hashování'')
\item Radix sort --- rekurzivní bucket sort
\end{itemize}
\end{frame}

\subsection{}
\begin{frame}{Otázky?}
\begin{center}
To je vše.

Vícerozměrné struktury, dynamizace, atd.
\end{center}
\end{frame}

\section{Vyčíslitelnost}

\subsection{}
\begin{frame}{Rekapitulace --- rekurzivní funkce}
\begin{itemize}
\item Přirozená čísla (s nulou): nula a kladná celá čísla
\item Numerály: ke každému přirozenému číslu se induktivně dopočítám z nuly
\item Canotorova párovací funkce: každou dvojici přirozených čísel umím zkomprimovat do jednoho čísla
\vskip 3ex
\item Rekurzivní funkce: skládané z funkcí (data) a operátorů (control flow)
\item Primitivně rekurzivní funkce: nemůže se zacyklit
\item Obecně rekurzivní funkce: mohla by se zacyklit, \\ ale určitě to neudělá
\item Rekurzivně spočetná funkce: může se zacyklit
\end{itemize}
\end{frame}

\begin{frame}{Rekapitulace --- logika a množiny}
\begin{itemize}
\item Logický systém: syntax a sémantika, první a druhý řád
\item Formule: pravdivé, nepravdivé; konzistentnost a úplnost
\item Pravdivost či nepravdivost: Existuje korektní ohodnocení?
\item Dokazatelnost: Mužeme odvodit tvrzení z axiomů (teorie)?
\vskip 3ex
\item Gödelova čísla: každé rek. funkci můžu přiřadit přirozené číslo
\item Rekurzivní predikát: oborem hodnot logické formule \\ je obor hodnot rekurzivní funkce
\item Rekurzivní množina: podmnožina přirozených čísel rozhodovaná rekurzivní funkcí
\item Rekurzivně spočetná (enumerable) množina: místo rozhodovací funkci máme generátor všech prvků
\end{itemize}
\end{frame}

\subsection{}
\begin{frame}{Peanova aritmetika}
\begin{itemize}
\item Axiomatizovatelná teorie: Množina dokazatelných formulí \\ je rekurzivně spočetná
\item Teorie {\bf základní aritmetické síly:} přirozená čísla, \\ sčítání a násobení, konečně mnoho axiomů
\item Každá ČRF je reprezentovatelná v teorii ZAS
\end{itemize}
\begin{block}{Peanova aritmetika}
\begin{itemize}
\item 0 je přirozené číslo
\item Relace = je reflexivní, symetrická, tranzitivní a uzavřená
\item Pro každé přirozené čislo je $S(n)$ přirozené číslo $\ne 0$
\item Pokud $S(m) = S(n)$ tak $m=n$ ($\forall m,n$)
\item Je-li predikát $\varphi(n)$ (i) pravdivý pro nulu (ii) pro každé $n$ pokud $\varphi(n)$ tak $\varphi(S(n))$, platí $\varphi$ pro všechna přirozená čísla
\item Sčítání $a+S(b)=S(a+b)$, násobení $a\cdot S(b) = a + (a\cdot b)$ a~uspořádání $\le$
\end{itemize}
\end{block}
\end{frame}

\subsection{}
\begin{frame}{Gödelovy věty o neúplnosti}
\begin{itemize}
\item Mějme bezespornou teorii ZAS $T$
\item Předvěta: Množina formulí $T$ dokazatelných v $T$ \\ není rekurzivní
\vskip 3ex
\item {\bf První věta:} Je-li $T$ axiomatizovatelná, existuje \\ pravdivá formule nerozhodnutelná v $T$
\item Neboli netriviální teorie nemohou být zároveň \\ konzistentní a úplné
\vskip 3ex
\item {\bf Druhá věta:} Říká-li o sobě $T$, že je konzistentní, \\ je nekonzistentní.
\end{itemize}
\end{frame}

\subsection{}
\begin{frame}{Důkaz první Gödelovy věty}
\begin{itemize}
\item {\bf První věta:} Je-li $T$ axiomatizovatelná, existuje \\ pravdivá formule nerozhodnutelná v $T$
\item Množiny $A,B$ jsou {\bf rekurzivně neoddělitelné}, neexistuje-li rekurzivní $M$, aby $A \subseteq M \land B \cap M = \emptyset$
\pause
\item $W_x = \{ y : \Psi(x, y) \downarrow \}$
\item Množiny $A,B$ jsou {\bf efektivně neoddělitelné}, existuje-li $f$:
$$(A \subseteq W_x \land B \subseteq W_y \land W_x \cap W_y = \emptyset) \Rightarrow f(x,y) \downarrow \land (f(x,y) \notin W_x \cup W_y)$$
\vskip 3ex
\item NEPROPADEJTE PANICE
\vskip 3ex
\pause
\item Chceme dokázat, že množina dokazatelných a vyvratitelných formulí je {\bf efektivně neoddělitelná dvojice}
\item Tedy můžeme efektivně najít popis všech předložených dokazatelných a vyvratitelných formulí a efektivně \\ vygenerovat novou, která není ani jedno
\end{itemize}
\end{frame}

\subsection{}
\begin{frame}{Důkaz první Gödelovy věty}
\begin{itemize}
\item {\bf Předvěta:} Množina dokazatelných formulí není rekurzivní
\item {\bf První věta:} Je-li $T$ axiomatizovatelná, existuje \\ pravdivá formule nerozhodnutelná v $T$
\vskip 3ex
\item Vezměme libovolné dvě efektivně neoddělitelné RSM $A,B$ a~popišme je logickým predikátem $G$ resp. $\lnot G$
\item Nové množiny $A',B'$ dokazatelných výroků $G$ a $\lnot G$
\item Lemma 1: $A' \cup B' = \emptyset$ (bezespornost)
\item Předvěta: $A',B'$ nejsou rekurzivní, jinak by separovaly $A,B$
\item Lemma 2: Z předpokladu efektivní neoddělitelnost $A,B$ lze z~určité množiny dokazatelných a nedokazatelných výroků vygenerovat prvek ležící mimo ně
\item Tedy umíme vygenerovat nedokazatelný výrok! QED
\end{itemize}
\end{frame}

\subsection{}
\begin{frame}{Otázky?}
\begin{center}
To je o výpočetní složitosti vše!

\vskip 3ex

Pominuli jsme mnoho dalších návazností: relativní vyčíslitelnost a~aritmetickou hierarchii,
souvislost aritmetiky a vyčíslitelnosti a~logiky, algoritmická náhodnost a Martingály, \dots
\end{center}
\end{frame}

\subsection{}
\begin{frame}{Děkuji vám}
\begin{center}
{\bf pasky@ucw.cz}

\vskip 6ex

Příště: Appendix (nejspíš bez slajdů)

Divné neuronové sítě, Kálmánovy filtry, Patience sort a Funnel sort, \dots

\vskip 3ex

brmiverzita (snad) nekončí!

Přihlašte se do {\bf announce@brmlab.cz} (pár mailů měsíčně).
\end{center}
\end{frame}

\end{document}