The reason GPUs are used for NN computation is that they are massively parallel. You have hundreds or thousands of cores that perform the same operation on different parts of the network.
Tiny variations in the computational environment, such as slightly different set of processes running on the system as well as tiny differences in core temperature or voltage - among many other factors, can cause computations to complete in non deterministic order relative to each other.
This meaning one run eventually calculates a+b+c, whereas another does a+c+b, yielding slightly different results. Those cascade down the chain, resulting, finally, in a different set of produced logits.
Notably, similar effects can and do affect pure CPU calculations on multi core machines, and as a matter of fact even on a single core depending on the architecture when considering eg pipelining, branch prediction etc.
Thus, real world matrix operations are not, in fact, deterministic.
Now, one could argue that all of these are negligible, but that is an empirical claim dependent on the problem at hand.
> Jesus Christ, so many people here who have no clue what they are talking about.
Indeed. If only some of those people would see the irony.
What matters most of all, as any first year student of mathematics would know, is whether the formal problem statement corresponds to the NL statement. TFA specifically states that at least some of the allegedly proven formal statements DO NOT.
No. What the paper says is that in principle, translating NL statements to Lean statements is hard. Nobody doubts that, translating informal to formal text cannot be formally proven correct, so...
Does the paper give a single example of one of the OpenAI solved theorems with a Lean certificate where the Lean statement does not correspond to the actual statement from the mathematical literature? I don't think so, but in case I am wrong, feel free to provide that example.
> To demonstrate the effect of this result we provide
several examples of AI mistranslations of NL statements and proofs into Lean in practice, resulting in mismatches between NL proofs and their Lean ‘verifications’. These include OpenAI’s announced Navier-Stokes proof.
Could /I/ be mistranslating the paper’s formal statement to NL? I don’t think so, but in case I am wrong, feel free to cite the correct formal statement that they claim as divergent between Lean and NL formulations by OAI.
Yes, you are misunderstanding what the paper claims. Navier Stokes for example is not such an example, only the proof is different. For their other examples, none of them they claim that they concern actually the open ai solved theorems. You are welcome.
And yet I cited a specific statement made concerning N-S specifically, whereas all you’ve done is make patronizing remarks, and strawman arguments.
Have you actually read it? They give a handful of examples of mistranslations of both claims and proofs thereof, in relation to NS and Euler, though I do concede that they do not go as far as claiming outright the NS statement itself is mistranslated.
Unfortunately, lean proof alone is not enough. sidestepping the raging discussion regarding the meaning of mathematics, just because the lean compiles is not proof in itself that it is correct in the sense that mathematicians mean. Unless of course, you can prove that lean itself is correct, which you can’t.
we have seen “proofs” earlier this year that essentially abused some bugs in the kernel. it would be very convenient if every program written in rust was automatically correct if compiles - something i strongly suspect you believe - unfortunately, this is not the case for either.
In case you are not aware, the actual theorem statement of N-S was never translated by an LLM, but was written independently by formal conjectures, as they say in the README [1].
A Lean proof has a much higher probability of being correct (in my opinion) than any published (either preprint or peer-reviewed) paper, yet no one before LLMs were walking around claiming every result published can't be trusted yet (without an actual reason).
We have seen one such instance of Lean bugs, which was found adversely against Lean (as in find bug then use this bug to prove Collatz, not just found when being asked to prove it).
It's also worth to note that the way N-S (and all the other proofs by OpenAI etc) have been found is first prove it in NL then translate to Lean. I.e. it would have to first believe it found a correct proof in NL, and then afterwards either accidentally or on purpose use a Lean kernel bug.
edit:
Probably also worth to mention that the proof have been checked both by the Lean kernel and the independent nanoda kernel, so it would need to exploit bug(s) from both.
2. No exploit of a kernel soundness bug in Lean (and the independent kernel nanodo, which OpenAI also checks against).
In particular, if you trust this, then you don't need to care about anything else the Lean program does, no matter how many lines, lemmas etc. it makes along the way.
As I said above, the theorem statement have been written independently by formal conjectures, and you are free to read it yourself (or trust other people have done it).
So, assuming you don't disagree the theorem statement have been written correctly, you pretty much need to believe 2 is false, if you don't trust the proof [1]. And that's what I find has a rather low probability personally.
[1] As the book says, you also need to trust the hardware, firmware etc.
You may be overconfident here. The NL paper may be properly stating the Navier Stokes problem, and the Lean code may not be.
Here's from the paper--
3.1. When the NL paper declares stronger statements than what Lean proves
We commence with an example that complements those in §2. In the following example the AI autoformalisation results in a different Lean proof of a weaker statement.
None of the examples are of the NS lean statement. The validity of the latter is not under question ( in this paper ). Please note the distinction between “statement of NS” and “statement of lemmas used in the NL proof of NS”.
You seem to be vaguely waving in the general direction of a point, without making any concrete claims or bothering to engage with the GP’s argument.
The tastes and interests of humans are absolutely not arbitrary. They are dictated by fate, the sun and the moon gods. Or maybe by the unitary evolution of the universe’s quantum state. Or by the probability distribution of finding ourselves in a particular branch of the universe.
What bearing does this have on whether math is a collaborative endeavor?
And what is unique to math, that your argument wouldn’t apply equally to physics, sociology or financial markets? All, “truth seeking” disciplines.
You seem rather aggressive so replying to you feels pointless and uncomfortable.
Nonetheless, the person writes, “ Math has been almost purely arbitrary”.
This is simply a misusage of the word arbitrary, which is a word with a specific meaning you can look up if you are unaware, since mathematics is (obviously) not arbitrary in the sense this person wants to convey, in part for the reasons I state. Humans are not choosing arbitrary logical statements to prove true or false.
I don’t recall anything specific off the top of my head but I am confident that such a proof would have immediate actionable implications.
Furthermore, careful analysis of the latter would as likely as not yield further understanding and, actually /would/ help finding such algorithms.
Finally, it has been observed time and time again that often (again, nothing comes up and i don’t want to ask AI) the certainty that something is possible and has been done is motivation and inspiration enough for people to independently solve a problem. Sometimes it is even enough for someone new to simply not know that something is “hard” to solve.
Of course this is all pure speculation concerning a hypothetical proof that most likely doesn’t exist, or indeed might be so complicated as to not be approachable even after hundreds of lifetimes of study.
Nevertheless your conclusion does not follow from the premise
i know because i went through this.
reply