miniF2F
Formal to Formal Mathematics Benchmark (by openai)
dex-lang
Research language for array processing in the Haskell/ML family (by google-research)
| miniF2F | dex-lang | |
|---|---|---|
| 4 | 25 | |
| 256 | 1,538 | |
| 2.7% | 0.5% | |
| 0.0 | 8.8 | |
| 9 months ago | 2 days ago | |
| Objective-C++ | Haskell | |
| - | BSD 3-clause "New" or "Revised" License |
The number of mentions indicates the total number of mentions that we've tracked plus the number of user suggested alternatives.
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
miniF2F
Posts with mentions or reviews of miniF2F.
We have used some of these posts to build our list of alternatives
and similar projects. The last one was on 2023-02-11.
-
[D] Have their been any attempts to create a programming language specifically for machine learning?
That said, you *can* write down a desired type and have a system write down a ton of type annotations or generate a bunch of code to prove that the type you wrote down is satisfied by your program. There's been recent work on this in deep learning for theorem proving, such as this work which uses GPT for proving theorems in Lean, a dependently type programming language and theorem prover. A better approach though would be to combine this with an actual tree search algorithm to allow a more structured search over the space of proofs, instead of trying to generate full correct proofs in one shot. Hypertree Proof Search does this, using a variant of AlphaZero to search and fine-tune the neural net. Unfortunately it hasn't been open-sourced though, and it's pretty compute intensive, so we can't use this for actual type inference yet. But yeah there's active interest in doing this kind of thing, both as a proving ground for using RL for reasoning tasks and from mathematicians for theorem-proving.
- [D] First Author Interview: AI & formal math (Formal Mathematics Statement Curriculum Learning)
- [D] OpenAI tackles Math - Formal Mathematics Statement Curriculum Learning (Paper Explained Video)
- MiniF2F
dex-lang
Posts with mentions or reviews of dex-lang.
We have used some of these posts to build our list of alternatives
and similar projects. The last one was on 2024-01-13.
-
Thinking in an Array Language
A really nice approach to this I've seen recently is Google's research on [Dex](https://github.com/google-research/dex-lang).
- Function Composition in Programming Languages – Conor Hoekstra – CppNorth 2023 [video]
- Dex Lang: Research language for array processing in the Haskell/ML family
-
[D] Have their been any attempts to create a programming language specifically for machine learning?
Dex
-
[D] PyTorch 2.0 Announcement
Have you tried Dex? https://github.com/google-research/dex-lang It is in a relatively early stage, but it is exploring some interesting parts of the design space.
- Mangle, a programming language for deductive database programming
-
Looking for languages that combine algebraic effects with parallel execution
I think [Dex](https://github.com/google-research/dex-lang) might be along the lines of what you're looking for, although its focus is on SIMD GPU-style parallelism rather than thread-level parallelism.
-
“Why I still recommend Julia”
Dex proves indexing correctness without a full dependent type system, including loops.
See: https://github.com/google-research/dex-lang/pull/969
-
Haskell for Artificial Intelligence?
In case you want to see one research direction that's combining practical machine learning and functional programming, one of the authors of JAX (and the main author of its predecessor, Autograd) is writing Dex (https://github.com/google-research/dex-lang), a functional language for array processing. The compiler itself is written in Haskell. JAX is one of the most popular libraries for doing a lot of machine learning these days, along with Tensorflow and PyTorch. You might also want to see the bug in the JAX repo about adding Haskell support, for some context: https://github.com/google/jax/issues/185
What are some alternatives?
When comparing miniF2F and dex-lang you can also consider the following projects:
tensor_annotations - Annotating tensor shapes using Python types
jax - Composable transformations of Python+NumPy programs: differentiate, vectorize, JIT to GPU/TPU, and more
einops - Flexible and powerful tensor operations for readable and reliable code (for pytorch, jax, TF and others)
futhark - :boom::computer::boom: A data-parallel functional programming language
torchtyping - Type annotations and dynamic checking for a tensor's shape, dtype, names, etc.
julia - The Julia Programming Language
FL - FL language specification and reference implementations
Pytorch - Tensors and Dynamic neural networks in Python with strong GPU acceleration
jaxtyping - Type annotations and runtime checking for shape and dtype of JAX/NumPy/PyTorch/etc. arrays. https://docs.kidger.site/jaxtyping/
hasktorch - Tensors and neural networks in Haskell
CIPs