4 ms·
This is great and could provide additional guardrails on top of large language models. I imagine we could provide a more rigorous approach to prove that a LLM c
by kittikitti 2y ago
This is great and could provide additional guardrails on top of large language models. I imagine we could provide a more rigorous approach to prove that a LLM can behave in certain ways within a workflow.
- ijustlovemath 2y agoLLMs are fundamentally probabilistic in nature; I think you could prove things about distributions of outputs but nothing like the kind of formal verification you can create with Lean or Rust.
- palata 2y agoIsn't it a fundamental limitation of LLMs that we can't?
- rscho 2y agoObviously not. It's right in the name, isn't it? LLM = limitless model...
- xigoi 2y agoAn LLM is pretty much a black box. You can’t prove anything meaningful about its output.
- IceDane 2y agoYou are really comparing apples to oranges here, and to say that trying to apply formal verification to a probabilistic lying machine is silly would be a colossal understatement.
- TypingOutBugs 2y agoThere’s a few papers in this space but it’s still early days, both using Formal Verification to test outputs of LLMs and using LLMs in formal verification itself Examples of both: https://sumitkumarjha.com/papers/2023_ICAA_LLM_Dehallucinating_Jha.pdf https://sumitkumarjha.com/papers/2023_ICAA_LLM_Dehallucinati... https://mathai2023.github.io/papers/28.pdf https://mathai2023.github.io/papers/28.pdf