bmc7505

My hunch is that CDCL is probably the wrong approach to take for parallelization due to synchronization issues. You want an algorithm that is communication-free or makes belief propagation wall-clock competitive for large set of instances. It should be possible to modify BP to be asymptotically complete by using a special-purpose PRNG that ensures samples are drawn uniformly without replacement from the search space, but I'm not sure how to make it more sample-efficient.

Interesting. Do you have a link where I can read more about that? How does this relate to k-SAT or CNF complexity, isn't UP is complete w.r.t. these problems?

The 2^n idea is just a thought experiment, but you should be able to realize linear or close-to-linear speedup using a communication-free algorithm that shards the search space evenly across available cores, no? I don't see why this strategy isn't more widely used.

I can see how continuity accelerates the search for solutions, but I see that more as an orthogonal property, not a limitation of parallelism. Even if your domain is continuous, accelerating gradient descent is nontrivial, and many discrete optimizations problems benefit from parallelism.

Oh you're one of the GPUShareSat guys, I forgot about that one. Would you say the main obstacle to scaling to a million processors is the synchronization overhead or are there certain instances from the SATComp benchmark that exhibited poor scaling with increased parallelism? Do you think sharing is essential or do you have any ideas how to improve communication-free strategies, i.e., parallelism without clause sharing using divide-and-conquer or randomized search? Six years ago, your co-author Mate wrote a very pessimistic remark on GPU-based SAT solvers here [1], I'm curious whether he still believes this or if his option was changed during the course of the project and what changed his mind? Thanks!

[1]: https://news.ycombinator.com/item?id=13667565

That’s SATComp, I was talking about the MAXSAT competition.

> SAT doesn’t exhibit the nice properties other optimization problems often have where you can tell when you’re near a correct answer.

You mean like a metric? Not all SAT instances have a natural metric, maybe a large fraction could be relaxed to MAXSAT, but it seems parallel solvers are not very popular in that setting either, i.e., there is no parallel track and parallel solvers are disqualified [1] from participating.

I'm not sure I follow how metrics are related to parallelism though. A naive strategy would be to try every assignment in parallel on 2^n processors. There are plenty of better strategies for search space splitting [2] and stochastic local search [3] algorithms that seem amenable to parallelization.

[1]: https://maxsat-evaluations.github.io/2023/rules.html

[2]: http://sat.inesc-id.pt/~ruben/papers/martins-ictai10-talk.pd...

[3]: https://link.springer.com/article/10.1023/A:1006350622830

I was thinking there might be some theoretical barrier to parallelization, e.g., maybe naturally-arising SAT instances have poor empirical scaling constants [1], so sequential solvers with good branch heuristics are pretty close to optimal. There are some portfolio solvers (e.g., [2]) that have shown modest, but not dramatic speedups. Or maybe we just haven't tried hard enough.

[1]: https://en.wikipedia.org/wiki/NC_(complexity)

[2]: https://baldur.iti.kit.edu/hordesat/files/horde.pdf

And yet, despite tremendous progress accelerating continuous optimization workloads, there are still no competitive GPU-based SAT solvers. I wonder why?

There were number of innovative but relatively obscure languages that came out of the first wave of cybernetics. Glushkov, one of Lyapunov's contemporaries, created a language called Analytik [1], with early support for linear algebra and symbolic differentiation. REFAL is another language that emerged during the same era and still under active development [2]. At its foundation is an alternative and surprisingly rich algebraic theory of computation based on abstract rewriting systems and so-called word problems [3].

[1]: https://link.springer.com/content/pdf/10.1007/BF01070461.pdf

[2]: https://github.com/bmstu-iu9/refal-5-lambda

[3]: https://en.wikipedia.org/wiki/Word_problem_for_groups

You asked about my beliefs and I engaged your question in good faith. Good day, Sebastian!

Although I think their hearts are in the right place, AI safety researchers are primarily driven by irrational instincts and misjudge the promise and perils of artificial intelligence. If humanity chooses to turn away from God and sacrifice each other worshipping false idols, that will be our fault alone, whether or not the technology exists to hasten our demise.

We do have thousands of Einsteins today wielding untold resources, but the slowing pace of scientific progress suggests there are limits to scaling intelligence. Even with a hundredfold increase in scientists, I am unconvinced that would lead to a meaningful increase in social progress and have come to believe the bottlenecks we face are not due to a lack of intelligence, but a lack of other virtues (e.g., kindness, curiosity, courage, compassion, perseverance).

The problems that AI will manifest are the result of human ambition and failings, no different as any other technology that empowers individuals. Yes, individuals and organizations will misuse AI for immoral purposes, but the popular belief that AI is inherently antihumanist launders accountability by pretending to remove human agency from the equation. How we use or misuse AI technology is entirely on us.

Furthermore, I would argue there are strong complexity-theoretic bottlenecks to computational processes which limit the expressive power of neural networks, even if they could harness galactic amounts of energy. Physical Turing machines have bottlenecks that upper-bound the power of oracles.

It’s a LARP at best and a scam at worst. I shared some of my thoughts on the matter in a prior thread: https://news.ycombinator.com/item?id=35145189#35147288

I am disappointed with increasing frequency to learn how certain individuals whom I previously believed to be serious scholars fall for the cargo cult of AI safety. Personally I find it difficult to believe they are willfully participating in such conartistry, and makes me question their views on other subjects. Although I suppose intelligence and gullibility can coexist and some forms of delusion are better pitied than scorned.

My great-grandfather also perished in a mine collapse near Wilkes-Barre, PA, sometime in the 1920s. I remember my grandfather, who was still a child when it happened, telling me about how the miners were treated. He was forced to take a job selling fruit to support his mother and brother because the mining company refused to pay any death benefits. It's easy to forget how bad the working conditions once were, and I suppose still are in some places today.

Relevant: https://www.cidrdb.org/cidr2022/papers/p17-blacher.pdf

With arbitrary-precision, you can essentially replace the entire neural network with a single trainable parameter. [1] Likewise, in model checking, one often uses bounded-length bitvectors, because even a PDA with two stacks is Turing-equivalent. The poor separability between theoretical and physically-realizable models of computation is one of the weaknesses of the Chomsky hierarchy and classical approximation theory, and why more descriptive theories to characterize function complexity, e.g., circuit complexity, algebraic complexity theory and/or logical expressivity, are often needed.

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

See Merrill & Sabharwal (2023) [1]:

  A transformer N is a specific kind of a computation graph family over vectors of floating-point numbers with p precision. We work with fixed-precision transformers, i.e., we take p to be constant with respect to the input sequence length n. In practice, transformers typically use p = 32, and, several newer, larger transformer language models use p = 16 (Brown et al., 2020; Zhang et al., 2022), even while allowing larger context lengths n than their predecessors.

[1]: https://arxiv.org/pdf/2210.02671.pdf#page=7

@dang The title should be changed from MILA to Mila/IQIA.

Sören Laue, creator and first author of this work [1] gave a nice talk [2,3] about it at our reading group not long ago. He also has written about how automatic and symbolic differentiation are essentially equivalent. [4]

[1]: https://papers.nips.cc/paper/2018/file/0a1bf96b7165e962e90cb...

[2]: https://www.youtube.com/watch?v=IbTRRlPZwgc

[3]: https://compcalc.github.io/public/laue/tensor_derivatives.pd...

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

I found this book browsing through a cousin's bookshelf as an early teenager, and thereafter it left a lasting impression on me. The idea of a bidirectional communication link with a two-dimensional world and its strangely endearing inhabitants stuck with me ever since, and subconsciously I believe, influenced me to study computer science. I know previous authors have explored similar themes, but the idea and its execution are so carefully and creatively illustrated. What's fascinating is how many of those ideas are now being realized with cellular automata, computer games, and thinking machines.

You could have, the creature would just need a pair of zippers that unzip and zip the digestive tract as materials pass through, a bit like RNA polymerase unwinds and rewinds a strand of DNA. The zipper's teeth could act as conduits for the nervous and circulatory systems.

There is a similarly-themed short story by Liu Cixin, author of “The Three Body Problem”, called “The Poetry Cloud” [1, 2].

[1]: https://en.wikipedia.org/wiki/The_Poetry_Cloud

[2]: https://www.cuhk.edu.hk/rct/pdf/e_outputs/b7778/v7778p087.pd...

In classroom settings, slides are a poor local optimum. Personally I feel that professors rely on slides too heavily and would strongly them to use chalk. Writing in real-time forces you to teach at the pace of human thought.

This also allows students to take notes and actually absorb the material - otherwise, there is a tendency to pack too much into slides and you end up loosing half your audience. Although sometimes helpful for giving visual intuitions, more often than not, slides just get in the way.

When there really is no alternative to slides (e.g., for workshops and conference presentations), I find LaTeX/Beamer much easier to handle. It has good defaults and does not require fiddling with transitions and formatting and superficial but ultimately pointless settings.

Fun fact: CZ is an alumnus of McGill University! Before he became a cryptocurrency tycoon, he was working on an EdTech platform called Classroom 2000. [1, 2] Maybe if he had devoted as much energy to replacing PowerPoint as fiat, we would have better presentation technology today.

[1]: https://www.mcgill.ca/engineering/files/engineering/cv.pdf#p...

[2]: https://www.cc.gatech.edu/fce/c2000/overview/

Monumental achievement, but what's really extraordinary here is that this monograph is completely written/illustrated/typeset using LaTeX. Can't even begin to imagine how much effort this took.

Not quite, but close. True words are formidable things and some shapes are just whirlygigs. It's more like, are you building or just performing?

  Those two branches despise each other with intense passion.

I never actually made this connection before, but having spent far too much time listening to both camps, this observation does ring true. Another observation I had is that there is an orthogonal axis to the safety/ethics dichotomy that follows a more scholastic approach, namely neuro/symbolism. These two branches correspond, roughly, to the debate between machine learning and mechanized reasoning (a.k.a. good old fashioned AI).

Vastly oversimplifying, the neural branch believes reasoning comes after learning and that by choosing the right inductive biases (e.g., maximum entropy, minimum description length), then training everything up using gradient descent, reasoning will emerge. The symbolists place a heavier emphasis on model interpretability and believe learning emerges from a logical substrate, albeit at a much higher level of abstraction.

Like safety/ethics "research", neural/symbolic folks are constantly bickering about first principles, but unlike their colleagues in the S/E camp (which is at best philosophy and at worst fanfiction), N/S debates are resolved by actually building things like language models, chess bots, programming languages, type theories and model checkers. Both are valid debates to have, but N/S is more technically grounded while S/E is a bit like LARPing.

I enjoyed your writing, but disagree with your premise that creationism and the steady-state model are at odds. In fact, Lemaître was opposed to mixing science with religion and insisted the two were never in conflict. Whether the universe originated from a primeval atom (Lemaître's words) or is a Poincaré recurrence is completely orthogonal to Voltaire's question of the watchmaker - regardless whether time is cyclic or not still leaves open the question of why there is a clock to begin with, instead of nothing at all? The mechanics of the clock are mostly immaterial.