Skip to content

Instantly share code, notes, and snippets.

View alreadydone's full-sized avatar

Junyan Xu alreadydone

  • Universität Heidelberg
  • Heidelberg / Shenzhen
  • 04:48 (UTC +01:00)
  • X @Junyan_Xu
View GitHub Profile
import Mathlib.Tactic
inductive E
| lit : Bool → E
| var : Nat → E
| ite : E → E → E → E
deriving DecidableEq
def E.hasNestedIf : E → Bool
| lit _ => false
import order.zorn
import category_theory.category.preorder
import category_theory.limits.cones
universes u v w
namespace category_theory
open limits

Reinforcement Learning for Language Models

Yoav Goldberg, April 2023.

Why RL?

With the release of the ChatGPT model and followup large language models (LLMs), there was a lot of discussion of the importance of "RLHF training", that is, "reinforcement learning from human feedback". I was puzzled for a while as to why RL (Reinforcement Learning) is better than learning from demonstrations (a.k.a supervised learning) for training language models. Shouldn't learning from demonstrations (or, in language model terminology "instruction fine tuning", learning to immitate human written answers) be sufficient? I came up with a theoretical argument that was somewhat convincing. But I came to realize there is an additional argumment which not only supports the case of RL training, but also requires it, in particular for models like ChatGPT. This additional argument is spelled out in (the first half of) a talk by John Schulman from OpenAI. This post pretty much

@cedrickchee
cedrickchee / LLMs.md
Last active January 24, 2024 06:16 — forked from yoavg/LLMs.md
Fix typos and grammar of the original writing.

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

@yoavg
yoavg / LLMs.md
Last active December 27, 2025 05:35

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

@alreadydone
alreadydone / unify_blowup.lean
Last active April 19, 2022 13:05
Unification during typeclass inference leads to exponential blowup.
--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 := ⟨()⟩
@jcommelin
jcommelin / henselian_etale.lean
Created September 4, 2021 09:27
Additions to henselian.lean after good etale API
/-
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
@andrejbauer
andrejbauer / UniverseInjection.agda
Last active February 28, 2021 10:27
Formalization of the fact that a dependent type theory with excluded middle cannot have a universe Set such that Set → Set injects into Set.
-- 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
@alreadydone
alreadydone / choice_and_excluded_middle.lean
Last active February 19, 2023 19:07
Implications involving choice principles, extensionality / quotient exactness, excluded middle, and classical/intermediate logics in type theory.
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 β