Well you can’t verify a prediction about human biology without a phase 3 clinical trial so…

The thing that I've not fully groked here (might be relevant) is that OAI is generating "paper" proofs first, and only then formalizes them in Lean as a separate step. They've as far as I'm aware not said anywhere how many write ups failed formalization due to a bug in the proof. If we assume that number is low, models would be quite good at one-shotting math proofs. Then it depends if you can replicate the math RL training for chemistry/biology/medicine. Is there enough data out there for that? No idea.

▲

abathologist a day ago | parent | next [-]

I'm seeing estimates of a %95-91 failure rate on attempts in generally (or, conversely, a max of ~10% success, but likely lower, since we can only go based on how many attempts they are willing to mention in their statements). E.g., from analysis in https://medium.com/@mehmet.ozel2701/openai-tried-about-4-000...

I wonder how many of those founder at the "paper" to formalization step, or at earlier or later steps (e.g., proof doesn't turn out to prove what the paper said, hits a bug in the kernel, etc.).

	▲	eru a day ago \| parent [-]
		Wouldn't a bug in the (Lean) kernel just result in a PR to Lean?

▲

KerrAvon a day ago | parent | prev [-]

based on how bad these models are at one-shotting complex real-world software engineering problems -- it always has to be a conversation -- there is absolutely no way they're one-shotting complex math proofs.

Also, goes without saying, but put Sam Altman in jail, obviously.

▲

a day ago | parent | prev [-]

[deleted]