ygolo
My termites win
- Joined
- Aug 6, 2007
- Messages
- 6,863
More thoughts countering the "scale it and benefits will come" cult.
There are many forms of reasoning. But on one form of reasoning, deductive reasoning, we created extremely sharpened forms of quality control (usually involving symbols):
1) Mathematics - considered the science of patterns. The proof (a mechanism developed over centuries) is a means to create high quality deductive reasoning about patterns. There are attempts to automate it or formalize it called Theorem Provers, the most popular being Lean and Rocq.
Here is one video of Terence Tao (arguably the world's best living Mathematician) using LLMs with Lean (There are others):
2) Computers and Software - Initially just a split from Math but now used everywhere. We've gone from humans being computers, to tapes, to punch cards, to assemblers, to compilers, to code generators, no-code tools, and now AI. This is an amazing match for use with AI. It's an evolution of things that have been happening for a long time.
In both these cases, you really don't need or want to regenerate results in math or computer science. It is incredibly wasteful - you want a copy. There's an old joke about reducing these problems to already solved problems.
But when you see the most energy inefficient, and most used areas for these large scale AIs, it is computing and math. This, to me, suggests that building an appropriate "database" of deductive arguments (say using Lean or Rocq, and of code snippets for standard problems) that then gets served to the whole public is the most societally energy efficient way to build a system for this purpose.
There are many forms of reasoning. But on one form of reasoning, deductive reasoning, we created extremely sharpened forms of quality control (usually involving symbols):
1) Mathematics - considered the science of patterns. The proof (a mechanism developed over centuries) is a means to create high quality deductive reasoning about patterns. There are attempts to automate it or formalize it called Theorem Provers, the most popular being Lean and Rocq.
Here is one video of Terence Tao (arguably the world's best living Mathematician) using LLMs with Lean (There are others):
2) Computers and Software - Initially just a split from Math but now used everywhere. We've gone from humans being computers, to tapes, to punch cards, to assemblers, to compilers, to code generators, no-code tools, and now AI. This is an amazing match for use with AI. It's an evolution of things that have been happening for a long time.
In both these cases, you really don't need or want to regenerate results in math or computer science. It is incredibly wasteful - you want a copy. There's an old joke about reducing these problems to already solved problems.
But when you see the most energy inefficient, and most used areas for these large scale AIs, it is computing and math. This, to me, suggests that building an appropriate "database" of deductive arguments (say using Lean or Rocq, and of code snippets for standard problems) that then gets served to the whole public is the most societally energy efficient way to build a system for this purpose.