4 ms·
The paper makes a similar point like this: Every definition and theorem in mathlib and this project have been checked by Lean’s trusted kernel, which computati
by btilly 3y ago
The paper makes a similar point like this:
Every definition and theorem in mathlib and this project have been checked by Lean’s trusted kernel, which computationally verifies that the proofs we have constructed are indeed correct. However, Lean cannot check that the statements of the definitions and theorems match their intended English equivalents, so when drawing conclusions from the code in this project, translation to and from English must be done with care.
- amw-zero 3y agoThis is precisely why humans will always be involved with creating software.
- rsaarelm 3y agoHow do you think humans are doing this this if you don't think machines can ever do anything similar?
- Ericson2314 3y agoYou misunderstand. The point here is not about humans being better or worse at some task than humans, but humans defining the objective function.
- nathan_compton 3y agoThis doesn't seem to follow. Why kind computers get better at doing this (anticipating what humans want or whatever) than people? Some people are better at it than others and people are not magic, so I'd guess at some point computers will get it too.
- wolfram74 3y agoI think what the parent post is referring to is that clarifying human intention rather axiomatically involves a human at some stage in the process.
- naasking 3y agoLLMs already write English better than most native speakers. I wouldn't bet everything on this.
- The_Colonel 3y agoDo you trust LLM so much that you don't check what it writes before sending the email? LLMs can write better English, but the curating step is still critical, because it also produces a lot of garbage.
- naasking 3y agoWould you trust a brand new assistant to write up an email for you without proof reading it? How much training would they require before you didn't need that step? How much training / fine-tuning would an LLM need? What about the next gen LLM? Remember, we're not talking about a static target here, and the post I replied to set no qualifications on the claim that a human will always be needed to check that a mathematical definitions in the proof match the English equivalents. That's a long timeline on a rapidly moving target that is, as I said, already seems to be better than most humans at understanding and writing English.
- The_Colonel 3y ago> Would you trust a brand new assistant to write up an email for you without proof reading it? Depends on the complexity, but for the simpler things I think I could get confident in a day or so. For more complex things, it might take longer to assess their ability. But I'm not going to trust LLM blindly for anything. > I replied to set no qualifications on the claim that a human will always be needed to check that a mathematical definitions in the proof match the English equivalents. I don't defend this strong claim and limit my answer to LLMs (and mostly just state of the art). OTOH I believe that trust will continue to be a big topic for any future AI tech.
- naasking 3y ago> But I'm not going to trust LLM blindly for anything. Again, what does "blindly" mean? Suppose you went a month without finding a single issue. Or two months. Or a year. The probability of failure must literally be zero before you rely on it without checking? Are you applying the same low probability failure on the human equivalent? Does a zero probability of failure for a human really seem plausible?