zhangir-azerbayev Goto Github PK

alphageometry

composer

doremi

Pytorch implementation of DoReMi, a method for optimizing the data mixture weights in language modeling datasets

dotfiles

config files, symbolically linked to correct locations

etk

Code for "Explicit Knowledge Transfer for Weakly Supervised Code Generation"

infinigen

Infinite Photorealistic Worlds using Procedural Generation

lean-chat

lean-chat-server

Server for lean-chat

lean-chat-vscode

lean-step-fork

Proof artifact co-training for Lean

levanter

Legible, Scalable, Reproducible Foundation Models with Named Tensors and Jax

llemma_formal2formal

Llemma formal2formal (tactic prediction) theorem proving experiments

llmstep

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

math_cc_net

Tools to download and cleanup Common Crawl data

mathematics_in_lean

The user home repository for the Mathematics in Lean tutorial.

mathlib-semantic-search

mathport

Experimenting with porting proofnet and minif2f

metagen

metagen-data

metagen-new

metamath

minif2f

Adding Lean 4

mizar-mirror

storing mizar files here to make them easy to access through the REST api.

mm-extract

Extracting human readable pre-training data from set.mm

nlp4code-experiments

nn-generalization

Neural Network Generalization Reading List

openwebmath

particle_filtering

Particle Filtering for Sequential Bayesian Inference

proof-pile

Scripts for downloading and pre-processing the `proof-pile`, a high quality dataset of mathematical text and code.

proofnet

Benchmark for undergraduate-level formal mathematics