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

First Proof

arxiv.org

Post reply on HN
Print view View original

41–50 of 126 posts

Re: First Proof

#41

Post by YeGoblynQueenne »

yorwba wrote: post #11
blenderob wrote: post #6

Can someone explain how this would work? > the answers are known to the authors of the questions but will remain encrypted for a short time. Ok. But humans may be able to solve the problems too. What prevents Anthropic or OpenAI from hiring mathematicians, have them write the proof and pass it off as LLM written? I'm not saying that's what they'll do. But shouldn't the paper say something about how they're going to v…

This is not a benchmark. They just want to give people the opportunity to try their hand at solving novel questions with AI and see what happens. If an AI company pulls a solution out of their hat that cannot be replicated with the products they make available to ordinary people, that's hardly worth bragging about and in any case it's not the point of the exercise.

Hey, sorry, totally out of context but I've always wanted to ask about the username. I keep reading it as "yoruba" in my mind. What does it mean, if I'm not being indiscreet?

Re: First Proof

#42

Post by Centigonal »

nemo1618 wrote: post #33
Syzygies wrote: post #23

I'm a mathematician relying heavily on AI as an association engine of massive scope, to organize and expand my thoughts. One doesn't get best results by "testing" AI. A surfboard is also an amazing tool, but there's more to operating one than telling it which way to go. Many people want self-driving cars so they can drink in the back seat watching movies. They'll find their jobs replaced by AI, with a poor quality of…

Centaurs are a transient phenomenon. In chess, the era of centaur supremacy lasted only about a decade before computers alone eclipsed human+computer. The same will be true in every other discipline. You can surf the wave, but sooner or later, the wave will come crashing down.

How transient depends on the problem space. In chess, centaurs were transient. In architecture or CAD, they have been the norm for decades.

Re: First Proof

#43

Post by eranation »

nemo1618 wrote: post #33
Syzygies wrote: post #23

I'm a mathematician relying heavily on AI as an association engine of massive scope, to organize and expand my thoughts. One doesn't get best results by "testing" AI. A surfboard is also an amazing tool, but there's more to operating one than telling it which way to go. Many people want self-driving cars so they can drink in the back seat watching movies. They'll find their jobs replaced by AI, with a poor quality of…

Centaurs are a transient phenomenon. In chess, the era of centaur supremacy lasted only about a decade before computers alone eclipsed human+computer. The same will be true in every other discipline. You can surf the wave, but sooner or later, the wave will come crashing down.

I'm highly worried that you are right. But what gives me hope is that people still play chess, I'd argue even more than ever. People still buy paper books and vinyl records. People still appreciated handwritten greeting cards over printed ones, pay extra to listen to live music where the recorded one is free and will likely sound much better. People are willing to pay an order of magnitude more for a sit in a theater for a live play, or pay premium for handmade products over their almost impossible to distinguish knock offs.

Re: First Proof

#44

Post by rvz »

> Conflicts of interest. No funding was received for the design or implementation of this project. None of the authors of this report was employed by or consulted with AI companies during the project, nor will they do so while contributing to it

As it should. Good.

This is a totally independent test not conducted or collaborated by any of the AI companies or employees so that no bias is introduced at all[0].

[0] Unless the researchers are not disclosing if they have any ownership of shares in private AI companies.

Re: First Proof

#45

Post by data_maan »

jsnell wrote: post #9
falloutx wrote: post #7

Anything special about these questions? Are they unsolved by humans. I am not working in mathematics research so its hard to tell the importance.

The abstract of the article is very short, and seems pretty clear to both of your questions. This is what is special about them: > a set of ten math questions which have arisen naturally in the research process of the authors. The questions had not been shared publicly until now; I.e. these are problems of some practical interest, not just performative/competitive maths. And this is what is know about the solutions:…

> these are problems of some practical interest, not just performative/competitive maths.

FrontierMath did this a year ago. Where is the novelty here?

> a solution is known, but is guaranteed to not be in the training set for any AI.

Wrong, as the questions were poses to commercial AI models and they can solve them.

This paper violates basic benchmarking principles.

Re: First Proof

#46

Post by pama »

hiq wrote: post #38

I'm realizing I don't know if it's currently harder for an LLM to: * come up with a formal proof that checks out according to a theorem prover * come up with a classical proof that's valid at a high-level, with roughly the same correctness as human-written papers Is this known?

The advantage of the formal proof is that the LLM in a loop can know that it failed and keep trying.

Re: First Proof

#47

Post by data_maan »

bawolff wrote: post #34
data_maan wrote: post #31

As mathematically interesting the 10 questions are that the paper presents, the paper is --sorry for the harsh language-- garbage from the point of view of benchmarking and ML research: Just 10 question, few descriptive statistics, no interesting points other than "can LLMs solve these uncontaminated questions", no long bench of LLMs that were evaluated. The field of AI4Math has so many benchmarks that are well execu…

Paper not about benchmarking or ML research is bad from the perspective of benchmarking. Not exactly a shocker. The authors themselves literally state: "Unlike other proposed math research benchmarks (see Section 3), our question list should not be considered a benchmark in its current form"

On the website https://1stproof.org/#about they claim: "This project represents our preliminary efforts to develop an objective and realistic methodology for assessing the capabilities of AI systems to autonomously solve research-level math questions."

Sounds to me to be a benchmark in all but a name. And they failed pretty terribly at achieving what they set out to do.

Re: First Proof

#48

Post by lanyard-textile »

nemo1618 wrote: post #33
Syzygies wrote: post #23

I'm a mathematician relying heavily on AI as an association engine of massive scope, to organize and expand my thoughts. One doesn't get best results by "testing" AI. A surfboard is also an amazing tool, but there's more to operating one than telling it which way to go. Many people want self-driving cars so they can drink in the back seat watching movies. They'll find their jobs replaced by AI, with a poor quality of…

Centaurs are a transient phenomenon. In chess, the era of centaur supremacy lasted only about a decade before computers alone eclipsed human+computer. The same will be true in every other discipline. You can surf the wave, but sooner or later, the wave will come crashing down.

Agreed. But I don't think the time scale will be similar.

Chess is relatively simple in comparison, as complex as it is.

Re: First Proof

#49

Post by cadamsdotcom »

Syzygies wrote: post #23

I'm a mathematician relying heavily on AI as an association engine of massive scope, to organize and expand my thoughts. One doesn't get best results by "testing" AI. A surfboard is also an amazing tool, but there's more to operating one than telling it which way to go. Many people want self-driving cars so they can drink in the back seat watching movies. They'll find their jobs replaced by AI, with a poor quality of…

This is beautifully written, thank you for writing it.

Typing out solutions to problems was only part of the job description because there was no other way to code. Now we have a far better way.

Post reply on HN