trentmkelly/LessWrong-43k huggingface dataset:
Distillation Of DeepSeek-Prover V1.5
by IvanLin — 2024-10-15T18:53:11.199Z

https://arxiv.org/abs/2408.08152 - "DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search"

https://github.com/deepseek-ai/DeepSeek-Prover-V1.5

TL;DR

DeepSeek-Prover-V1.5 is an improved open-source language model for theorem proving in Lean 4.

The paper continues pre-training DeepSeekMath-Base, a math foundation model, and then does supervised fine-tuning on a dataset of incomplete proofs in Lean 4, followed by RL with feedback sourced from Lean 4. DeepSeek-Prover-V1.5 finds proofs using truncate-and-resume, which combines existing proof generation techniques, and a novel Monte-Carlo-Tree-Search (MCTS) algorithm for superior performance.

Overview

Definitions:

Tactic - a command used to manipulate the current proof state
Proof State/Tactic State - Current state of a proof at a given time, includes a list of goals and context.
(tactic state and proof state is often used interchangeably, tactic state is more specific as proof state can also be the state of a proof with a missing step)

Language models trained for theorem proving typically do one of two things:

Proof Step Generation, in which successive tactics are predicted by the prover and verified with a proof assistant. The tactic state is updated and search techniques are used to construct proofs. Each proof step is therefore valid. This method is not computationally efficient because each proof step has to be verified by the proof assistant.
Whole Proof Generation, in which the entire proof is generated in a single step based on the theorem statement. If a proof-step is invalid, the model generates a new proof in the next attempt. This is computationally efficient as a proof assistant is not required, but risks more invalid steps.

DeepSeek-Prover-V1.5 combines proof-step and whole-proof generation, naming the combination truncate-and-resume. Truncate-and-resume starts with whole-proof generation. If Lean detects an error in the proof, all code succeeding the error is removed (truncate), and the valid proof steps are used as a prompt for the next proof segment (resume). This truncate and resume mechanism is used in conjunction with MCTS to search over possible proof states. A reward-free exploration algorithm that uses intrinsic motivation to explore the tactic space is introduced to address reward sparsity.

Pre-Training and SFT

Pre-training:

Further pre-t

...
Improving Model-Written Evals for AI Safety Benchmarking
by Sunishchal Dev — 2024-10-15T18:25:08.179Z

This post was written as part of the summer 2024 cohort of the

ML Alignment & Theory Scholars

program, under the mentorship of Marius Hobbhahn.

Abstract

As model-written evals (MWEs) become more widely used in AI benchmarking, we need scalable approaches to assessing the quality of the eval questions. Upon examination of an existing benchmark dataset (

Perez et al., 2022

), we found a variety of data quality issues in both the model-written and human-written evals (HWEs). These include response divergence (LLMs responding very differently to HWEs and MWEs in the same question category), high separation in sentence embedding clusters, low-quality questions (graded by an LLM judge), response brittleness (unable to elicit different responses from a question), and a host of errors (hallucinations, strange artifacts, hint passing in answer choices, structural/formatting differences, and missing questions or answer choices). We propose a modernized approach to model-written eval generation that largely ameliorates these issues and reduces the risk of similar failure modes in AI safety benchmarking. We also propose four novel metrics for assessing eval dataset quality: LLM-graded quality, Limit Testing, Normalized Volume Ratio, and Embedding Diversity Entropy. The improved datasets and code for these metrics can be found in our

GitHub

.

Introduction

Large Language Models like GPT and Claude have become increasingly useful for AI research, but can we trust them to create evaluations that are critical for AI safety benchmarking? The idea is enticing: automate the process, get results faster, and leverage the model’s creativity to cover scenarios humans may not have thought of. However, we find a variety of issues in current MWE datasets that may yield unreliable results. If we’re not careful, we run the risk of overconfidence in the safety of AI systems due to insufficient validation of model-written evaluations, which could result in unsafe deployments. For example, in the

SafetyPrompts

database, an estimated 45% of AI safety benchmarks contain model-written evals. Given this, we feel it’s important to develop methods for generating evals that are as robust as possible.

We chose to analyze Anthropic’s

Advanced AI Risk dataset

, which was published as part of

Discovering Language Model Behaviors with Model-Written Evaluations

(Per...
Taking nonlogical concepts seriously
by Kris Brown — 2024-10-15T18:16:01.226Z
Link: https://topos.site/blog/2024-10-11-nonlogical-concepts/

I recently wrote this post for the Topos Institute blog, engaging with some recent work in the philosophy of language which I believe is relevant to foundational questions regarding semantics. Many concepts (which we might call 'fuzzy' or tied up with 'values') aren't amenable to logical formalization, so their input is systemically unrepresented in science and technology building. But, through a change in our perspective about what the role of logic is, we can work with these concepts and build an approach to science that bakes these values in, while still being able to use all the great mathematical logic that we are used to. I believe this clarification about meaning sheds light on the problem of communication and alignment of our intentions with those of automated agents, though I only touch upon it in this introductory blog post.

Reasoning vs (purely) logical reasoning

This section is largely an exposition of material in Reasons for Logic, Logic for Reasons (Hlobil and Brandom, 2024).

Logical validity

Logic has historically been a model of good reasoning. Let X,Y,...⊢Z denote that the premises X,Y,... (and so on) altogether are a good reason for Z. Alternatively: it's incoherent to accept all of the premises while rejecting the conclusion. As part of codifying the ⊢ ('turnstile') relation, one uses logical rules, such as A,B⊢A∧B (the introduction rule for conjunction, for generic A and B) and A∧B⊢A (one of two elimination rules for conjunction). In trying to reason about whether some particular inference (e.g. p⊢q∧r) is good, we also want to be able to assume things about nonlogical content. The space of possibilities for the nonlogical content of p,q,r are shown below:

p	q	r
⊤ / ⊥	?	?	?

We care about good reasoning for specific cases, such as p is "1+1=2", q is "The moon is made of cheese", and r is "Paris is in France". Here, we can represent our nonlogical assumptions in the following table:

p	q	r
⊤ / ⊥	⊤	⊥	⊤

Any logically valid inference, e.g. p∨q, p∧r⊢p, is reliable precisely because it does not presuppose its subject matter. Not presupposing anything about p,q,r here means it's incoherent to accept the premises while rejecting the conclusion in any of the eight scenarios. Logical validity requires...
Rashomon - A newsbetting site
by ideasthete — 2024-10-15T18:15:02.476Z

Hello Rationalists!
A while ago I created a concept to evaluate political biases that I call "newsbetting" and made a demo site at rashomonnews.com. Essentially, one receives a news article stripped of identifying information (so stuff like title, author, news source, etc) so that they only get the text of the news article. The reader then places a bet on what they believe the political bias of the news source is - far left, left, center, right or far right. The news source evaluations were taken from allsides.com, but the plan was to eventually have users vote on what they believed the bias was for each news source.

I kind of consider the project closed for the time being, but I wanted to share my results with the community here. There's more data and analysis based off of an initial demo of the site with ~70 users, mostly friends and family.

I understand that "politics is the mindkiller" but I'm hoping it's obvious why this idea is so suited towards rationalists. This idea was directly based on Robin Hanson's famous quote "We vote on values, we bet on beliefs" and combines or potentially could have combined many mainstay ideas found in rationalist communities - betting markets, cryptocurrencies, bayesian statistics, a preoccupation with quantification and bias. I'm hoping to hear feedback from the community that inspired the idea, nothing more. It's a free to use demo site, there's no actual money involved, it's just a way to quantify you biases. Obviously, it's possible to cheat, but I'm hoping this community approaches it in the spirit it was meant to be used in.
Thanks, hope to hear more from the Bayesian perspective regarding this idea.
On the Practical Applications of Interpretability
by Nick Jiang — 2024-10-15T17:18:25.280Z

In late May, Anthropic released a paper on sparse autoencoders that could interpret the hidden representations of large language models. A great deal of excitement followed in the interpretability community and beyond, with people exclaiming the potential of finally breaking down how LLMs think and process information. The initial excitement from SAEs has now died down, so the question is what’s next in the field of interpretability? SAEs are cool, but are they societally useful?

I want to jot down my current thoughts on how interpretability might transfer from an academic subject to a method used widely in industry. As a rough definition, interpretability is broadly the study of how ML models work so effectively, the current main modes being bottom-up (mechanistic interpretability) and top-down (representation engineering) approaches. With the recent rise of large language models (LLMs) like ChatGPT, interpretability research has mainly focused on deciphering the

transformer

.

Whereas most of the current thought on interpretability revolves around AI safety implications (i.e. avoiding a Skynet-like, doomsday scenario where AI destroys humanity), which is clearly relevant and significant, I want to explore how interpretability research might bolster how we benefit from ML (vs. harm reduction).

Hypothesis 1: Model debugging

The biggest problem with model deployment[1] today is the lack of reliability. Companies fear their models will hallucinate, work inconsistently, or inaccurately complete their prescribed tasks, and they need some method to fix their systems when things go wrong.

When models fail, the most common strategy today has been to build “around” them. This might include having a separate LLM to judge the outputs of a main LLM, extremely detailed

micro-prompts

, and retrying on failure

2

. There isn’t a focus on debugging the source—the model itself—which I think is a huge mistake. It’s not to say that these other methods won’t be valuable; I just think that increasing your system’s accuracy from 75% to 90% so you don’t need to have so many additional checks is going to save tons of money long-term.

I also don’t think models will remain “static” particularly for open-ended contexts. Needs for models change. Even today’s machine learning systems (the good ones, at least) are constantly being trained and retrained on the latest data.

If there’s a way to co...
Anthropic's updated Responsible Scaling Policy
by Zac Hatfield-Dodds — 2024-10-15T16:46:48.727Z
Link: https://www.anthropic.com/news/announcing-our-updated-responsible-scaling-policy

Today we are publishing a significant update to our Responsible Scaling Policy (RSP), the risk governance framework we use to mitigate potential catastrophic risks from frontier AI systems. This update introduces a more flexible and nuanced approach to assessing and managing AI risks while maintaining our commitment not to train or deploy models unless we have implemented adequate safeguards. Key improvements include new capability thresholds to indicate when we will upgrade our safeguards, refined processes for evaluating model capabilities and the adequacy of our safeguards (inspired by safety case methodologies), and new measures for internal governance and external input. By learning from our implementation experiences and drawing on risk management practices used in other high-consequence industries, we aim to better prepare for the rapid pace of AI advancement.

The promise and challenge of advanced AI

As frontier AI models advance, they have the potential to bring about transformative benefits for our society and economy. AI could accelerate scientific discoveries, revolutionize healthcare, enhance our education system, and create entirely new domains for human creativity and innovation. However, frontier AI systems also present new challenges and risks that warrant careful study and effective safeguards.

In September 2023, we released our Responsible Scaling Policy, a framework for managing risks from increasingly capable AI systems. After a year of implementation and learning, we are now sharing a significantly updated version that reflects practical insights and accounts for advancing technological capabilities.

Although this policy focuses on catastrophic risks like the categories listed below, they are not the only risks that we monitor and prepare for. Our Usage Policy sets forth our standards for the use of our products, including rules that prohibit using our models to spread misinformation, incite violence or hateful behavior, or engage in fraudulent or abusive practices. We continually refine our technical measures for enforcing our trust and safety standards at scale. Further, we conduct research to understand the broader societal impacts of our models. Our Responsible Scaling Policy complements our work in these areas, contributing to our understanding of current and potential risks.

A framework for proportional safeguards

As before, we maint...
When is reward ever the optimization target?
by Noosphere89 — 2024-10-15T15:09:20.912Z

Alright, I have a question stemming from TurnTrout's post on Reward is not the optimization target, where he argues that the premises that are required to get to the conclusion of reward being the optimization target are so narrowly applicable as to not apply to future RL AIs as they gain more and more power:

https://www.lesswrong.com/posts/pdaGN6pQyQarFHXF4/reward-is-not-the-optimization-target#When_is_reward_the_optimization_target_of_the_agent_

But @gwern argued with Turntrout that reward is in fact the optimization target for a broad range of RL algorithms:

https://www.lesswrong.com/posts/ttmmKDTkzuum3fftG/#sdCdLw3ggRxYik385

https://www.lesswrong.com/posts/nmxzr2zsjNtjaHh7x/actually-othello-gpt-has-a-linear-emergent-world#Tdo7S62iaYwfBCFxL

So my question is are there known results, ideally proofs, but I can accept empirical studies if necessary that show when RL algorithms treat the reward function as an optimization target?

And how narrow is the space of RL algorithms that don't optimize for the reward function?

A good answer will link to results known in the RL literature that are relevant to the question, and give conditions under which a RL agent does or doesn't optimize the reward function.

The best answers will present either finite-time results on RL algorithms optimizing the reward function, or argue that the infinite limit abstraction is a reasonable approximation to the actual reality of RL algorithms.

I'd like to know which RL algorithms optimize the reward, and which do not.
An Opinionated Evals Reading List
by Marius Hobbhahn — 2024-10-15T14:38:58.778Z
Link: https://www.apolloresearch.ai/blog/an-opinionated-evals-reading-list

While you can make a lot of progress in evals with tinkering and paying little attention to the literature, we found that various other papers have saved us many months of research effort. The Apollo Research evals team thus compiled a list of what we felt were important evals-related papers. We likely missed some relevant papers, and our recommendations reflect our personal opinions.

Our favorite papers

Evaluating Frontier Models for Dangerous Capabilities

(Phuong et al., 2024)

Contains detailed descriptions of multiple LM agent evals across four categories. Also explores new methodologies for estimating evals success probabilities.
We think it is the best “all around” evals paper, i.e. giving the best understanding of what frontier LM agent evals look like
We tested the calibration of their new methodologies in practice in

Hojmark et al., 2024

, and found that they are not well-calibrated (disclosure: Apollo involvement).

Observational Scaling Laws and the Predictability of Language Model Performance

(Ruan et al., 2024)

They find that it is possible to find a low-rank decomposition of models’ capabilities from observed benchmark performances. These can be used to predict the performance of bigger models in the same family.
Marius: I think this is the most exciting “science of evals” paper to date. It made me more optimistic about predicting the performance of future models on individual tasks.

The Llama 3 Herd of Models

(Meta, 2024)

Describes the training procedure of the Llama 3.1 family in detail
We think this is the most detailed description of how state-of-the-art LLMs are trained to date, and it provides a lot of context that is helpful background knowledge for any kind of evals work.

Discovering Language Model Behaviors with Model-Written Evaluations

(Perez et al., 2022)

Shows how to use LLMs to automatically create large evals datasets. Creates 154 benchmarks on different topics. We think this idea has been highly influential and thus highlight the paper.
The original paper used Claude-0.5 to generate the datasets, meaning the resulting data is not very high quality. Also, the methodology section of the paper is much more confusingly written than it needs to be.
For an improved methodology and pipeline for model-written evals, see Dev et al., 2024 or

ARENA chapter 3.2

(disclosure: Apollo involvement).

Evaluating Language-Model Agents on Realistic Autonomou

...
Anthropic rewrote its RSP
by Zach Stein-Perlman — 2024-10-15T14:25:12.518Z

Canonical linkpost: https://www.lesswrong.com/posts/Q7caj7emnwWBxLECF/anthropic-s-updated-responsible-scaling-policy.

Anthropic's new version of its RSP is here at last.

Today we are publishing a significant update to our Responsible Scaling Policy (RSP), the risk governance framework we use to mitigate potential catastrophic risks from frontier AI systems. This update introduces a more flexible and nuanced approach to assessing and managing AI risks while maintaining our commitment not to train or deploy models unless we have implemented adequate safeguards. Key improvements include new capability thresholds to indicate when we will upgrade our safeguards, refined processes for evaluating model capabilities and the adequacy of our safeguards (inspired by safety case methodologies), and new measures for internal governance and external input. By learning from our implementation experiences and drawing on risk management practices used in other high-consequence industries, we aim to better prepare for the rapid pace of AI advancement.

Summary of changes.

Initial reactions:

ASL-3 deployment mitigations have become more meta — more like we'll make a safety case. (Compare to original.) (This was expected; see e.g.

The Checklist: What Succeeding at AI Safety Will Involve

.

) This is OK; figuring out exact mitigations and how-to-verify-them in advance is hard.

But it's inconsistent with wanting the RSP to pass the LeCun test — for it to be sufficient for other labs to adopt the RSP (or for the RSP to tie Anthropic's hands much). And it means the procedural checks are super important. But the protocol for ASL/mitigation/deployment decisions isn't much more than CEO and RSO decide. A more ambitious procedural approach would involve strong third-party auditing.

I really like that Anthropic shared "non-binding descriptions of [their] future ASL-3 safeguard plans," for deployment and security. If you're not going to make specific object-level commitments, you should totally still share your plans. And on the object level, those planned safeguards tentatively look good.

The new framework involves "preliminary assessments" and "comprehensive assessments." Anthropic will "routinely" do a preliminary assessment: check whether it's been 6 months (or >4x effective compute) since the last comprehensive assessment, and if so, do a comprehensive assessment. "Rout...
[Intuitive self-models] 5. Dissociative Identity (Multiple Personality) Disorder
by Steven Byrnes — 2024-10-15T13:31:46.157Z

5.1 Post summary / Table of contents

Part of the Intuitive Self-Models series.

Dissociative Identity Disorder (DID) (previously known as “Multiple Personality Disorder”) involves a person having multiple “alters” (alternate identities), with different preferences and (in some cases) different names. A DID diagnosis also requires some nonzero amount of “inter-identity amnesia”, where an alter cannot recall events that occurred when a different alter was active. For example, DSM-V talks about patients “coming to” on a beach with no recollection of how they got there.

Anyway, just like trance in the previous post, DID was one of those things that I unthinkingly assumed was vaguely fictional for most of my life. Maybe that’s because my only exposure to it was in actual fiction. While the artistic merit of these fictional DID depictions spanned a broad range—from the highs of Fight Club to the oh-so-very-low lows of Me, Myself & Irene—the psychological merit was uniformly crap.

And again like trance in the previous post, my take now is that DID does in fact exist. Even the memory lapses are real, although calling them “amnesia” is an oversimplification of something more nuanced. These people aren’t just trolling us. And in light of this series (especially Post 3), my explanation for DID is the obvious one: each different “alter” (“alternate identity”) in DID corresponds to a different “homunculus” concept in the intuitive self-model.

This explanation has a lot of overlap with trance. In fact, according to DSM-V, in cultures that have spirit-possession trance rituals, DID tends to manifest as that same kind of spirit possession. What makes DID different is that the trance states are recurrent and involuntary, rather than only happening in the appropriate ceremonial context.

Seems simple, but fleshing it out will involve a lot of subtle details!

Section 5.2 talks about how the suggestion of culture and psychologists is a risk factor for DID. I argue that this is naturally expected given the discussion of probabilistic inference in §1.2, and does not imply that the condition isn’t “real”.
Section 5.3 offers an explanation of why DID strongly correlates with Borderline Personality Disorder (BPD): we all have the everyday distinction between angry-me, happy-me, sad-me, etc. These are not normally DID—they all involve the same homunculus

...