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

COPRA: An in-COntext PRoof Agent which uses LLMs like GPTs to prove theorems in formal languages.

The official Python library for the OpenAI API

White-box automation for Lean 4

LLMs as Copilots for Theorem Proving in Lean

SGLang is a structured generation language designed for large language models (LLMs). It makes your interaction with models faster and more controllable.

LLM verified with Monte Carlo Tree Search

Efficient implementations of state-of-the-art linear attention models in Pytorch and Triton

Named Tensors for Legible Deep Learning in JAX

A collection of resources and papers on Diffusion Models

A high-throughput and memory-efficient inference and serving engine for LLMs

DSPy: The framework for programming—not prompting—foundation models

Gaussian processes in JAX.

Betty: an automatic differentiation library for generalized meta-learning and multilevel optimization

DialOp: Decision-oriented dialogue environments for collaborative language agents

An environment for learning formal mathematical reasoning from scratch

Loopy belief propagation for factor graphs on discrete variables in JAX

A library for differentiable nonlinear optimization

Dynamic Programming Volume 1

Some teaching material and other educational resources

An easy to use, fast extensible effects library with seamless integration with the existing Haskell ecosystem.

Soufflé is a variant of Datalog for tool designers crafting analyses in Horn clauses. Soufflé synthesizes a native parallel C++ program from a logic specification.

Kakoune Language Server Protocol Client

A demo implementation of a simple dependently-typed language

🍜 A tasty Haskell front-end framework

Data and code for the ICLR 2023 paper "Dynamic Prompt Learning via Policy Gradient for Semi-structured Mathematical Reasoning".