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

91–100 of 107 posts

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

#91

Post by embedding-shape »

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

Earlier quoted context omitted.

> 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 l…

> I haven’t found that to be the case in practice.

Do you have any public test code you could share? Or create even, should be fast.

I'm asking because I hear this constantly from people, and since most people don't have as high standards for their testing code as the rest of the code, it tends to be a half-truth, and when you actually take a look at the tests, they're as messy and incorrect as you (I?) think.

I'd love to be proven wrong though, because writing good tests is hard, which currently I'm doing that part myself and not letting LLMs come up with the tests by itself.

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

#92

Post by fragmede »

embedding-shape wrote: post #91
seanmcdirmid wrote: post #81

Earlier quoted context omitted.

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 l…

> I haven’t found that to be the case in practice. Do you have any public test code you could share? Or create even, should be fast. I'm asking because I hear this constantly from people, and since most people don't have as high standards for their testing code as the rest of the code, it tends to be a half-truth, and when you actually take a look at the tests, they're as messy and incorrect as you (I?) think. I'd lo…

Testing is fun, but getting all the scaffolding in place to get to the fun part and do any testing suuuuucks. So let the LLM write the annoying parts (mocks. so many mocks.) while you do the fun part

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

#93

Post by sorokod »

RestartKernel wrote: post #64
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…

Is there a term for "LLM psychology" like this? If so, it seems closer to a soft science than anything definitive.

Divination?

Divination is the attempt to gain insight into a question or situation by way of a magic ritual or practice.

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

#94

Post by seanmcdirmid »

embedding-shape wrote: post #91
seanmcdirmid wrote: post #81

Earlier quoted context omitted.

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 l…

> I haven’t found that to be the case in practice. Do you have any public test code you could share? Or create even, should be fast. I'm asking because I hear this constantly from people, and since most people don't have as high standards for their testing code as the rest of the code, it tends to be a half-truth, and when you actually take a look at the tests, they're as messy and incorrect as you (I?) think. I'd lo…

I'm doing all my work at Google, so its not like I can share it so easily. Also, since GeminiCLI doesn't support sub-agents yet...I've had to get creative with how I implement my pipelines. The biggest challenge I've found ATM is controlling conversation context so you can control what the AI is looking at when you do things (e.g. not looking at code when writing tests!). I hope I can release what I'm doing eventually, although it isn't a key piece of AI tech (just a way to orchestrate the pipeline to make sure that AI gets different context for different parts of the pipeline steps, it might be obsolete after we get better support for orchestrating dev work in GeminiCLI or other dev-oriented AI front ends).

The tests can definitely be incorrect, and are often incorrect. You have to tell the AI that consider that the tests might be wrong, not the implementation, and it will generally take a closer look at things. They don't have to be "good" tests, just good enough tests to get the AI writing not crap code. Think very small unit tests that you normally wouldn't think about writing yourself.

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

#95

Post by embedding-shape »

seanmcdirmid wrote: post #94
embedding-shape wrote: post #91

Earlier quoted context omitted.

> I haven’t found that to be the case in practice. Do you have any public test code you could share? Or create even, should be fast. I'm asking because I hear this constantly from people, and since most people don't have as high standards for their testing code as the rest of the code, it tends to be a half-truth, and when you actually take a look at the tests, they're as messy and incorrect as you (I?) think. I'd lo…

I'm doing all my work at Google, so its not like I can share it so easily. Also, since GeminiCLI doesn't support sub-agents yet...I've had to get creative with how I implement my pipelines. The biggest challenge I've found ATM is controlling conversation context so you can control what the AI is looking at when you do things (e.g. not looking at code when writing tests!). I hope I can release what I'm doing eventuall…

> They don't have to be "good" tests, just good enough tests to get the AI writing not crap code. Think very small unit tests that you normally wouldn't think about writing yourself.

Yeah, those for me are all not "good tests", you don't want them in your codebase if you're aiming for a long-term project. Every single test has to make sense and be needed to confirm something, and should give clear signals when they fail, otherwise you end locking your entire codebase to things, because knowing what tests are actually needed or not becomes a mess.

Writing the tests and let the AI write the implementation ends you up with code you know what it does, and can confidently say what works vs not. When the IA ends up writing the tests, you often don't actually know what works or not, not even by scanning the test titles you often don't learn anything useful. How is one supposed to be able to guarantee any sort of quality like that?

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

#96

Post by seanmcdirmid »

embedding-shape wrote: post #95
seanmcdirmid wrote: post #94

Earlier quoted context omitted.

I'm doing all my work at Google, so its not like I can share it so easily. Also, since GeminiCLI doesn't support sub-agents yet...I've had to get creative with how I implement my pipelines. The biggest challenge I've found ATM is controlling conversation context so you can control what the AI is looking at when you do things (e.g. not looking at code when writing tests!). I hope I can release what I'm doing eventuall…

> They don't have to be "good" tests, just good enough tests to get the AI writing not crap code. Think very small unit tests that you normally wouldn't think about writing yourself. Yeah, those for me are all not "good tests", you don't want them in your codebase if you're aiming for a long-term project. Every single test has to make sense and be needed to confirm something, and should give clear signals when they f…

If it clarifies anything, I have my workflow (each step is a separate prompt without preserved conversation context):

1 Create a test plan for N tests from the description. Note that this step doesn't provide specific data or logic for the test, it just plans out vaguely N tests that don't overlap too much.

2 Create an interface from the description

3 Create an implementation strategy from the description

4.N Create N tests, one at a time, from the test plan + interface (make sure the tests compile) (note each test is created in its own prompt without conversation context)

5 Create code using interface + implementation strategy + general knowledge, using N tests to validate it. Give feedback to 4.I if test I fails and AI decides it is the test's fault.

If anything changes in the description, the test plan is fixed, the tests are fixed, and that just propagates up to the code. You don't look at the tests unless you reach a situation where the AI can't fix the code or the tests (and you really need to help out).

This isn't really your quality pass, it is crap filter pass (the code should work in the sense that a programmer wrote something that they thinks works, but you can't really call it "tested" yet). Maybe you think I was claiming that this is all the testing that you'll need? No, you still need real tests as well as these small tests...

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

#98

Post by teiferer »

YeGoblynQueenne wrote: post #89
teiferer wrote: post #53

Earlier quoted context omitted.

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 prob…

Baffling to see such a take on HN.

If I give you a die and ask about the probabiliy for a 6, then it's exactly 1/6. Being able to quantify this exactly is the great success story of probability theory. You can have a different "gut feeling", and indeed many people do (lotteries are popular), but you would be wrong. If you run this experiment a large number of times, then about 1/6 of the outcomes will be a 6, proving the 1/6 right and the deviating "gut feeling" wrong. That number is not "pulled out of somebody's ass" or some frequentist approach. It's what probability means.

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

#99

Post by YeGoblynQueenne »

teiferer wrote: post #98
YeGoblynQueenne wrote: post #89

Earlier quoted context omitted.

>> "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 prob…

Baffling to see such a take on HN. If I give you a die and ask about the probabiliy for a 6, then it's exactly 1/6. Being able to quantify this exactly is the great success story of probability theory. You can have a different "gut feeling", and indeed many people do (lotteries are popular), but you would be wrong. If you run this experiment a large number of times, then about 1/6 of the outcomes will be a 6, proving…

Yes, that's the frequentist approach. Surely, even on HN, there is an understanding that there are two interpretations of probability?

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

#100

Post by CyberDildonics »

YeGoblynQueenne wrote: post #99
teiferer wrote: post #98

Earlier quoted context omitted.

Baffling to see such a take on HN. If I give you a die and ask about the probabiliy for a 6, then it's exactly 1/6. Being able to quantify this exactly is the great success story of probability theory. You can have a different "gut feeling", and indeed many people do (lotteries are popular), but you would be wrong. If you run this experiment a large number of times, then about 1/6 of the outcomes will be a 6, proving…

Yes, that's the frequentist approach. Surely, even on HN, there is an understanding that there are two interpretations of probability?

You don't think that the probability of each side of a die is 1/6 ?
Post reply on HN