News for hackers. Stuff that matters.
Re:DeepSeek: Advancing theorem proving in LLMs through large... by disconcision on Monday October 14, 2024 @09:50PM (#41844144)
not obviously the case. natural language also has tree/dag structure yet transformers do okay with it. encoding higher order structure in linear sequences seems necessary for transformers to be able to do most anything
Re:DeepSeek: Advancing theorem proving in LLMs through large... by llm_trw on Monday October 14, 2024 @11:10PM (#41844539)
Not to arbitrary depth. Empirically the majority of text has depth less than 6 when represented as a tree. Proofs on the other hand have no a priori limits to their depth.
Re:DeepSeek: Advancing theorem proving in LLMs through large... by looofooo0 on Tuesday October 15, 2024 @06:16AM (#41846997)
But isn't math strucutured in the same way subdivided in lemmas, theorems, corollarys with limited depth.
Re:DeepSeek: Advancing theorem proving in LLMs through large... by llm_trw on Tuesday October 15, 2024 @07:09AM (#41847305)
No. It's pretty common to have depth 20+ on even relatively simple proofs when you start looking at decomposing proofs to their axioms.

The old joke about 1 + 1 = 2 being on page 360 of Principia Mathematica still largely holds.

Re:DeepSeek: Advancing theorem proving in LLMs through large... by auggierose on Tuesday October 15, 2024 @07:19AM (#41847353)
That depends on the granularity of your proof steps. That old joke doesn't hold for a very long time now (take a look at Isabelle/Isar proofs), yet people keep bringing it up.
Re:DeepSeek: Advancing theorem proving in LLMs through large... by llm_trw on Tuesday October 15, 2024 @07:59AM (#41847620)
Doesn't matter what the granularity of your proof step us you still need to understand what that proof step does to be a mathematician. You seem to mistake syntactic brevity for semantic meaning.
Re:DeepSeek: Advancing theorem proving in LLMs through large... by auggierose on Tuesday October 15, 2024 @01:39PM (#41851005)
Mathematicians do very large proof steps, and so can the computer these days. If you do something like (proof by auto: thm_1 thm_2 thm_3) and it goes through, then I know why the proof works (because of these theorems), and this is similar to how a mathematician understands something. Syntactic brevity is indeed an indicator that you understand the proof. The better you understand something, the more concise you can formulate and prove it.