458 Matching Annotations
  1. Oct 2022
    1. Automated Reinforcement Learning

      2022-10-13 16:00

    2. Dynamic Selection and Configuration of Optimization Algorithms: From Hyperparameter Control to AutoML

      2022-10-12 11:00

      Black-box optimization (maximization)

      Explore first, exploit near the end: cf. simulated annealing, BO

      Self-adjusting parameter selection

      Adjust parameters during the run. The update depends on the success of previous iterations.

      1-5th rule

      • If mutation was successful, increase mutation probability (heat).
      • If mutation was unsuccessful, decrease mutation probability (cool).

      Dream: dynamic algorithm configuration

      Select algorithm + HPs for next iteration from: - Previous experiments - Current optimization process state

      ELA-based Algorithm Selection

      Cf. SATZilla

    3. User-Priors for Hyperparameter Optimization


      \(\pi\)BO is implemented in HyperMapper.

    4. Recommender Systems for AutoML & AutoML for Recommender Systems


      Goals of the lecture

      • Have a secondary field of research besides AutoML
      • Choose an interesting field of application for AutoML
      • Look out of the box to improve AutoML

      Types of recommendations

      1. Rating prediction
      2. Top-n ranking


      Several rating prediction libraries exist. They focus on CASH (... algorithm selection ...) problem.

    5. On the Automation of Data Science


      4 quadrants of AutoDS

      • Data exploration
      • Data engineering
      • Model building - AutoML
      • Exploitation


      • Architecture search
      • HPO
      • Meta-learning

      Automatic Statistician

      Data exploration

      De Bie: Subjective interestingness (contrast with the data analyst's prior expectations)

      Synth Research Camp

      Data engineering

      • Data wrangling

      Inductive programming - FlashFill - FlashGPT3

      Jesse Davis: time series to tabular data


      Data engineering + AutoML + exploitation

      Input: Partially filled set of tables

      • Autocompete, autocorrect (?)
      • Constraint satisfaction - e.g. employee shift rostering - "Populate each work shift with a nurse."
        • Constraint detection from data

      Constraint learning

      Few ML scientists learn constraints from data.

      • Yields explainable models
      • SMT constraint learning can be encoded as SMT problem (model search).


      MERCS - bidirectional regression and classification decision trees - cf. Bayesian networks (can they do regression?)

      AD-MERCS - anomaly detection

      Alternatives: - Psyche - probabilistic models - Probabilistic programming

    1. AutoML for diverse tasks: cf. general game playing


      Deadline for competitions: 2022-10-13 12:30

    1. datasets

      H2O only supports tabular datasets.

    2. What makes the training nondeterministic: - Neural networks with more than 1 worker - Wallclock time limit

    3. Code will be provided, which can be used to automatically train and explain models on your own datasets.
    1. I recommend this introduction to neural networks: https://www.3blue1brown.com/topics/neural-networks

      Examples of art

      • Helena Nikonole: Bird Language
      • Interspecifics Collective: Recurrent Morphing Radio
        • Infinite music: cf. procedural music by Eno etc., generative.fm
      • Dadabots: Relentless Doppleganger
      • Hexorcismos: Transfiguracion (2020)

      Glossary of machine learning

      • Dataset
      • Training
      • Epoch
      • Hyperparameters
        • Examples: Learning rate, number of epochs
      • Weights/Checkpoints
      • Inference/Prediction


      • Autoencoder
      • Variational autoencoder
      • Generative adversarial network
  2. Sep 2022
    1. Efficient Neural Clause Selection by Weight

      Comments: - Doesn't the exponentiation of symbol weights make some symbols too heavy? - Use a simpler ML model - F: Example: Simple symbol features (arity, predicate/function, ...) - Train age-weight ratio too - Can you learn on larger sets of clauses than pairs?

    2. Evolutionary Computation for Program Synthesis in SuSLik
    3. Walter Dean and Alberto Naibo

      philosophers, logicians

    4. A modular reinforcement learning based automated theorem prover

      Modules: - Parser - Proof state - Proof calculus - Clause encoder - Given clause selection guidance

      Interface a prover should implement to be compatible: OpenAI Gym in Python

    5. Elements of Reinforcement Learning in Saturation-based Theorem Proving

      If the stochasticity of queue selection (age or weight) is useful, could selecting the next clause from the selected queue stochastically be similarly advantageous? We could use a geometric distribution to favor the clauses near the head of the queue.

    6. Proving Theorems using Incremental Learning and Hindsight Experience Replay

      Incremental learning: Solve as many problems in the problem set within an overall time budget (e.g. one week).

      Uniform Budgeted Scheduler: 1 1 2 1 1 2 4 1 1 2 1 1 2 4 8 ...

      Hindsight Experience Replay

      Augmenting training data from failed proof searches:

      We used to be data poor and now we are data rich.

    7. Forbidden Substructure Theorems

      Theorem: interesting, meaningful, valid in some theory

      "interesting": David Hilbert: "One can measure the importance of a scientific work by the number of earlier publications rendered superfluous by it."

      A new kind of mathematician: One who asks good questions to a perfect oracle (ATP)

      We can piggy-back on existing interesting and meaningful theorems by searching for similar theorems - mutating them.

  3. Jun 2022
  4. 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.

  5. 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

  6. 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. ```

  7. 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.

  8. 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.

  9. 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.

  10. Dec 2021
  11. 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
  12. 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.

  13. 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

  14. Jul 2021
  15. 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


  16. 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

  17. Apr 2021
  18. 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)} $$

  19. Nov 2020
  20. 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.

  21. 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.

  22. 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 "|"
  23. 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.

  24. May 2020
  25. 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
  26. 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
  27. Jan 2020
    1. Which core is the best to emulate(some console/game)?

      Emulation General Wiki contains comparisons of emulators of various platforms.

  28. Dec 2019
  29. 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. μ

      The higher mu is, the more closely aligned the true gradient and g must be.

    2. comparable

      [close on average]

    3. stepsizeαk

      learning rate

    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. ∑j=1tjlog(pj)

      This expression should be negated so that the loss increases as \(p_k\) decreases.

    2. negative log likelihood for the linearregression

      Assumption: y is a linear function of x with Gaussian noise with the same standard deviation (sigma) in each dimension.