A short proof that LLMs (even o1) still can't reason:
Consider the problem of inverting a perfect binary tree. That's an old, entry-level interview question that humans and LLMs can solve easily. Now, let's add just 3 key nuances to make it new and unique:
1. It must invert *keys* ("bit-reversal permutation") 2. It must be a dependency-free, pure recursive function 3. It must have type `Bit -> Tree -> Tree`
These small changes are enough to move this problem out of the "memorized solution zone". It isn't on the internet. And, guess what? This is enough to make it completely intractable to modern AIs. All of them fail miserably at it, no matter how you prompt it.
This is very relevant, because the problem is still easy to a human researcher, and being capable of solving it is clear pre-requisite to contribute to CS research. Yet, all modern AIs fail miserably. As much as I love LLMs, truth is: they do NOT reason, and they will never do CS.
I'm willing to give $10k to anyone who shows any AI capable of implementing this function correctly. It just won't work, no matter how long it thinks. (The solution is 7 lines of code!)
guys please before posting a solution at least test it 😐
HVM is becoming the world's fastest λ-calculator! For a perspective, let's perform a Radix Sort on a Scott Tree with millions of ints, vs state-of-art runtimes:
How is that possible? See below ↓
Why HVM ran quicker
[ ] GPT-5 designed it
[ ] Different algorithms
[X] It used 12 cores 😬
HVM is NOT so fast in a single core (yet), but it can turn normal programs into multi-core executables for free, giving it a boost! But why would it work, when so many attempts failed?
Jan 4, 2023 • 4 tweets • 1 min read
Announcement time!
Over the last months, many asked what are our plans with HVM, Kind, Kindelia. I can finally answer that question: we're launching a tech startup! There is a lot to explain, but, for now, check our silly pitch preview:
github.com/VictorTaelin/H…
It is time to get out of the comfort zone and turn tech demos into products that solve real business problems. Personally, I have much to learn. But when I have a goal, I don't rest until I make it. My goal is to make this company thrive, and I'll be fully committed to it now.
Jan 3, 2023 • 16 tweets • 4 min read
Things I wish I had time to play with: Quantum Fourier Transform on Interaction Nets. QFT is the key component of Shor's algorithm (yes, the one that'd break all of crypto as we know it). Thing is, there is no proof this can't be achieved in a classical computer. I bet it can!
If there is one way to do it, interaction nets must play a role. On inets, mathematical elegance is the king of all optimizations, and modular exponentiation and repeated squaring are precisely the things that they do very elegantly. And that is deeply connected to primes & FFTs.
Dec 24, 2022 • 9 tweets • 2 min read
So, here is a provocative question, that nobody will be able to answer, but I'll ask anyway: if you had to design a type theory to be used exclusively by a computer, how it would look like? (details on the thread)
Specifically, the computer will use it to train its intelligence, trying to write proofs to random, AI-generated theorems. The checker would tell if the proof is correct or not, and that'll be used as the scoring function to train the AI.
Nov 4, 2022 • 22 tweets • 6 min read
Since I've been receiving a bunch of DMs asking what HVM, Kindelia and Kind are, and since it is still so early (we don't even have a pitch deck yet!), let me make some tweets to present our work, and a sneak peek on the crazy things we're building. *GIANT TECH THREAD INCOMING*
First, the origins: I'm a huge programming language theory nerd who spent years trying to understand "the true nature of computation". After trying every esoteric language imaginable, hacking λ-terms, and wondering why Haskell is such a slow λ-calculator, I found a curious paper.
