4 ms·
While this isn't optimization, is there any LLM systems that create "provably correct" transformations yet? I have used ChatGPT on some fairly awful code, aski
by CJefferson 3y ago
While this isn't optimization, is there any LLM systems that create "provably correct" transformations yet?
I have used ChatGPT on some fairly awful code, asking it to add comments, rename variables and functions, etc. I find the outputs useful, but a couple of times it's broken the code. I imagine for many (not all) languages, you could ask the LLM to produce suggested changes, then use a code-rewriting tool to apply them in a way you could be 100% sure they weren't going to change the behaviour of the progrma.
- deleted 3y ago[deleted]
- quickthrower2 3y agoSounds like TDD and langchain? Where the T can be anything from Ruby unit tests to Coq proofs.
- wrsh07 3y agoAre you compiling the code or interpreting?
- CJefferson 3y agoCompiling C++ code, which means there is a chance you could prove transformations correct, but I’m not going to try it myself :)
- wrsh07 3y agoAt the very least transformations that produce identical assembly are safe. I think.
- darksaints 3y agoI can't imagine there would be any success with an LLM that isn't already known about via Satisfiability Modulo Theory.
- CJefferson 3y agoI use SMT, but I can’t imagine how it would suggest good names for variables?
- aureianimus 3y agoNot strictly what you're looking for, but in Lean (functional language/theorem prover), there's some interesting work being done. Using the tool actually shows which suggestions will compile, which certifies correctness to some degree. https://leandojo.org/ https://leandojo.org/
- isaacfung 3y agoSimilar ideas Certified Reasoning with Language Models https://github.com/gpoesia/certified-reasoning https://github.com/gpoesia/certified-reasoning It's based on Peano, a theorem proving environment Peano: Learning Formal Mathematical Reasoning https://arxiv.org/abs/2211.15864 https://arxiv.org/abs/2211.15864 (https://github.com/kyegomez/LOGICGUIDE https://github.com/kyegomez/LOGICGUIDE claims to implement the same paper as the first repo but it is fake)