436 Matching Annotations
  1. Jun 2022
  2. May 2022
    1. One ATP system runs on one CPU at a time, with access to half (128GB) the memory.

      How is this enforced? What benchmarking framework is used? Options: - runsolver - BenchExec

    2. Intel(R) Xeon(R) E5-2667
    1. Special Variables

      when solver pipelines are used, a third argument will be present that contains the path to the additional output directory used by the previous stage.

  3. Apr 2022
    1. Všichni "odborníci" se shodují, že vakcíny zabraňují těžkému průběhu Covid-19. Jen data jim to trochu kazí... (Anglie Covid úmrtí leden 2022. Zelená neočko, červená očko 2 dávky.)

      Citovaná zpráva: https://assets.publishing.service.gov.uk/government/uploads/system/uploads/attachment_data/file/1052353/Vaccine_surveillance_report_-_week_5.pdf

      Death rates per 100k written in the report (Table 13): - Not vaccinated, 80+: 307.4 or 325.5 - Vaccinated with at least 3 doses, 80+: 69.4 or 78.0

  4. Mar 2022
    1. 7 Completion




      • LPO(\(g > f\)): \({fgfx \to x, gfx \to fgx, ffgx \to x}\)
      • LPO(\(f > g\)): \({fgfx \to x, fgx \to gfx, gffx \to x}\)


      LPO with arbitrary symbol order: Completion diverges.

    2. 6 Confluence



      \(r_1 = f(r_2)\)


      \(R\) is not confluent. Critical pair in normal form: \(\left < ggfx, fggx \right >\)

      \(R' = R \cup {ggfx \to fggx}\). - \(R'\) is confluent: the only new critical pair \(\left < fgggfx, gggx \right >\) is joinable. - \(R'\) terminates: LPO with \(g>f\) proves termination.


      The system is not a term rewrite system, because \(Var(l) \nsupseteq Var(r)\). It is not confluent, because \(f(x)\) has at least two normal forms: \(g(x, g(x, x)\) and \(g(x, g(g(x, x), x)\).

    3. Exercises


      Counterexample: \(\to := {(a, c), (b, c)}\)


      \(a \to b\) iff \(a\) encodes Turing machine \(M_a\) and \(b\) encodes a valid terminating computation (sequence of states) of \(M_a\).


      Let \(|w|_a := \varphi_a(w)\).

      \(\varphi(w) := 3^{|w|_a} 2^{|w|_b}\)


      1. Let \(u \to_1 v\). Then \(\varphi(v) = 3^{|v|_a} 2^{|v|_b} = 3^{|u|_a+1} 2^{|u|_b-2} = 3^{|u|_a} 2^{|u|_b} \frac{3}{4} = \varphi(u) \frac{3}{4} < \varphi(u)\).
      2. Let \(u \to_2 v\). Then \(\varphi(v) = 3^{|v|_a} 2^{|v|_b} = 3^{|u|_a-1} 2^{|u|_b+1} = 3^{|u|_a} 2^{|u|_b} \frac{2}{3} = \varphi(u) \frac{2}{3} < \varphi(u)\).



      Let \(a > b\). Then \([b^n a | n \in [0, 1, \ldots]]\) is an infinite chain according to \(>_{Lex}\).

      Note: This exercise completes the discussion of Lemma 2.4.3.


      Let \(s, t\) be terms. Run BFS from \(s\) using \(\leftrightarrow^E\). If \(t\) is encountered, conclude that \(s \approx_E t\). If the BFS finishes enumerating the equivalence class without encountering \(t\), conclude that \(\lnot s \approx_E t\).


      Let \(x \in Var(r) \setminus Var(l)\). Let \(p\) be a position of \(x\) in \(r\).

      Infinite chain:

      • \(t_0 = x\)
      • \(t_{i+1} = r[t_i]_p\)


      1. a
        • Unifier: \({x \to h(a), y \to h(a)}\)
        • Matcher: \({x \to h(a), y \to x}\)
      2. b
        • Unifier: Unsolvable
        • Matcher: \({x \to h(x), y \to x}\)
      3. c
        • Unifier: \({x \to h(y), z \to b}\)
        • Matcher: Unsolvable
      4. d
        • Unifier: Unsolvable
        • Matcher: Unsolvable


      Counterexample TRS \(R\):

      1. \(a \to b\)
      2. \(b \to b\)
    1. rewrite ordering

      If \(>\) is a rewrite ordering and \(s > t\) for each identity \(s \approx t \in E\), then \(s > t\) for each reduction \(s \to_E t\).

    2. there exist X, Y ∈ Mult(M ) with X 6 = ∅, X ⊆A, B = (A\X) ∪ Y , and for all y ∈ Y exists an x ∈ X withx > y.

      the smaller multiset is obtained from the larger one by removing a nonempty subset \(X\) and adding only elements which are smaller than some element in \(X\).

      Source: Term Rewriting and All That, page 22

    1. Schedule

      • Week 1: JitPro
      • Weeks 2 to 4: Megalodon
      • Week 4: Introduction to Coq
      • Weeks 5-6: Isabelle, Mizar
    2. A few simple basic logic exercises in Megalodon: Basic Logic Exercises

      ``` Definition True : prop := forall p:prop, p -> p. Definition False : prop := forall p:prop, p.

      Theorem FalseE: forall A:prop, False -> A. let A. prove False -> A. assume H: False. prove A. prove False. exact H. Qed.

      Definition not : prop -> prop := fun A:prop => A -> False.

      ( Unicode ~ "00ac" ) Prefix ~ 700 := not.

      Theorem notE: forall A:prop, not A -> A -> False. let A. prove not A -> A -> False. assume HnA: not A. assume HA: A. prove False. apply HnA. prove A. exact HA. Qed.

      Theorem notI: forall A:prop, ( A -> False) -> not A. let A. assume HAF: A -> False. prove not A. exact HAF. Qed.

      Definition and : prop -> prop -> prop := fun A B:prop => forall p:prop, (A -> B -> p) -> p.

      ( Unicode /\ "2227" ) Infix /\ 780 left := and.

      Theorem andEL : forall A B:prop, A /\ B -> A. let A B. assume HAB: A /\ B. prove A. apply HAB. prove A -> B -> A. assume HA HB. exact HA. Qed.

      Theorem andER : forall A B:prop, A /\ B -> B. let A B. assume HAB: A /\ B. prove B. apply HAB. prove A -> B -> B. assume HA HB. exact HB. Qed.

      Theorem andI : forall (A B : prop), A -> B -> A /\ B. let A B. assume HA HB. prove A /\ B. let p. assume HABp: A -> B -> p. prove p. exact HABp HA HB. Qed.

      Definition or : prop -> prop -> prop := fun A B:prop => forall p:prop, (A -> p) -> (B -> p) -> p.

      ( Unicode \/ "2228" ) Infix \/ 785 left := or.

      Theorem orE : forall A B C:prop, A \/ B -> (A -> C) -> (B -> C) -> C. let A B C. assume HAB: A \/ B. assume HAC: A -> C. assume HBC: B -> C. prove C. apply HAB. - prove (A -> C). exact HAC. - prove (B -> C). exact HBC. Qed.

      Theorem orIL : forall A B:prop, A -> A \/ B. let A B. assume HA: A. prove A \/ B. let p. assume HAp: A -> p. assume HBp: B -> p. prove p. exact HAp HA. Qed.

      Theorem orIR : forall A B:prop, B -> A \/ B. let A B. assume HB: B. prove A \/ B. let p. assume HAp: A -> p. assume HBp: B -> p. prove p. exact HBp HB. Qed. ```

  5. grid01.ciirc.cvut.cz grid01.ciirc.cvut.cz
    1. SType

      What is SType?

    2. Sep


    3. admit. (** fill in the rest of this proof **)

      let y. assume Hy : y :e ... prove y :e B. apply ReplE_impred U f y Hy. let x. assume Hx H1. rewrite H1. prove f x :e B.

      rewrite matches left hand side and changes its occurrence to right-hand side.

      Other direction: rewrite <- H1

      Rewrite a particular (for example 2nd) occurrence: rewrite H1 at 2

      Alternative: apply (requires a special lambda term)

      Related tactic: reflexivity

    4. ReplE_impred


      Harder to understand, easier to use

    5. exists x :e A, y = F x

      exists x, x :e A /\ y = F x

    6. Repl


    7. Set Theory


      • Empty set
      • Union of set of sets
      • Power set
      • Repl
      • Membership
    8. assume Hp: p.

      To assert that we are proving p -> p at this point:

      prove p -> p.

    9. →I Γ, s ` tΓ ` s → t

      Megalodon: assume

      Can only be applied on implication.

    10. sxt

      s [x := t]

    11. x ∈ Vα \ FΓ

      x is not free in \(\Gamma\).

    12. Conv Γ ` sΓ ` t s≈t

      Most common case: \(\beta\)-normalize the goal

    13. o is also written prop.


    1. X is a pre-fixed point

      \(\Phi X \subseteq X\)

    2. JitPro cheatsheet: JitPro Inference Rules

    3. Object. The name Sep is a term of type set → (set → prop) → set.


      Sep separates elements from a set.

    4. Subgoal 1

      Let \(\Phi\) be monotone. Let \(Y = {u \in A | \forall X \in P A . \Phi X \subseteq X \to u \in X}\). Then \(\Phi Y \subseteq Y\).

    5. lpfp A Φ u

      u lies in the intersection of all pre-fixed points of \(\Phi : P(A) \to P(A)\).

    6. fp A Φ

      fixed-point of \(\Phi : P(A) \to P(A)\)

    7. fp


    8. Known. (set_ext)

      Set extensionality

    9. (∀U ∈ 𝒫 A, Φ U ∈ 𝒫 A)

      \(\Phi\) maps subsets of A to subsets of A.

  6. Feb 2022
    1. {F x|x ∈ A}

      Repl A F

    2. λA B ⇒ ∀x ∈ A, x ∈ B

      \(\lambda A B . \forall x \in A . x \in B\)

      \(\lambda A . \lambda B . \forall x \in A . x \in B\)

    3. when

      [superfluous word]

    4. If P → Q is on the branch, then we can split into two subgoals to refute given by two extended branches: one extended by Q and the other extended by ¬ P

      \(\frac{P \to Q}{Q \mid \neg P}\)

    5. If ¬ (P → Q) is on the branch, then we can extend the branch with P and ¬ Q.

      \(\frac{\neg (P \to Q)}{P, \neg Q}\)

    6. set

      Notation: set is the implicit type.

    7. Tableau Refutations

      Additional rules: - Universal quantifier: - \(\forall x . s \models s[x := t]\) - \(\neg \forall x . s \models \neg s[x := y]\) where \(y\) is fresh - Equality: \(s = t, P[s] \models P[t]\)

    8. Negated Implication

      This is the most common rule.

    9. Theorem: Schroeder Bernstein

      Also known as Cantor–Bernstein theorem.

      Wikipedia: Schröder–Bernstein theorem

    10. set extensionality

      Axiom: \(X \subseteq Y \to Y \subseteq X \to X = Y\)

    11. pre-fixed point

      At least one pre-fixed point exists: A.

    12. (∀U V ∈ 𝒫 A, U ⊆ V → Φ U ⊆ Φ V)

      \(\Phi\) is monotone

    13. Φ Y = Y

      Y is a fixed point of \(\Phi\)

    1. Meds/Bandages/Herbal Meds not referred to on Fate cards are returned to the Storage.


      Assigned Bandages / Meds / Herbal Meds cannot be taken from a Character in any situation except for the rules written on Fate cards.

  7. Jan 2022
    1. platí1 ₒ 2 = id1 . Podobně i obráceně 2 ₒ 1 = id2

      Z \(\phi_1 \circ \phi_2 = id_1\) vyplývá, že \(\phi_1\) je injektivní a \(\phi_2\) je surjektivní.

    2. valuace proměnných z tkonstantními výrazy

      Srovnej s valuací prvky z nosiče.

      Přesnější označení: základní ohodnocení / valuace

    3. Pro každou algebraickou specifikaci S = (D, , E), existuje právě jednatřída iniciálních algeber ve třídě všech modelů specifikace S.

      Jak víme, že existuje alespoň jedna?

    4. Každou valuaci lze jednoznačně rozšířit na zobrazení ’: T(X)  A .

      Musíme ale nejdřív zafixovat algebru.

    5. Jsou tyto modely isomorfní?

      Nejsou. Viz slide 16.

    6. X = [X]T pro každý typ

      Proč ne raději "\(X = [X_d]_{d \in D}\) pro každý druh"?

    7. množin 

      Musí být každá \(\Sigma_\tau\) konečná?

      Aby bylo možné signaturu zapsat konečným řetězcem, musí být každá \(\Sigma_\tau\) konečná.

    8. grupoid
    1. partial concatenation operation

      The operation is partial because not every pair of paths can be concatenated. Two paths can only be concatenated if the target of the first one coincides with the source of the second one.

    1. A team that doesn’tunderstand formal methods has only a notion of whatthey specified using a formal notation and is unclearabout how to refine the development process will almostcertainly sink the project.
      • A team that
        • doesn’t understand formal methods,
        • has only a notion of what they specified using a formal notation, and
        • is unclear about how to refine the development process,
      • will almost certainly sink the project.
    1. Filip Bártek


      Evaluation from the teacher:

      Your grade for your presentation was a B+. Your visuals were quite good, your information was interesting, and your verbal delivery was very solid. Your non-verbal communication, however, had some issues, especially with eye contact and engaging with the audience. These are things that will continue to improve with practice, however. Overall, good work.

  8. Dec 2021
  9. Nov 2021
    1. def curry (α β γ : Type*) (f : α × β → γ) : α → β → γ := sorry def uncurry (α β γ : Type*) (f : α → β → γ) : α × β → γ := sorry
      def curry (α β γ : Type*) (f : α × β → γ) : α → β → γ := λ a b, f (a, b)
      def uncurry (α β γ : Type*) (f : α → β → γ) : α × β → γ := λ p, f p.1 p.2
  10. Oct 2021
    1. Vývoj cen na spotovém vnitrodenním trhu Operátora trhu za posledních dvanáct měsíců
    2. Vývoj cen na spotovém denním trhu Operátora trhu za posledních dvanáct měsíců
    1. EQU (with equality)

      This characteristic is only used for problems all of whose atoms are equalities.

    1. Krajicek:

      We take turns in lecturing.

      Next Friday I will lay out the questions we will be interested in. We will discuss who will talk about what.

      Browse through the Xena materials.

  11. Sep 2021
    1. Creation of a modular proof assistant engine for a logic e-tutor
    2. Computer Verification for Historians of Philosophy

      This lecture is canceled.

    3. Cryptomorphism

      concept equivalence

    4. Contrastive finetuning of generative language models for informal premise selection
    5. Mathematics in the Scholarly Literature
    6. Filip Bártek and Martin Suda Project Proposal: Model-Based Optimization of Strategy Schedules (20m)


    1. an error


      • ValueError if
        • a hyperparameter (HP) instantiation is illegal,
        • an active HP is not specified, or
        • an inactive HP is specified.
      • ConfigSpace.exceptions.ForbiddenValueError if a forbidden clause is violated.

      Source: ConfigSpace/c_util.pyx

  12. Jul 2021
  13. Jun 2021
    1. Krátké animované filmy z festivalu B16

      Promítaly se filmy:

      1. Acid Rain
      2. Takové pěkné město
      3. M E Z E R Y
      4. Divoké bytosti


  14. May 2021
    1. i učitelé mají dobrou paměť a studenty, kteří výuku tak nějak flinkají, obvykle, i přes celou řadu slibů, vést nechtějí

      zbytečná moralizace

    1. Začátkem práce na tvorbě textu končí období, které jsme věnovali přípravě podkladů, tvorbě výstupů, provedení rešerší a dalších činností, které vycházely ze zadání závěrečné práce.
    2. téměř vždy je na vině student

      zbytečná moralizace

  15. Apr 2021
  16. Mar 2021
    1. X⊥⊥Z|Y[π],thenπ(X,Y,Z)canb ereconstructedfromπ↓{X,Y}andπ↓{Y,Z}usingEquation(1.1).

      $$ \pi(x,y,z) = \frac{\pi(x,y) \pi(y,z)}{\pi(y)} = \frac{\pi(x,y) \pi(y,z)}{\sum_{x' \in \mathbb{X}_X} \pi(x',y)} $$

  17. Nov 2020
  18. Oct 2020
    1. Symmetry breaking

      Two propositional variables are symmetrical iff exchanging them leads to the same problem. Their identity carries no relative value.

    1. Difference logic

      Why are there no propositional operations?

    2. EUF

      Theory of Equality and Uninterpreted Functions

    3. if𝜙′/∈SAT, then return𝜙 /∈SAT

      The first SAT is propositional. The second SAT is modulo T.

    1. How does the meaning of the formula change if you replace(𝑥𝑛∨𝑦𝑛∨𝑎𝑛−1)by(𝑥𝑛∨𝑎𝑛−1)∧(𝑦𝑛∨𝑎𝑛−1)?

      The inequality becomes strict.

    2. What is the purpose of auxiliary variables?

      Let's assume that \(a_0 = 1\). Let \(j\) be the smallest index such that \(x_j \neq y_j\). Then \(a_i = 1\) for all \(i < j\).

      • If \(x_j > y_j\), then the formula is unsatisfiable.
      • If \(x_j < y_j\), then \(a_i\) is unconstrained for all \(i \geq j\).

      \(a_i\) is forced to 1 iff \(x\) and \(y\) are constrained at index \(i\).

    3. Why can we replace(𝑥𝑛∨𝑦𝑛∨𝑎𝑛−1)∧(𝑥𝑛∨𝑎𝑛∨𝑎𝑛−1)∧(𝑦𝑛∨𝑎𝑛∨𝑎𝑛−1)just by(𝑥𝑛∨𝑦𝑛∨𝑎𝑛−1)? Hence we need only3𝑛−2clauses and𝑛−1auxiliary variables (𝑎𝑛is also useless)

      The only purpose of \(a_i\) is to signal to the higher indices of \(x\) and \(y\) whether they are constrained.

    4. Why is𝑎0always false and hence useless?

      We must constrain \(a_0\) to 1. Otherwise the whole formula is satisfied by \(a_i = 0\) for all \(i\).

    1. How to encode typical constraints
    2. hard—must be satisfied

      This seems to be possible to implement with transfinite weights.

    3. 𝑝

      Usually \(p < 0.5\).

    4. Unary encoding (order encoding)

      Makes expressing inequalities easy:

      • \(x < i \leftrightarrow \overline{x_i}\)
      • \(x \geq i \leftrightarrow x_i\)
    5. while𝜙contains a pure literal𝑙dodelete clauses containing𝑙from𝜙

      In practice pure literal elimination is usually not used because it does not work efficiently with the data structures used to keep track of unit clauses.

    1. There are few exercises in this unit and all of them are voluntary (only intended for inexperienced students).

    1. Acronyms are all right as long as they are defined explicitly first, for example:

      personal protective equipment (PPE)

    2. Oxford comma”

      Oxford comma is useful especially when a list item contains "and", for example:

      One, two and three, and four.

  19. Sep 2020
    1. If not, you must pick up the discard pile.

      Do I get to pick the card I just flipped over as well?

    1. DO NOT use etc., i.e., or e.g.

      Michael: It is ok to use these short forms in brackets.

    2. hedging

      What exactly is hedging? What does it look like?

    3. Be non-personal

      How should I deal with sentences such as:

      we restrict our attention to learning precedences for predicate symbols only

      In this work, we design a system [...]

      We call the vector w the coefficients [...]

      Source: https://github.com/filipbartek/learning-precedences-from-elementary-symbol-features/releases/download/paar2020%2Fceur-2/Learning_Precedences_from_Simple_Symbol_Features.pdf

    4. and / or

      "and / or" does not seem to be an adequate substitute for "etc." to me.

    1. Punctuation in Academic Writing

      Punctuation is governed by style guides. When writing for a journal, ask them what style guide they follow.

    1. Michael prefers the participants to have their video enabled.

      Homework assignments:

      1. Introduction (paragraph or section)
      2. Body (paragraph or section)
    1. monotone


    2. Two formulae𝜙and𝜓are equivalent, we write𝜙≡𝜓or𝜙|=|𝜓

      Cf. "equisatisfiable"

    3. (𝜙1∧···∧𝜙𝑛)→(𝜓1∨···∨𝜓𝑚)

      Special example: Horn clauses

    4. 𝜙follows from(oris a consequence of)a formula𝜓

      \(\psi\) entails \(\phi\)

    5. all valid formulae are derivable (provable)

      valid -> derivable

    6. only valid formulae are derivable (provable)

      derivable -> valid

    7. Examples of used formal systems

      Not to be discussed in this course:

      • QBF
      • modal logics
      • HOL
    8. British Museum algorithm

      Random search

    9. foundations of mathematics in the late 19thcentury and early 20th century

      Cf. Hilbert's program

    10. derive (prove) formulae


    11. semantic consequence.


    12. {𝑥:𝑥 /∈𝑥}

      How to define a set? For example by set comprehension, as exemplified here.

    1. The course extends on some previous courses. Namely we discuss computational aspects of inference.

      Filip Zelezny: The lectures are to be recorded by the students.

      Karel Chvalovsky: Feel free to unmute yourself and ask questions, or write them in the chat.

    2. First-order resolution

      We rely on theoretical knowledge of e.g. resolution from previous courses and we focus on computation hacks.

    3. Proof assistants

      Is this lecture focused at high-order logic?

    4. 9 23.11. Chvalovský Answer set programming 10 30.11. Chvalovský First-order logic 11 7.12. Chvalovský First-order resolution 12 14.12. Chvalovský Equality and model finding 13 4.1. Chvalovský Proof assistants

      These approaches are more modern than Prolog.

    5. Prolog

      Logical programming is not as important nowadays as it used to be. It is currently not fashionable.

      Filip: Why not use OCaml instead?

      Prolog is an example of declarative programming language.

    6. SAT solving

      Improving SAT solvers leads to making many NP-complete problems easier to solve computationally.

  20. Aug 2020
    1. the place value of the "hundreds" digit in base seven is 49

      I don't understand.

    1. Node List

      How to print the info:

      sinfo -o "%9n %9P %.4c %.6m %.8d %14f %G"

      How to format with xsv:

      sinfo -o "%n|%P|%c|%m|%d|%f|%G" | xsv table --delimiter "|"
  21. Jun 2020
    1. Unfortunately

      I consider it rather fortunate since it allows me to clean up, as demonstrated below.

    1. "There was a 0.95 correlation. I asked them about it. They said, 'We read this article in Chain Store Age magazine that said beer and diapers are correlated, so we put beer next to diapers in all of our stores," he said. "What they did was they created the data that actually validates the data. In effect, they created the signal they used to validate the signal."

      Placement of the goods is a confounder.

  22. May 2020
  23. Apr 2020
    1. Zaměstnanci s emailovou adresou ve formátu: jmeno.prijmeni@cvut.cz

      Configuration that works in Thunderbird in English in Ubuntu:

      • Incoming:
        • Authentication: Normal password
        • Username: bartefil
      • Outgoing:
        • Authentication: Normal password
        • Username: bartefil
  24. Feb 2020
    1. fisk.pdf(x, c, loc, scale)
      y = (x - loc) / scale
      return c * np.power(y, -c-1) * np.power(1 + np.power(y, -c), -2) / scale
  25. Jan 2020
    1. Which core is the best to emulate(some console/game)?

      Emulation General Wiki contains comparisons of emulators of various platforms.

  26. Dec 2019
  27. Nov 2019
    1. více než 75% bylo vyplacenona stipendia studentů

      Musí být více než 75 % z osobních nákladů vyplaceno na stipendia studentů, nebo 75 % z osobních nákladů akademiků, nebo 75 % z celkových nákladů na projekt?

    1. strict concavity

      \(\lambda_i > 0, \sum \lambda_i = 1: \log \sum \lambda_i x_i > \sum \lambda_i \log x_i\)

    2. Pθ0(supθ∈Θ|L(θ,Tm)−L(θ)|> )m→∞−−−−→0

      Starting with m, all the following approximations are strictly contained within epsilon-wide sleeve around the true L.

    3. zj

      \(z^j = (x^j, y^j)\)

    4. consistency

      The more training data we have, the closer we get to the true optimum.

    5. p(y|x) =exp[y(〈w,x〉+b)]1 + exp[〈w,x〉+b]

      \(p(y|x) = \frac{p(x, y)}{p(x)} = \frac{p(x|y) p(y)}{p(x)} = ... \)

    6. Generative learning

      We assume a certain model architecture. We need to estimate the parameters of the model.

    7. x∈Rn,y∈{0,1}withy∼Bern(α)andx|y∼N(μy,V)

      Unknown parameters:

      • Prior: alpha
      • Posterior: mu_0, mu_1, V
    8. Linear Classifier

      Example of discriminative learning version 2

    9. Logistic Regression

      Example of discriminative learning version 1

    10. Gaussian Discriminative Analysis

      Example of generative learning

    11. Discriminative learning(1)

      Example: Softmax layer for classification - estimates class probabilities

    12. max

      Correction: min

    13. conditional


    14. maximum likelihood estimator (MLE)

      Why "likelihood" rather than "probability"? If the domain is real valued, p is a PDF and summing over p values does not correspond to probability.

    1. neural network

      What does the network output?

      1. Value estimate (required for this assignment)
      2. Policy (to be introduced in later lecture)
    1. Forward Message

      JD: The corresponding backward message may be one of the exam assignments.

    2. Universal approximation theorem: one layer is enough


      the universal approximation theorem states that a feed-forward network with a single hidden layer containing a finite number of neurons can approximate continuous functions on compact subsets of Rn, under mild assumptions on the activation function.

    1. Minimální výše měsíčního stipendia v prezenční formě při plnění studijních povinností je 15 000 Kč.

      Skutečné údaje:

      • Minimální stipendium za měsíc: 9 000 Kč. Zdroj: Příkaz rektora č. 11/2019
      • Minimální stipendium za kalendářní rok: 12 x 12 000 Kč. Zdroj: Stipendijní řád - článek 6:1-3
  28. Oct 2019
    1. {trn,val,tst}_kernel_mat.svmlight

      Python: Use the library svmlight. Consider using sklrean.svm.


      Solution consists of:

      • Source code (Python or Matlab)
      • PDF with answers to questions (and nothing else)
    1. 1nin

      Alternative from Xavier: \(\frac{2}{n_{in} + n_{out}}\)

    2. letwiandxibe independentrandom variables

      Is it safe to assume that x_i are independent across i?

    3. =

      Independent across i

    4. E(xi)

      We may need to normalize the input.

    5. αk>0is thelearning rateorstepsize

      Learning rate may be further specialized e.g. for each layer.

    6. θk−αk∇L(θk)

      We move in the opposite direction of the gradient.

    7. yk=σk(xTW)

      Class confidence distribution

    1. ULLN applies

      Proof: Seminar 3, Assignment 4

      1. \(R(h_m) - R_{T^m}(h_m) \leq \sup_{h \in H} |R(h) - R_{T^m}(h)|\) - trivial
      2. \(R_{T^m}(h_H) - R(h_H) \leq \sup_{h \in H} |R(h) - R_{T^m}(h)|\) - easy to see
    2. \(R_{T^m}(h_m) \leq R_{T^m}(h_H)\) because \(h_m \in \argmin_{h \in H} R_{T^m}(h)\).

    3. Neural Networks learned by back-propagation

      Neural networks need not converge to the global minimum. \(R(h_m)\) need not equal \(R(h_H)\).

    1. Empirical risk minimization

      An empirical risk minimization (ERM) algorithm returns \(h_m \in H\) that minimizes \(R_{T^m}(h)\).

      • Excess error: \(R(h_m) - R^*\)
        • Estimation error: \(R(h_m) - R(h_H)\)
        • Approximation error: \(R(h_H) - R^*\)

      An algorithm is statistically consistent in \(H\) iff \(\forall \epsilon > 0: \lim_{m \rightarrow \infty} P(R(h_m) - R(h_H) \geq \epsilon) = 0\).

      The hypothesis space \(H\) satisfies the uniform law of large numbers (ULLN) iff \(\forall \epsilon > 0: \lim_{m \rightarrow \infty} P(\sup_{h \in H} |R(h) - R_{T^m}(h)| \geq \epsilon) = 0\).

      Theorem 1: If \(H\) satisfies ULLN then ERM is statistically consistent in \(H\).

      Corollary 1: The ULLN is satisfied for a finite \(H\).

      Generalization bound for finite hypothesis space \(H\) with \(Im(l) \subseteq [a, b]\): \(P(\max_{h \in H} |R_{T^m}(h) - R(h)| < \epsilon) \geq 1 - 2 |H| \exp(-\frac{2 m \epsilon^2}{(b - a)^2})\)

    1. lunar_lander

      The environment adheres to reward shaping. Each state has a hidden value and reward of an executed action is always the difference between the values of the previous and the current state. (?)

    2. The tasks are evaluated automatically using the ReCodEx Code Examiner.

      We can submit one or more Python source files (modules) with the .py file extension.