4 ms·

This must be one of the best applications for LLMs, as you can always automatically verify the results, or reject them otherwise, right?

by _flux 2y ago

deleted 2y ago
[deleted]
UltraSane 2y ago
[dead]
yuhfdr 2y ago
Same with code generation. But generating useless code, or proofs, just to discard them is hardly a consequence and externality free effort.
- kkzz99 2y ago
  But you can far more easily scale llm generation compared to human researchers.
  - yuhfdr 2y ago
    Sloppyjoes always assume the best case for llms and worst case for their counter example of choice. 10 trillion llms, powered by a Dyson sphere, that still output slop is still worse than one unappreciated post doc.
    - bluechair 2y ago
      That was funny even if I don’t agree with the sentiment.
aithrowawaycomm 2y ago
The dependence on huge amounts of synthetic data makes it hard for me to see an application for mathematicians. The theorems being proved here are incredibly boring, more like calculation-heavy homework problems from a professor who is mean to freshmen. (This is not the same thing as what Terence Tao has been looking at, which is more human language -> Lean "translation.") There is a basic problem that new and interesting mathematics does not have the data for ANNs to learn from; this mathematics is very old and there are thousands of examples online. To be extremely pedantic the authors didn't show DeepSeek was good at proofs, but rather at undergraduate competition math problems. I am assuming some of that transfers... but I am a huge critic of LLMs and even so I constantly overestimate them! However I could see this being useful for verified software development, which usually involves a huge amount of tedious and uninteresting lemmas, and the size of the proofs becomes exhausting. Having an LLM check all 2^8 configurations of something seems worthwhile.
danielmarkbruce 2y ago
Any situation involving the ability to simulate (like, weather models, bio models, physics models) is potentially a good application. It's still hard to make a good model to approximate an extremely complex function.

This must be one of the best applications for LLMs, as you can always automatically verify the results, or reject them otherwise, right?

by _flux 2y ago

This must be one of the best applications for LLMs, as you can always automatically verify the results, or reject them otherwise, right?

deleted 2y ago

[deleted]

UltraSane 2y ago

[dead]

yuhfdr 2y ago

Same with code generation. But generating useless code, or proofs, just to discard them is hardly a consequence and externality free effort.

kkzz99 2y ago
But you can far more easily scale llm generation compared to human researchers.
- yuhfdr 2y ago
  Sloppyjoes always assume the best case for llms and worst case for their counter example of choice. 10 trillion llms, powered by a Dyson sphere, that still output slop is still worse than one unappreciated post doc.
  - bluechair 2y ago
    That was funny even if I don’t agree with the sentiment.

aithrowawaycomm 2y ago

The dependence on huge amounts of synthetic data makes it hard for me to see an application for mathematicians. The theorems being proved here are incredibly boring, more like calculation-heavy homework problems from a professor who is mean to freshmen. (This is not the same thing as what Terence Tao has been looking at, which is more human language -> Lean "translation.") There is a basic problem that new and interesting mathematics does not have the data for ANNs to learn from; this mathematics is very old and there are thousands of examples online. To be extremely pedantic the authors didn't show DeepSeek was good at proofs, but rather at undergraduate competition math problems. I am assuming some of that transfers... but I am a huge critic of LLMs and even so I constantly overestimate them! However I could see this being useful for verified software development, which usually involves a huge amount of tedious and uninteresting lemmas, and the size of the proofs becomes exhausting. Having an LLM check all 2^8 configurations of something seems worthwhile.

danielmarkbruce 2y ago

Any situation involving the ability to simulate (like, weather models, bio models, physics models) is potentially a good application. It's still hard to make a good model to approximate an extremely complex function.