Stars
LeanArchitect extracts a blueprint directly from Lean source.
LeanHammer is an automated reasoning tool for Lean that brings together multiple proof search and reconstruction techniques and combines them into one tool.
HyperTree Proof Search for Neural Theorem Proving -- "La science est l'œuvre de l'esprit humain, qui est plutôt destiné à étudier qu'à connaître, à chercher qu'à trouver la vérité."
A banchmark list for evaluation of large language models.
Neural theorem proving toolkit: data extraction tools for Lean 4
Rigourous evaluation of LLM-synthesized code - NeurIPS 2023 & COLM 2024
KMD is a collection of conversational exchanges between patients and doctors on various medical topics. It aims to capture the intricacies, uncertainties, and questions posed by individuals regard…
We introduce MKQA, an open-domain question answering evaluation set comprising 10k question-answer pairs aligned across 26 typologically diverse languages (260k question-answer pairs in total). The…
Multilingual Large Language Models Evaluation Benchmark
llmstep: [L]LM proofstep suggestions in Lean 4.
Download, parse, and filter data PubMed, data-ready for The-Pile
Official Implementation of OCR-free Document Understanding Transformer (Donut) and Synthetic Document Generator (SynthDoG), ECCV 2022
jax-triton contains integrations between JAX and OpenAI Triton
Sea-Snell / JAX_llama
Forked from meta-llama/llamaInference code for LLaMA models in JAX
Large language models (LLMs) made easy, EasyLM is a one stop solution for pre-training, finetuning, evaluating and serving LLMs in JAX/Flax.
PyTorch extensions for high performance and large scale training.
🐙 OctoPack: Instruction Tuning Code Large Language Models
Ongoing research training transformer models at scale
Training and serving large-scale neural networks with auto parallelization.
A curated list of awesome papers related to pre-trained models for information retrieval (a.k.a., pretraining for IR).
some common Huggingface transformers in maximal update parametrization (µP)