bmc7505

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’m looking for a way to run thousands of simultaneous 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

This is roughly the intuition I have developed -- any computational function requires time and space to evaluate. Most computations carry with them some epistemic or aleatoric modeling uncertainty, but sometimes even a perfectly deterministic function with a worst case constant time complexity is worth approximating, as the constant factor may be prohibitive.

Given an exact decision procedure with astronomical lower bounds, and an approximate one that is identical on 99.99% of IID sampled inputs that takes a second to evaluate, which would you prefer? Given a low latency, high variance approximation, would you be willing to exchange latency for lower variance? Engineering is all about such tradeoffs.

There is a neat picture [1] in GEB that captures a similar idea.

[1]: https://miro.medium.com/v2/resize:fit:4800/format:webp/1*VU1...

FWIW, I’ve had a very similar encounter with another famous AI influencer who started lecturing me on fake automata theory that any CS undergrad would have picked up on. 140k+ followers, featured on the all the big podcasts (Lex, MLST). I never corrected him but made a mental note not to trust the guy.

This is a handy tool, but I wish it supported edge snapping. If you inspect the generated LaTeX it doesn't actually link up the FSM states, it just anchors them to raw TikZ coordinates.

The trick is not just synthesizing valid functions, but doing so in a parallel communication-free manner, without compromising soundness or completeness. You want to massively scale up a discrete sampler without replacement. One very efficient way of doing this is by constructing an explicit bijection from the sample space to the integers, sampling integers, then decoding them into programs.

While this technique enjoys certain advantages, i.e., it is embarrassingly parallelizable and guaranteed to enumerate distinct solutions with a bounded delay, it also somewhat unnatural. By flattening the distribution onto the integers a la Gödel numbering, it destroys locality, does not play well with incremental decoding methods (left-to-right is currently en vogue in generative language modeling), and will fail if the sample space is uncountable.

Another key step is reducing symmetries in your sample space by quotienting it somehow (e.g., by α-equivalence). The author seems to be invoking some kind of equivalence relation by “superposition”, but the technical details here are a little fuzzy.

This problem is also closely related to model counting in the CSP literature, so a practical speedup could lead to improvements on a lot of interesting downstream benchmarks.

In general, the problem of program induction from input-output examples is not well-posed, so specialized solvers that can make stronger assumptions will usually have an advantage on domain-specific benchmarks. Most existing program synthesizers do not satisfy all of these desiderata (e.g., soundness, completeness, naturalness, incrementality).

Maciej Bendkowski has some related work [1] on generating random lambda terms, but was unable to overcome what he calls the asymptotic sparsity problem:

  Sampling simply-typed terms seems notoriously more challenging than sampling closed ones. Even rejection sampling, whenever applicable, admits serious limitations due to the imminent asymptotic sparsity problem — asymptotically almost no term, be it either plain or closed, is at the same time (simply) typeable. [...] Asymptotic sparsity of simply-typed λ-terms is an impenetrable barrier to rejection sampling techniques. As the term size tends to infinity, so does the induced rejection overhead. In order to postpone this inevitable obstacle, it is possible to use dedicated mechanisms interrupting the sampler as soon as it is clear that the partially generated term cannot be extended to a typeable one. The current state-of-the-art samplers take this approach, combining Boltzmann models with modern logic programming execution engines backed by highly-optimised unification algorithms. Nonetheless, even with these sophisticated optimisations, such samplers are not likely to generate terms of sizes larger than one hundred.

I would be curious to see a more rigorous analysis of the sample complexity of generating well-typed expressions in, e.g., the STLC. Maybe there is a way to avoid or reduce the rejection rate before evaluation.

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

This is a very nice approach. Unfortunately, Piantadosi's pairing function does not work for acyclic grammars (i.e., finite CFLs). We found a variant that handles enumerating all trees of a certain width from an arbitrary CFG, i.e., L(G) ∩ Σ^n, or whose language is finite [1]:

[1]: https://github.com/breandan/galoisenne/blob/master/latex/laf...

It's coming! CMUSphinx used to have something like this, and there are some [1] solutions [2] on the horizon.

[1]: https://github.com/alphacep/vosk-api/issues/55

[2]: https://github.com/outlines-dev/outlines?tab=readme-ov-file#...

> All AI is written with Python.

Type error on line 3: “Python” is not a valid type for “all AI”.

A more charitable view is that a lot of research projects which seem like chmess to an outside observer become a lot more rational when properly contextualized. Often, the authors have justifications, ontological commitments or motivational factors for pursuing esoteric research that get lost in the writing process and only become apparent when familiar with the ambient conceptual framework.

Old enough to remember the days when Java reached near AI-level hype. Most of the advanced placement and undergraduate CS courses in the U.S. were taught in Java. There was an annual conference in San Fransisco called JavaOne/Oracle OpenWorld that rivaled the size of even NeurIPS, drawing tens of thousands of attendees each year. According to some statistics, there were 10 million Java developers and 3 billion devices running Java worldwide. I wonder what happened? Why does HN dislike Java so much?

edit: Someone should really take the time to highlight all the innovative machine learning research happening in Java. The original implementation of t-SNE [1] was written in Java. Most NLP researchers have heard of CoreNLP [2], also Java. One of the earliest ML libraries, Weka [3], was written in Java and is still actively developed at the University of Waikato. Noteworthy research on ML4Code specifically targets the Java language [4]. There's a bunch of published sketching algorithms for Java (e.g., DataSketches [5], t-digests, ddsketch et al.), featured in an invited talk [6] to NeurIPS this year. Just to name a few off the top of my head.

[1]: https://github.com/lejon/T-SNE-Java

[2]: https://github.com/stanfordnlp/CoreNLP

[3]: https://www.cs.waikato.ac.nz/ml/weka/

[4]: https://openreview.net/pdf?id=bUDmRzeh3PT

[5]: https://github.com/apache/datasketches-java

[6]: https://nips.cc/virtual/2023/events/Invited%20Talk

I assure you, the open source community around modern IDEs is thriving. I see plenty of innovation in plugin marketplaces that is hard to find in even the Emacs/Vim ecosystem. Despite its share of detractors, there is a lot of value in having a business model that prioritizes language support, platform stability and a well-curated plugin marketplace. The IdeaVim integration is thoughtfully designed and I seldom notice much difference coming from Vim. I see where you're coming from with resource consumption, but even Fleet is starting to offer rudimentary Vim support, which I expect will address many of the issues around bloat. [1]

[1]: https://youtrack.jetbrains.com/issue/FL-10664/Vim-mode-plugi...

The best part is, you don't need to choose between using IDEs and your favorite text editor! Most modern IDEs with proper plugin support can be configured to provide a superset of Vim's functionality. I personally use IdeaVim on the IntelliJ Platform [1] with AceJump [2] and haven't looked back. You can import many of the settings from your .vimrc and it interoperates fairly well with the IDE features. Although I prefer Vim keybindings and it is technically possible to hack together an IDE-like UX with ctags and LSP, the IDE experience is so much better I wouldn't even consider working on a large Java or Kotlin project from the command line.

[1]: https://plugins.jetbrains.com/plugin/164-ideavim

[2]: https://plugins.jetbrains.com/plugin/7086-acejump