alreadydone

Go: A Human Counterattack?

Lu Changhai

Last month, a news article titled "Man beats machine at Go in human victory over AI" caught my interest. The article was first published on February 17th by Financial Times. However, I was traveling in London at the time and missed the news by a few days. So, I decided to wait for follow-up news before discussing it. But as I waited, there were no further updates, so I decided to revisit the topic and discuss it again.

The news was about an American amateur 6-dan Go player, Kellin Pelrine, who used the vulnerabilities of the open-source Go programs KataGo and Leela Zero to defeat them with overwhelming superiority.

Before 2015, this type of news would not have made headlines because Go programs were far inferior to human players. However, since DeepMind's Go system, AlphaGo, defeated the French Chinese professional 2-dan player Fan Hui with a score of 5-0 in October 2015, and then defeated the 14-time world champion South Korean professional 9-dan player Lee

alreadydone

Some remarks on Large Language Models

Yoav Goldberg, January 2023

Audience: I assume you heard of ChatGPT, maybe played with it a little, and was impressed by it (or tried very hard not to be). And that you also heard that it is "a large language model". And maybe that it "solved natural language understanding". Here is a short personal perspective of my thoughts of this (and similar) models, and where we stand with respect to language understanding.

Intro

Around 2014-2017, right within the rise of neural-network based methods for NLP, I was giving a semi-academic-semi-popsci lecture, revolving around the story that achieving perfect language modeling is equivalent to being as intelligent as a human. Somewhere around the same time I was also asked in an academic panel "what would you do if you were given infinite compute and no need to worry about labor costs" to which I cockily responded "I would train a really huge language model, just to show that it doesn't solve everything!". We

alreadydone

import data.fintype.basic

variables {ι : Type*} {α : ι → Type*} [S : Π i, setoid (α i)] {β : Sort*}
include S

def quotient.map_pi_pred (p : ι → Prop) (h : ∀ i, p i) :
  @quotient (Π i, p i → α i) pi_setoid → @quotient (Π i, α i) pi_setoid :=
quotient.map (λ f i, f i $ h i) (λ f g he i, he i $ h i)

def quotient.map_pi_pred₂ (p₁ p₂ : ι → Prop) (h : p₂ ≤ p₁) :

alreadydone

import ring_theory.dedekind_domain.ideal
/- https://math.stackexchange.com/a/95857/12932 -/

open_locale non_zero_divisors big_operators

namespace submodule 
variables {R M N P : Type*}
variables [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P]
variables [module R M] [module R N] [module R P]

alreadydone

import topology.semicontinuous

open_locale topological_space filter
open topological_space set filter

variables {α β : Type*} [topological_space α] (f : α → β) (x : α)

section

variables [linear_order α] [t : order_topology α]

alreadydone

import analysis.bounded_variation
import topology.path_connected
/- Authors: Rémi Bottinelli, Junyan Xu -/

open_locale ennreal big_operators
noncomputable theory

section arclength

variables {α E : Type*} [linear_order α] [pseudo_emetric_space E] (f : α → E) {a b c : α}

alreadydone

import topology.uniform_space.basic
import topology.homeomorph

open_locale topological_space uniformity filter
open filter uniform_space set

variables {α β : Type*} [uniform_space α] [uniform_space β]

lemma is_compact.nhds_set_diagonal₁ {α} [uniform_space α] {s : set α} (hs : is_compact s) :
  𝓝ˢ ((λ x, (x, x)) '' s) = 𝓤 α ⊓ 𝓝ˢ (prod.fst ⁻¹' s) := 

alreadydone

import data.polynomial.ring_division

structure EllipticCurve (K : Type*) := (a₁ a₂ a₃ a₄ a₆ : K)

variables {K : Type*} (E : EllipticCurve K)

namespace polynomial
open_locale polynomial

noncomputable def weierstrass_polynomial [ring K] : K[X][X] :=

alreadydone

import data.finsupp.lex
import logic.hydra

variables {α N : Type*} (r : α → α → Prop) (s : N → N → Prop)

namespace finsupp
open relation prod

variable [has_zero N]

alreadydone

variables {α : Sort*} {r : α → α → Prop} {C : α → Sort*} (x : α) (acx : acc r x)
variable F : Π x, (Π y, r y x → C y) → C x

namespace well_founded

lemma fix_F_eq0 : fix_F F x acx = fix_F F x (acc.intro x $ λ y, acx.inv) := rfl
lemma fix_F_eq1 : fix_F F x (acc.intro x $ λ y, acx.inv) = F x (λ y p, fix_F F y $ acx.inv p) := rfl
lemma fix_F_eq2 : fix_F F x acx = F x (λ y p, fix_F F y $ acx.inv p) := rfl
/- fix_F_eq2 fails but fix_F_eq0 and fix_F_eq1 work, demonstrating nontransitivity. -/