No the meaning is that there's a wave of hardware innovators who started as software innovators. Musk (Paypal) is the most obvious example. The Boom CEO featured here is another. There's a fair bunch more, I agree with the author that a weirdly high % of founders of cool hardware / deeptech companies have a software engineering background. Like, you'd expect that space to be dominated by mechanical engineers, electrical engineers and physicists etc but somehow it isn't.
Because people who led software companies (which have insanely high margins) have access to the vast capital needed for serious heavy hardware development. They then hire the engineers they need to succeed.
Yep. I suspect they're also better at getting warm intros to and selling their vision to Silicon Valley CEOs than your average aerospace engineer with a dream.
But I suppose the bigger goal remains improving their language model, and this was an experimentation born from that. These works are symbiotic; the original DeepSeekMath resulted in GRPO, which eventually formed the backbone of their R1 model: https://arxiv.org/abs/2402.03300
The "obvious" thing to try, which presumably some people are trying pretty hard right now[1], is to (1) use a mathematically-tuned LLM like this one to propose informal Next Things To Try, (2) use an LLM (possibly the same LLM) to convert those into proof assistant formalism, (3) use the proof assistant to check whether what the LLM has suggested is valid, and (4) hook the whole thing together to make a proof-finding-and-verifying machine that never falsely claims to have proved something (because everything goes through that proof assistant) and therefore can tolerate confabulations from LLM #1 and errors from LLM #2 because all those do is waste some work.
[1] IIRC, AlphaProof is a bit like this. But I bet that either there's a whole lot of effort on this sort of thing in the major AI labs, or else there's some good reason to expect it not to work that I haven't thought of. (Maybe just the "bitter lesson", I guess.)
It would doubtless be challenging to get such a system to find large difficult proofs, because it's not so easy to tell what's making progress and what isn't. Maybe you need LLM #3, which again might or might not be the same as the other two LLMs, to assess what parts of the attempt so far seem like they're useful, and scrub the rest from the context or at least stash it somewhere less visible.
It is, of course, also challenging for human mathematicians to find large difficult proofs, and one of the reasons for them is that it's not so easy to tell what's making progress and what isn't. Another major reason, though, is that sometimes you need a genuinely new idea, and so far LLMs aren't particularly good at coming up with those. But a lot of new-enough-ideas[2] are things like "try a version of this technique that worked well in an apparently unrelated field", which is the kind of thing LLMs aren't so bad at.
[2] Also a lot of the new-enough-ideas that mathematicians get really happy about. One of the cool things about mathematics is the way that superficially-unrelated things can turn out to share some of their structure. If LLMs get good at finding that sort of thing but never manage any deeper creativity than that, it could still be enough to produce things that human mathematicians find beautiful.
Natural language is a lot more, well, readable than say lean. You get a lot less intuition and understanding of what the model is attempting to do in the first place.
Ok I guess I could have told you that. What I really meant is that in the future where LLMs are doing new math (which I'm skeptical of, but I digress) I would not trust any of it unless it was formally verified.
I think there's a lot of baggage doing it in lean. like what the libraries are at currently. how things are implemented. which things are not implemented, etc. but it still remains to be seen what wins (my money would be on informal)
Does anyone have a similar article with more detail? I don't quite want to read the datasheet of your favorite microprocessor, but I would like a decent amount more detail than what's provided. Especially before UEFI/BIOS.
At a very high level, the processor initialization procedure is similar to most microcontrollers:
- processor is powered up with RESET pin asserted, making sure that all circuits are in a known-safe state.
- when RESET is deasserted, all autonomous circuits (e.g. core control units, cache controllers, ALUs) go through a hardware setup phase.
- the processor accesses the boot firmware according to the platform design. There's many options here, but the three most common are 1) the boot ROM is permanently mapped to a dedicated hardware address, and the processor uses its memory controller to access that memory; 2) the boot ROM is directly connected to the processor via dedicated I/O pins; 3) the initial boot code is located on the processor itself (factory-programmed EEPROM).
- if the boot ROM is not mapped to a memory address, the data is loaded into CPU cache (external RAM needs to be initialized first, and that task is usually performed by the firmware).
- the primary cpu core starts executing boot code (UEFI/BIOS/etc) from said predefined hardware address. Other cores (and processors) are usually left uninitialized throughout the startup process, and it is left to the operating system to bring up the remaining parts of the system.
Rice's theorem is about decidability, not difficulty. But you are right that assuming P != NP there is no algorithm for efficient SAT (and other constraint) solving.
I'm surprised to hear this. Modern SAT solvers can easily handle many problems with hundreds of thousands of variables and clauses. Of course, there are adversarial problems where CDCL solvers fail, but I would be fascinated if you can find industrial (e.g. human written for a specific purpose) formulas with "dozens of variables" that a solver can't solve fairly quickly.
One thing that I spent a particularly long time trying to get working was learning near-minimum-size exact languages from positive and negative samples. DFAMiner [0] has a relatively concise formulation for this in terms of variables and clauses, though I have no way to know if some other reformulation would be better suited for SAT solvers (it uses CaDiCaL by default).
It usually starts taking a few seconds around the ~150-variable mark, and hits the absolute limit of practicality by 350–800 variables; the number of clauses is only an order of magnitude higher. Perhaps something about the many dependencies in a DFA graph puts this problem near the worst case.
The annoying thing is, there do seem to be heuristics people have written for this stuff (e.g., in FlexFringe [1]), but they're all geared toward probabilistic automata for anomaly detection and similar fuzzy ML stuff, and I could never figure out how to get them to work for ordinary automata.
In any case, I eventually figured out that I could get a rough lower bound on the minimum solution size, by constructing a graph of indistinguishable strings, generating a bunch of random maximal independent sets, and taking the best of those. That gave me an easy way to filter out the totally hopeless instances, which turned out to be most of them.
The original claim was to create a new programming language for developing games.
Everything that has come out of Verse so far has been "oh look, I designed this language I wanted to design and the only relation it has to gaming is the title of the paper"
We don't even know if it's a good programming language for anything, as it doesn't exist outside Unreal for Fortnite
Tim Sweeney & Epic are creating the language Verse whose logic functional underpinnings will make concurrency & correctness easier in Fortnite.
https://youtu.be/ub-dls31Pyw
What is this? I can't find easily the meaning of "bits to atoms." Is this meaning that US is going away from digital "exports"?