Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Case study: Creative math – How AI fakes proofs

tomaszmachnik.pl

Post reply on HN
Print view View original

81–90 of 107 posts

Re: Case study: Creative math – How AI fakes proofs

#81

Post by seanmcdirmid »

embedding-shape wrote: post #63
seanmcdirmid wrote: post #49

Earlier quoted context omitted.

Yes, and better still the AI will fix its mistakes if it has access to verification tools directly. You can also have it write and execute tests, and then on failure, decide if the code it wrote or the tests it wrote are wrong, snd while there is a chance of confirmation bias, it often works well enough

> decide if the code it wrote or the tests it wrote are wrong Personally I think it's too early for this. Either you need to strictly control the code, or you need to strictly control the tests, if you let AI do both, it'll take shortcuts and misunderstandings will much easier propagate and solidify. Personally I chose to tightly control the tests, as most tests LLMs tend to create are utter shit, and it's very obvio…

I haven’t found that to be the case in practice. There is a limit on how big the code can be so it can do it like this, and it still can’t reliably subdivide problems on its own (yet?), but give it a module that is small enough it can write the code and the tests for it.

You should never let the LLM look at code when writing tests, so you need to have it figure out the interface ahead of time. Ideally, you wouldn’t let it look at tests when it was writing code, but it needs to tell which one was wrong. I haven’t been able to add an investigator into my workflow yet, so I’m just letting the code writer run and evaluate test correctness (but adding an investigator to do this instead would avoid confirmation bias, what you call it finding a loophole).

Re: Case study: Creative math – How AI fakes proofs

#82

Post by esafak »

dns_snek wrote: post #61
esafak wrote: post #43

Earlier quoted context omitted.

What do you make of human failures to reason then?

Humans who fail to reason correctly with similar frequency aren't good at solving that task, same as LLMs. For the N-th time, "LLM is as good at this task as a human who's bad at it" isn't a good selling point.

You didn't claim that such humans fail to "reason in our sense of the word". Why are you not holding them up to the same standard?

Re: Case study: Creative math – How AI fakes proofs

#83

Post by dns_snek »

esafak wrote: post #82
dns_snek wrote: post #61

Earlier quoted context omitted.

Humans who fail to reason correctly with similar frequency aren't good at solving that task, same as LLMs. For the N-th time, "LLM is as good at this task as a human who's bad at it" isn't a good selling point.

You didn't claim that such humans fail to "reason in our sense of the word". Why are you not holding them up to the same standard?

I didn't but I'm happy to make that claim - humans who exhibit that sort of behavior aren't reasoning either, and they are just as unpleasant to deal with as LLMs are.

Re: Case study: Creative math – How AI fakes proofs

#85

Post by cindyllm »

dns_snek wrote: post #61
esafak wrote: post #43

Earlier quoted context omitted.

What do you make of human failures to reason then?

Humans who fail to reason correctly with similar frequency aren't good at solving that task, same as LLMs. For the N-th time, "LLM is as good at this task as a human who's bad at it" isn't a good selling point.

[dead]

Re: Case study: Creative math – How AI fakes proofs

#86

Post by arational »

musculus wrote: post #72
comex wrote: post #40

I like how this article was itself clearly written with the help of an LLM. (You can particularly tell from the "Conclusions" section. The formatting, where each list item starts with a few-word bolded summary, is already a strong hint, but the real issue is the repetitiveness of the list items. For bonus points there's a "not X, but Y", as well as a dash, albeit not an em dash.)

Good catch. You are absolutely right. My native language is Polish. I conducted the original research and discovered the 'square root proof fabrication' during sessions in Polish. I then reproduced the effect in a clean session for this case study. Since my written English is not fluent enough for a technical essay, I used Gemini as a translator and editor to structure my findings. I am aware of the irony of using an…

I see you used LLM to polish your English.

Re: Case study: Creative math – How AI fakes proofs

#87

Post by codeflo »

simonw wrote: post #19

Somewhat ironic that the author calls out model mistakes and then presents https://tomaszmachnik.pl/gemini-fix-en.html - a technique they claim reduces hallucinations which looks wildly superstitious to me. It involves spinning a whole yarn to the model about how it was trained to compete against other models but now it's won so it's safe for it to admit when it doesn't know something. I call this a superstition beca…

In my experience, there seems to be a limitless supply of newly crowned "AI shamans" sprouting from the deepest corners of LinkedIn. All of them make the laughable claim that hallucinations can be fixed by prompting. And of course it's only their prompt that works -- don't listen to the other shamans, those are charlatans.

If you disagree with them by explaining how LLMs actually work, you get two or three screenfuls of text in response, invariably starting with "That's a great point! You're correct to point out that..."

Avoid those people if you want to keep your sanity.

Re: Case study: Creative math – How AI fakes proofs

#88

Post by YeGoblynQueenne »

zkmon wrote: post #51

We are entering into a probabilistic era where things are not strictly black and white. Things are not binary. There is no absolute fake. A mathematical proof is an assertion that a given statement belongs to the world defined by a set of axioms and existing proofs. This world need not have strict boundaries. Proofs can have probabilities. Maybe Reimann's hypothesis has a probability of 0.999 of belonging to that mat…

What you're hinting at is the fact that proofs created by human mathematicians are not complete proofs but rather sketch proofs whose purpose is to convince mathematicians (including the person deriving the proof) that a statement (like the Reimann hypothesis) is true. Such human-derived proofs can even be wrong, as they sometimes turn out to be, so just because a proof is given, doesn't mean we have to automatically believe what it proves.

In that sense, proofs can be seen as evidence that a statement is true, and since one interpretation of Bayesian probabilities is that they express degrees of belief about the truth of a formal statement, then yes, proofs have something to do with probabilities.

But, in that context, it's not proofs that probabilities should be attached to. Rather, we can assign some probability to a formal statement, like the Reimann hypothesis, given that a proof exists. The proof is evidence that the statement is true and we can adjust our belief in the truth of the statement according to this and possibly other lines of evidence. In particular, if there are multiple and different proofs of the same statement that can increase our certainty that the statement is true.

The thing to keep in mind is that computers can derive complete proofs, in the sense that they can mechanically traverse the entire deductive closure of a statement given the axioms of a theory, and determine whether the statement is a theorem (i.e. true) or not but without skipping or fudging any steps, however trivial. This is what automated theorem provers do.

But it's important to keep in mind that LLMs don't do that kind of proof. They give us at best sketch proofs like the ones derived by human mathematicians, with the added complication that LLMs themselves cannot distinguish between a correct proof (i.e. one where every step, however fudgy, follows from the ones before it) and an incorrect one, or an automated theorem prover, are still required to check the correctness of a proof. LLM-based proof systems like AlphaProof work that way, passing an LLM-generated proof to an automated theorem prover as a verifier.

Mechanically-derived, complete proofs like the ones generated by automated theorem provers can also be assigned degrees of probability, but once we are convinced of the correctness of a prover (... because we have a proof!) then we can trust the proofs derived by that prover, and have complete belief in the truth of any statements derived.

Re: Case study: Creative math – How AI fakes proofs

#89

Post by YeGoblynQueenne »

teiferer wrote: post #53
zkmon wrote: post #51

We are entering into a probabilistic era where things are not strictly black and white. Things are not binary. There is no absolute fake. A mathematical proof is an assertion that a given statement belongs to the world defined by a set of axioms and existing proofs. This world need not have strict boundaries. Proofs can have probabilities. Maybe Reimann's hypothesis has a probability of 0.999 of belonging to that mat…

Definitely not. "Probability" does not mean "maybe yes, maybe not, let me assign some gut feeling value measuring how much I believe something to be the case." The mathematical field of probability theory has very precise notions of what a probability is, based in a measurable probability space. None of that applies to what you are suggesting. The Riemann Hypothesis is a conjecture that's either true or not. More pre…

>> "Probability" does not mean "maybe yes, maybe not, let me assign some gut feeling value measuring how much I believe something to be the case."

That's exactly what Baeysian probabilities are: gut feelings. Speaking of values attached to random variables, a good Bayesian basically pulls their probabilities out their ass. Probabilities, in that context, are nothing but arbitrary degrees of belief based on other probabilities. That's the difference with the frequentist paradigm which attempts to set the values of probabilities by observing the frequency of events. Frequentists ... believe that observing frequencies is somehow more accurate than pulling degrees of belief out one's ass, but that's just a belief itself.

You can put a theoretical sheen on things by speaking of sets or probability spaces etc, but all that follows from the basic fact that either you choose to believe, or you choose to believe because data. In either case, reasoning under uncertainty is all about accepting the fact that there is always uncertainty and there is never complete certainty under any probabilistic paradigm.

Re: Case study: Creative math – How AI fakes proofs

#90

Post by godelski »

lancebeet wrote: post #74
godelski wrote: post #20

I thought it funny a few weeks ago Karpathy shared a sample od NanoBannana solving some physics problems but despite getting the right output it isn't get the right answers. I think it's quite illustrative of the problem even with coding LLMs. Code and math proofs aren't so different, what matters is the steps to generate the output. All that matters far more than the actual output. The output is meaningless if the s…

>Maybe what surprised me most is that the mistakes NanoBananna made are simple enough that I'm absolutely positive Karpathy could have caught them. Even if his physics is very rusty. I'm often left wondering if people really are true believers and becoming blind to the mistakes or if they don't care. I've seen this interesting phenomenon many times. I think it's a kind of subconscious bias. I call it "GeLLMann amnesi…

That naming works better than it should lol. Crichton would be proud.
Post reply on HN