LLMs like even the sota flash models have great range of background math knowledge and have no problem reading and understanding flt level of math. On the other hand you don't want to go through 13 million lines of often repetitive code line by line. Models are great at synthesizing math content out of code. My contribution is to steer it through subjects of most interests to me, drill down into jargons that can be confusing, be creative in using computation for illustration (which coding agents can execute very proficiently) etc.
I enjoy learning math from LLM proofs with the help of LLMs https://github.com/htzh/flt_for_human . It is amazing how well models do when they are well grounded by formalized proof traces (even if created by other models).
Proofs are erasable. If you don't doubt it exists why do you care? Understanding is a side effect. Only people who want to understand the proof would need to care about it.
I don't think the truth of the theorem is ever in doubt so any attack would be silly. But the proof would enable tutorials like this: https://github.com/htzh/flt_for_human/blob/main/math/001-fre...
which would be hard to do without a proof outline as agents are not good at math per se, even though they are very knowledgeable and capable.
To really read the proof, clone the repo and drop the root index.html into your browser and enjoy. Due to the large amount of files in a directory Github won't serve the .lean files in Theorems/ beyond A. Github preview won't work with the htmls beyond the few top level docs either.
Nice to get some resonance. And if I may, past --> taste; vision --> future. And to compensate for our poor memory, taste<=>value network while vision<=>policy network, borrowing from RL parlance.
First I have to say this is sooner than expected, even though I never doubted that this could be done. I am grateful that they dedicated resources to accomplish this. It is clear that agents are very good at discerning and holding onto very weak signals from RL traing on long horizon tasks, so much so that in my own experience even very chaotic agent thinking can converge to meaningful solutions if there is a verifier. I have not dug through the proof yet so I don't know how readable it is to a human. But it has been a dream of mine to understand the FLT proof. I think LLMs will be a big part of making it truly accessible to humans.
Taste or vision? They are hill climbing and they can't see the other side. And sometimes that is because they don't live in your head and don't know what you want.
Linear layers use decays (like IIR filters) that naturally provide relative positions. Full attention layers can then be free to develop concepts that attend to each other regardless of distance.
That's not true. First there is still a licensing and quota scheme on the US side for the H200s. Secondly China blocked them for use in inferencing. Thirdly Chinese companies don't want them for training because newer chips are more cost effective.
Well, so far as the governments get VAT from the manufacturers, they are getting a return on their investments. They are more like mutualizing the companies than subsidizing them, that is the successful or mature ones are getting taxed to help the nascent ones.
Performance is generally limited by the process. Yield not so much. Assuming you can make it at a meaningful level at all, yield is generally a learning process.
Yield is generally not an issue over time, at least not as big as someone outside of the industry would think, if you get enough chips to work in the first place. For high volume chips, fabs will tune their process specifically for your chip over time. And you can do mask changes just to address yield problems and you can add redundancies if you have to. For example Huawei is no longer bottlenecked by the quantities of chips they can get for their handsets. Their problem is that they can't get the performance they could get with a better process.
What do you mean? Yield is a function of the chip size and density as well as the process. Plus it's a commercial secret so your bet can't be adjudicated.
Yes division is a poor example. It's a poor separation of concerns to try to wrap at this level without usage context. To see the point try to wrap overflows on arithmetic functions.
A lot of Chinese internet commentators are very ignorant of the reality in the US, but the Economist's riposte is weird too. For example how is the Chinese property malaise, which reflects an oversupply of housing and largely affordability of rent, somehow a refutation to the Chinese focusing on US homelessness? Is the Economist's position that they should create housing shortage to shore up the economy?
Price of a commodity metal can do whatever they want without causing a big problem. It is just a resource allocation signal. However if you base your currency value on it suddenly you are forcing debtors into bankruptcies if the value shoots up. Credit relationships aka investments are what make an economy run and grow, not some arbitrary commodity price.
Your point is right on. And additionally, why would an average Indian refuse the pay package to work in China? The top r&d guy at SMIC is from Taiwan after all. Liang got both Samsung and SMIC into the advanced nodes.
Humans are also not rewarded for making pronouncements all the time. Experts actually have a reputation to maintain and are likely more reluctant to give opionions that they are not reasonably sure of. LLMs trained on typical written narratives found in books, articles etc can be forgiven to think that they should have an opionion on any and everything. Point being that while you may be able to tune it to behave some other way you may find the new behavior less helpful.
I don't think people mind having bigger spaces but market is not clearing. In the US you have slums and bombed out building shells in prime urban locations as well. It is fascinating how human expectations work against each other.
Cheap housing isn't the problem. The problems are people speculating on the appreciation of property, banking system depending on property value as loan collaterals and local governments depending on property sales for revenue generation.
I don't think the repair could be done. It's not about plugging a hole in space. It's about surviving reentry. They can't guarantee the integrity of the glass. Anyway to your point they could stock the kits in space on regular supply missions, which again diminishes the utility of express delivery.
It has a fixed capacity of how many different things it can pay close attention to. If it fails on a seemingly less important but easy to follow instruction it is an indicator that it has reached capacity. If the instruction seems irrelevant it is probably prioritized to be discarded, hence a canary that the capacity has been reached.