bmc7505

  “breakthrough” is nothing more than an artifact of mathematicians not being able to properly specify the rules of their games in natural language… the theory of computer science has a culture that actively discourages running algorithms on a computer.

This is not an entirely faithful characterization. TCS and does make the distinction between galactic algorithms and what are called “feasible” algorithms (e.g., Karatsuba’s or Strassens’s algorithm), which yield a measurable speedup on practical inputs.

Cool to think this demo would have been possible over fifty years ago. I wonder what someone from 1975 would have said if you had shown this to them back then.

This topic recently came up at the FLANN workshop [1], and seems to periodically be rediscovered [2,3,4] in different contexts. While some have speculated about the biological role it plays (e.g., Pearlmutter & Houghton [5]), we still lack a conclusive theory of sleep, but the convergent evolution of this specific phenomenon across the animal kingdom and the fact that deprivation is inevitably fatal seems like an important clue.

[1]: https://flann.cs.yale.edu

[2]: https://www.cs.toronto.edu/~hinton/csc2535/readings/ws.pdf

[3]: https://arxiv.org/abs/1711.02282

[4]: https://arxiv.org/abs/2006.08381

[5]: https://mural.maynoothuniversity.ie/id/eprint/1653/1/Hamilto...

I've recently been using this plugin [1], which is still under development but is an adequate stopgap until a better solution comes along.

[1]: https://plugins.jetbrains.com/plugin/22150-noctule-the-swift...

As foretold six years ago. [1]

[1]: https://breandan.net/2020/06/30/graph-computation#roadmap

Fast matrix multiplication would be a more useful benchmark: https://fmm.univ-lille.fr/

17k TPS is slow compared to other probabilistic models. It was possible to hit ~10-20 million TPS decades ago with n-gram and PDFA models, without custom silicon. A more informative KPI would be Pass@k on a downstream reasoning task - for many such benchmarks, increasing token throughput by several orders of magnitude does not even move the needle on sample efficiency.

There are a few approaches if you want to write a new language. One, as the author argues, is to write a library in an existing language, which may require sacrificing ergonomics to fit inside the syntax of the host language, but is safe, modular and reusable.

Many DSLs can be bolted onto an existing language with support for compiler extensions. This approach offers more flexibility, but often leads to fragmentation and poor interoperability in the language ecosystem.

There is third approach, established by a group in Minnesota [1], which is to design languages and tools which are modular and extensible from the get-go, so that extensions are more interoperable. They do research on how to make this work using attribute grammars.

If the host language has a sufficiently expressive type system, you can often get away with writing a fluent API [2] or type safe embedded DSL. But designing languages and type systems with good support for meta-programming is also an active area of research. [3, 4]

If none of these options work, the last resort is to start from tabula rasa and write your own parser, compiler, and developer tools. This offers the most flexibility, but requires an enormous amount of engineering, and generally is not recommended in 2026.

[1]: https://melt.cs.umn.edu

[2]: https://arxiv.org/pdf/2211.01473

[3]: https://www.cs.tsukuba.ac.jp/~kam/papers/aplas2016.pdf

[4]: https://arxiv.org/pdf/2404.17065

Interesting. I wonder if mqjs would make it feasible to massively parallelize JavaScript on the GPU. I want to run thousands of simultaneously JS interpreters, each with an isolated heap and some shared memory. There are some research projects [1, 2] in this direction, but they are fairly experimental.

[1]: https://github.com/SamGinzburg/VectorVisor

[2]: https://github.com/beehive-lab/ProtonVM

You could argue that since automatic differentiation and symbolic differentiation are equivalent, [1] symbolic AI did succeed by becoming massively parallelizable, we just needed to scale up the data and hardware in kind.

[1]: https://arxiv.org/pdf/1904.02990

> The solvers participating in this track will be executed with a wall-clock time limit of 1000 seconds. Each solver will be run an a single AWS machine of the type m6i.16xlarge, which has 64 virtual cores and 256GB of memory.

For comparison, an H100 has 14,592 CUDA cores, with GPU clusters measured in the exaflops. The scaling exponents are clearly favorable for LLM training and inference, but whether the same algorithms used for parallel SAT would benefit from compute scaling is unclear. I maintain that either (1) SAT researchers have not yet learned the bitter lesson, or (2) it is not applicable across all of AI as Sutton claims.

The difference is that SAT/SMT solvers have primarily relied on single-threaded algorithmic improvements [1] and unlike neural networks, we have not [yet] discovered a uniformly effective strategy for leveraging additional computation to accelerate wall-clock runtime. [2]

[1]: https://arxiv.org/pdf/2008.02215

[2]: https://news.ycombinator.com/item?id=36081350

The correct way to do this is with finite model theory but we're not there yet.

Gingsberg stole it from Yeats — “the best lack all conviction…” / “the best minds of my generation…” — many similar verses, e.g., “what rough beast…” / “what sphinx of cement…”

https://www.poetryfoundation.org/poems/43290/the-second-comi...

Called it three years ago: https://news.ycombinator.com/item?id=30142353

Depending on how comfortable you are with model theory you might also enjoy Dzhafarov and Mummert’s textbook, which first brought the subject to my attention.

Although Wolfram doesn't mention it by name, this is closely related to what he is trying to do: https://en.wikipedia.org/wiki/Reverse_mathematics