Meta Lingua: a lean, efficient, and easy-to-hack codebase to research LLMs.

Benchmark LLMs by fighting in Street Fighter 3! The new way to evaluate the quality of an LLM

Grok open release

Fast & more realistic evaluation of chat language models. Includes leaderboard.

Retrieval-Augmented Theorem Provers for Lean

The official implementation of Self-Play Fine-Tuning (SPIN)

A concise but complete full-attention transformer with a set of promising experimental features from various papers

Implementation of the training framework proposed in Self-Rewarding Language Model, from MetaAI

[ICLR'24] RAIN: Your Language Models Can Align Themselves without Finetuning

The math library of Lean 4

A simulation framework for RLHF and alternatives. Develop your RLHF method without collecting human data.

[ACL 2024] Progressive LLaMA with Block Expansion.

🤗 The largest hub of ready-to-use datasets for ML models with fast, easy-to-use and efficient data manipulation tools

An open-source implementation of the AlphaGoZero algorithm

Sample implementations of proximal operators

A bagel, with everything.

The simplest, fastest repository for training/finetuning medium-sized GPTs.

Build better UIs faster.

An open platform for training, serving, and evaluating large language models. Release repo for Vicuna and Chatbot Arena.

An automatic evaluator for instruction-following language models. Human-validated, high-quality, cheap, and fast.

💧 Liquid Tensor Experiment

LLMs as Copilots for Theorem Proving in Lean

ChatGPT plugin for theorem proving in Lean

llmstep: [L]LM proofstep suggestions in Lean 4.

NaturalProver: Grounded Mathematical Proof Generation with Language Models

Lean 3's obsolete mathematical components library: please use mathlib4

A formalization of the concept of a perfectoid space in the Lean formal theorem prover.