bmc7505

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

Hi, author here. Would you mind sharing which browser and version you are using? Thanks.

I guess I was thinking more of multithreading as an umbrella term for parallelism but I see your point. If you squint, SIMD and multithreading are the same problem. What I mean is, if you have a computable function you want to evaluate on a finite amount of bits, the problem of how to physically layout and schedule the computation to minimize latency is very similar to maximizing throughput.

From a circuit complexity standpoint, you could evaluate a wide but shallow circuit to evaluate the function in a nanosecond, or a deep but narrow circuit that takes eons. Whether parts of that circuit are evaluated synchronously or asynchronously is immaterial, although synchronous computation does seem easier to reason about and the UX is more user-friendly from a programmability standpoint.

I agree with you the fundamental limitation is the speed of light if you are width-bounded (i.e., if physical space is the dominating constraint).

Well, yes. But assuming the question is how to reduce overall latency, what alternative is there besides algorithmic improvements or increasing clock frequency?

I mean why isn’t multithreading the answer?

Care to elaborate?

Curves need not be smooth, for example we may consider elliptic curves over finite fields [1] or space-filling curves [2]. In general, there are various ways to generalize the notion of curvature to discrete structures like graphs and programs [3] which reflects our intuitive understanding about local curvature on smooth manifolds. For example, one way to view discrete curvature is to grow a ball around a point and look at how quickly its volume deviates from a ball of the same radius embedded in a uniformly connected graph approximating a “flat” or Euclidean space.

[1]: https://en.wikipedia.org/wiki/Elliptic_curve#Elliptic_curves...

[2]: https://en.wikipedia.org/wiki/Space-filling_curve

[3]: https://www.maths.dur.ac.uk/users/norbert.peyerimhoff/peyeri...

How would you access the source code of an encrypted program after copyright expiration if the author is dead and gives no one the keys? You might be thinking of public domain?

Nope. I support open source and personally release all my work in the open, but also support authors' freedom to distribute their own work however they wish and users' freedom to choose between them. These are fully consistent views.

I am a firm believer in open source, with the caveat that authors should always and everywhere have ultimate say over how to release their own work, never legislators or courts. FOSS may be the morally and technically preferable choice for many projects but is not inherently superior, and there are several advantages to going proprietary - plenty of examples where paid software is actually higher quality, regardless of whether it is developed in the open. This is also likely to be the case with ML software. If you want nice things then pay for them, but ultimately authors should be able to retain full creative freedom and executive control over their own software and let the marketplace decide.

They would be foolish not to at least try, either by intercepting entropy-supplying syscalls or compromising the hardware directly. RNG attacks are easy to design and nearly impossible to detect.

https://en.wikipedia.org/wiki/Yao%27s_test

You also need some kind of beam search or rejection sampling since JSON tokens to not exactly correspond to logits.

edit: They describe this more carefully in the paper.

Not sure why you are getting downvoted, as I believe there is a kernel of truth to what you are saying. Although I am sympathetic to the idealist position, based on what we know today about computers, I have come to believe that the thing some would call mathematics today is not grounded in reality. Whenever mathematics departs from reality, it leads those who practice it down a path that ends with insanity.

In the same way that psychology can be harmful to the pursuit of truth, there is an evil or deformity in what pure mathematics represents (or became), as Cantor and Gödel both discovered trying to eliminate its paradoxes. Mathematics as practiced by, e.g., Leibniz and Euler, was much more interested in calculation, i.e., mechanization. It is this form of "mathematics", as the thing has come to be called, that should have been developed, instead of trying to axiomatize infinite sets, explain the continuum, or fix impredicativity.

But despite the many paradoxes of mathematics (e.g., AoC, LEM) and machines (i.e., bugs), computer science has happily chugged along and made many practical contributions which explain the universe and shed light into people's minds, fulfilling the role that pure mathematics once served. Today, we are very close to mechanizing both minds and mathematics, and can replicate many aspects of reality (i.e., mathematical or otherwise) inside computers. It is not unimaginable that one day, computer science as it is practiced today will be seen as a kind of telescope for revealing the nature of mathematics and/or reality, which the mind alone cannot fathom.

Another related thread from last month: https://news.ycombinator.com/item?id=36084461

The current generation of LLMs will never generalize on problems whose expected complexity is significantly harder than the training set. One way to think of why this is the case is because transformers are learning shortcuts to multistep reasoning tasks [1, 2], but do not learn to reason systematically and unsurprisingly fail to generalize when presented with more challenging tasks.

The proper way to evaluate systematic reasoning is by training on a curriculum of problems of increasing average-case complexity. Think random k-SAT in the critical region, bisimulation games, or interpolation in certain logical theories. Although there is a growing evidence that Transformers and GNNs have foundational limits to expressivity [3, 4, 5], if the scaling crowd could show strong generalization results on these sorts of problems they would have the last laugh...

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

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

[3]: https://arxiv.org/pdf/2106.16213.pdf

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

[5]: https://arxiv.org/pdf/2303.04613.pdf

This is what happens when your objective function is to generate plausible or well-aligned next-word predictions - the model will converge on agreeable nonsense that sounds credible but is increasingly divorced from the truth. RLHF is a lousy patch to fix this problem. The real solution to grounding LLMs is by training it on hard-to-solve but easy-to-verify (i.e., NP-complete / hard-on-average problems), then formally verifying the generated outputs. While this may be difficult for prose, by including a large amount of training data containing formal reasoning tasks and programmatic text, this puts a strong bias towards correctness.

I was skeptical, but it turns out you're right! According to Wikipedia, the Northernmost point in California is 42 degrees north, and the Southernmost point in Canada is Middle Island, which is 41.7 degrees north [1], or about 0.3 degrees farther south of the Northernmost point in California.

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

[2]: https://en.wikipedia.org/wiki/List_of_extreme_points_of_U.S....

It can be done for fixed-length lists. Optimal sorting networks [1] are an active research topic with many interesting connections to differentiable sorting and ranking [2].

[1]: https://en.wikipedia.org/wiki/Sorting_network#Optimal_sortin...

[2]: https://arxiv.org/abs/2105.04019

Isn't CZ already being sued by the CFTC? Is cryptocurrency a security or a commodity and under whose jurisdiction does Binance fall? Or were they trading in both types of instruments?

https://news.ycombinator.com/item?id=35327996

Just gotta keep on trucking. Either way, I would be interested in seeing how the 2XSAT reduction works. Don't get discouraged!

Is superoptimization related to supercompilation, or are these unrelated compiler optimization techniques? From what I have read, it seems like Turchin [1] et al. are trying to prove equality using some sort of algebraic rewriting system (i.e., the "intensional" approach), whereas superoptimization uses an extensional technique to first try proving disequality by testing on a small set of inputs, then applies formal verification to the remaining candidates.

Massalin (1987) [2] calls the first phase "probabilistic execution" and claims that nearly all of the functions which pass the PE test also pass the more rigorous Boolean verification test. Can you give any insight into the benefits of TT over more "automated" optimizations? I am curious if MLTT/HoTT is more suitable for certain compiler optimizations or offers additional expressive power for proving equivalence, or is the benefit mostly ergonomics?

[1]: https://dl.acm.org/doi/pdf/10.1145/5956.5957

[2]: https://dl.acm.org/doi/pdf/10.1145/36177.36194

There is a qualitative difference in both perception and intent between a figure of speech, and a machine specifically designed to impersonate a human. Although we articulate familiar concepts in anthropomorphic terms, no reasonable listener would interpret these phrases literally. The former is simply a play on words, while the latter is a subliminal attempt to mislead users into humanizing a machine.

I have been making a similar argument for some time. The choice to anthropomorphize dialogue systems and large language models is a clichéd and misleading UI design choice. By presenting chatbots as disembodied persons, we are implicitly suggesting agency to an inanimate object, and subtly exploiting humans' social instincts into engaging with a system that is incapable of empathy. AI is best thought of as a programmable tool, not a conversational agent.

Thank you for the detailed reply, this is the first cogent answer I have read that explains why GPU solvers are not as widely used in SAT. The argument that we should focus on getting sequential solvers to run fast, then parallelizing that in hopes that it can be reused on each core does make sense, although I can't help but wonder if there isn't a smarter way to leverage parallelism than simply running CDCL in parallel on n-independent cores.

I guess if I were to summarize your argument, (current) solvers do not use GPUs because there are not many algorithms that can leverage the additional compute (and maybe there is some theoretical barrier?). On the other hand, the continuous optimization folks had neural networks for more than half a century before they figured out how to make them run fast, and were also ridiculed for pursing what was widely believed to be a dead-end. So I would be careful about falling for the "smart people tried really hard for a while" argument.

I remain skeptical. NC=P? is still an open conjecture, so there could be problems which are decidable in P, but only when using a polynomial number of processors or superpolynomial on a single processor, but polynomial on a polynomial number of processors. Furthermore, the amortized complexity of common instances could turn out to be tractable on average (e.g., random 3-SAT instances are tractable unless they fall in a very narrow region where the ratio of clauses to variables is ~4.25, but NP-complete in the worst case).

Isn’t UP complete with respect to CNF satisfiability though? How does P completeness relate to parallelizability of SAT?

It depends on the sharding granularity. If you choose a low sharding ratio, then you waste a whole core, but that's assuming 1:1 shards to cores. If you shatter the search space using a large multiple of the number of cores, e.g. 1000:1, then shuffle the shards and have each core pick a shard off the queue, if any core ever gets stuck with a bad shard (i.e., conflict), it discards and picks a new one off the queue. This requires no communication and ensures all cores stay hot. I guess you might also need some preprocessing to remove trivially-conflicting shards.

Using a naive splitting strategy is trivial, but ensuring the distribution is well-balanced across the subspaces is not. You need to preprocess the formula by setting the variables, then doing some propagation, then restarting, otherwise one core will get stuck doing a bunch of useless work.