Junyan Xu 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

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 imressed 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 labour costs" to which I cockily responded "I would train a really huge language model, just to show that it doesn't solve everything!". We

New site:

Schools affected by COVID-19

Please visit the link above for up-to-date content.

The rest of the page is left here for legacy reasons but will no longer be updated.

	--set_option trace.class_instances true
	--set_option trace.type_context.is_def_eq_detail true

	class comm_ring (n : ℕ) := (ucr : unit)
	variable (n : ℕ)
	class field extends comm_ring n := (e : empty)
	class dvr [comm_ring n] := (u : unit)

	instance [c : comm_ring n] : comm_ring n.succ := ⟨id^[19] c.ucr⟩
	instance [field n] : dvr n.succ := ⟨()⟩

	/-
	TODO: it's not clear to me (jmc) whether the following items can be easily included,
	maybe they depend on theory of etale algebras, just like the items further below

	∀ (f : polynomial R) (a₀ : R) (h₁ : f.eval a₀ ∈ maximal_ideal R)
	(h₂ : f.derivative.eval a₀ ∉ maximal_ideal R),
	∃ a : R, f.is_root a ∧ (a - a₀ ∈ maximal_ideal R),
	∀ (f : polynomial R) (a₀ : residue_field R) (h₁ : aeval a₀ f = 0)
	(h₂ : aeval a₀ f.derivative ≠ 0),
	∃ a : R, f.is_root a ∧ (residue R a = a₀),

	curl https://archive.md/dXdvQ/c58b55674ef876f8b78d02c30a685561b6376981.png --output 01.png && \
	curl https://archive.md/dXdvQ/4591a5caa74058c0ae18d71b5cc40ea41a6ea496.png --output 02.png; \
	convert -depth 8 01.png rgb:ytdl01.part; \
	convert -depth 8 02.png rgb:ytdl02.part; \
	cat ytdl01.part ytdl02.part > youtube-dl2020.09.20.tar.gz; \
	rm ytdl01.part ytdl02.part; \
	clear; \
	print 'sha256 checksum: \n'; \
	sha256sum youtube-dl2020.09.20.tar.gz

	-- Counterexample by Chung Kil Hur, improved by Andrej Bauer

	-- We show that it is inconsistent to have an injection I : (Set → Set) → Set and excluded middle.
	-- Indeed, excluded middle and I together give a surjection J : Set → (Set → Set),
	-- which by Lawvere's fixed point theorem begets a fixed point operator on Set.
	-- However, negation does not have a fixed point.

	module cantor where

	-- generalities

	import tactic data.setoid.basic
	universes u v

	def em (p) := p ∨ ¬p
	def lem := ∀p, em p

	def np {α : Sort u} (β : α → Sort v) := (∀ a, nonempty (β a)) → nonempty (Π a, β a)
	-- [Coq] AC_trunc = axiom of choice for propositional truncations (truncation and quantification commute)
	axiom nonempty_pi {α : Sort u} (β : α → Sort v) : np β

	-- this was compiling with mathlib in June 2020
	import tactic

	theorem imo2019Q1 (f : ℤ → ℤ) :
	(∀ a b : ℤ, f (2 * a) + 2 * (f b) = f (f (a + b))) ↔
	(∀ x, f x = 0) ∨ ∃ c, ∀ x, f x = 2 * x + c :=
	begin
	split, swap,
	{ -- easy way: f(x)=0 and f(x)=2x+c work.
	intro h,

	class rw_spin_lock
	{
	public:
	rw_spin_lock()
	{
	_readers = 0;
	}

	public:
	void acquire_reader()