joelburget

I wrote an OCaml implementation of this paper a few years ago, which I've now extracted into its own [repo](https://github.com/joelburget/constructive-reals/blob/main/C...)

The link in the paper to their Java implementation is now broken: does anyone have a current link?

And more recently, [Language Models Use Trigonometry to Do Addition](https://arxiv.org/abs/2502.00873)

This is a good idea, though one problem is that Einsum notation (as realized in Numpy and Pytorch) doesn't support the notion of co-contravariance, and the site is based on their Einsum notation. I could potentially add the variances for the examples, though that would move away from how the site currently works (where the information about the reduction comes only from the einsum input).

A couple of these I'd like references on if anyone happens to have them.

1. "current science suggests that the actual health impact from consuming most types of plastic might well be essentially zero"

2. "the (weak) evidence we have now suggests running strengthens your knees"

o1 is an application of the Bitter Less. To quote Sutton: "The two methods that seem to scale arbitrarily in this way are search and learning." (emphasis mine -- in the original Sutton also emphasized learning).

OpenAI and others have previously pushed the learning side, while neglecting search. Now that gains from adding compute at training time have started to level off, they're adding compute at inference time.

Vision Transformers do a shocking amount of compression in the tokenizer. In the [Chameleon paper](https://arxiv.org/pdf/2405.09818) they say the tokenizer "encodes a 512 × 512 image into 1024 discrete tokens from a codebook of size 8192". That's 256 pixels per token (512 * 512 / 1024). If we assume that a pixel is 24 bits (3x 8 bit channels), this implies that they've compressed 256 * 24 = 6144 bits into 13 = (log2(8192)). [An Image is Worth 32 Tokens for Reconstruction and Generation](https://yucornetto.github.io/projects/titok.html) pushes this even further. If these models work similarly, it's no wonder they struggle with some vision tasks.

Vision transformers should be our default guess as to how GPT-4o works, yet this article never mentions them.

It works on all human languages, just inefficiently. I ran it over a sample I found on wikipedia:

sample = "ฟองมันฟันหนู, ฟันหนูฟองมัน, ฝนทองฟองมัน" len(sample), len(enc.encode(sample))

This returns `39, 40` so it's just encoding one character at a time. It's probably like this for almost all non-English text.

A few interesting findings: * the cl100k_base tokenizer has ~100k tokens -- previous tokenizers had ~50k. (enc.n_vocab gives 100277 but some numbers in that range don't work, starting at 100256) * it has exactly 1110 tokens which are just digits. 10 1 digit tokens, 100 2 digit tokens and 1000 3 digit tokens! (none have preceding spaces). this is a huge improvement from GPT2's tokenizer, which was a huge mess. * there are <|fim_prefix|>, <|fim_middle|>, and <|fim_suffix|> tokens (see * Efficient Training of Language Models to Fill in the Middle)

The biggest news to me is the improved handling of numbers. This could explain some improved performance on arithmetic. One disappointment is that it tokenizes from the front*, e.g. "1000000" -> 100|000|0. This is one of those "so close!" moments -- I would work for free to fix this.

For those looking to run this on a Mac, the following seems to have worked for me (M1, Big Sur 11.2.3):

``` brew tap gcenx/wine brew install --cask --no-quarantine wine-crossover brew install winetricks winetricks corefonts vcrun6 vb5run native_oleaut32 vcrun2010 richtx32 comdlg32 comctl32ocx wine BookStory_en.exe ```

You have a keen eye -- thanks for the close reading.

Thanks for the heads up. It never occurred to me the svg might render differently. I'll see if we can fix this.

I'll use a bit of Haskell in my response, since that's what I'm most comfortable with and what we actually use for our work. Hopefully that's okay.

We can define a data type of expressions in our language, with addition, multiplication, etc.

  data Expr = Addition Expr Expr | Multiplication Expr Expr | ...

Then we need the type of an interpreter which consumes program inputs and produces an output. I'll leave this abstract for now.

  data Interpreter = ...

By map, we just mean that we can write a Haskell function with this type

  interpret :: Expr -> Interpreter
  interpret (Addition a b) = (+) <$> interpret a <*> interpret b
  interpret (Multiplication a b) = (*) <$> interpret a <*> interpret b

If you're curious, here's some real symbolic evaluation code I wrote doing the same https://github.com/kadena-io/pact/blob/234ba3dd01f0df8b4e462...

Stick around for part 2. We haven't gotten to the good stuff yet :)

Co-author here. We're planning to turn this into a series, with additional posts on how symbolic execution works at a lower level, how to present counterexamples to users, and ideas for future programming tools built on symbolic execution.

Similarly, I once wrote a triangular maze generator https://www.khanacademy.org/computer-programming/triangle-ma...