5 ms·
IMHO, in the future programming may look similar to this. Write a type declaration for a function with an expressive type system, e.g. refinement types. Then us
by nextos 3y ago
IMHO, in the future programming may look similar to this. Write a type declaration for a function with an expressive type system, e.g. refinement types. Then use LLMs + SAT/SMT to generate provably correct code.
This strikes a happy medium, where machines are assisting programmers, making them much more productive. Yet the resulting code is understandable as a human has decomposed everything into functions, and also robust as it is formally verified.
I am working on a F# proof-of-concept system like this, there are other alternatives around implemented in Haskell and other languages with varying levels of automation. It is potentially an interesting niche for a startup.
- edunteman 3y agoyeah I had a moment working with fructose where I realized "oh this is more like functional programming than I expected"
- obeavs 3y agoIs the F# POC open source? Link?
- nextos 3y agoNot yet, it's a bit rough. The LLM I am using requires a bit of extra fine-tuning to be really smooth, I need to rent a bigger GPU. Besides, I am working on some novel integration between transformers and SAT/SMT that will take me some time to finish.
- yaj54 3y agoIs the theory tied to a specific llm? I'm interpreting it as, e.g., the llm writes the code, the solver verifies it, repeat until correct. In this situation the two are decoupled and the llm would be a drop in and thusly could be any local or remote llm. Is there something about your approach that doesn't allow this? (also, +1 for OS link request)
- nextos 3y agoDecoupling both is the simplest option, but not the one I am focusing on. Also note SAT/SMT can also be used for synthesis. In fact, synthesis has a relatively rich history using SAT/SMT solvers.
- yaj54 3y agoAre you using the SAT/SMT solvers to feed training data into a transformer or integrating the solver logic into the model code?
- obeavs 3y agoOur product (phosphor) is built end-to-end in F# so this stuff is close to my heart. You might find Moonbit's approach to functional AI interesting as well https://www.moonbitlang.com/blog/moonbit-ai https://www.moonbitlang.com/blog/moonbit-ai.
- ravenstine 3y agoYeah, functional programming and pure functions seem perfect for generative programming. Granted, I think they're perfect in general, but as long as human programmers are still stuck in the world of object-orientation (the modern sense), then they're going to be wasting the time in the LLM feedback loop. The LLM should be be able to write a unit of code however it wants in a way that is as self-contained as possible. Since an LLM can, in theory, quickly "understand" code that most software engineers would object to, then we should get out of the way of LLMs rather than expect them to be like we are.
- fwip 3y agoThis project seems pretty different to what you've proposed. Fructose looks like it's "just" asking an LLM to evaluate a function (written in English text), and then jamming whatever comes out back into your type system. Being able to sometimes answer a given question is perhaps a first step to writing code that can answer that question reliably, but it's a long way from an LLM that does the former to one that does the latter.
- nickpsecurity 3y agoThe field that has been doing this is called Program Synthesis. Here’s an example survey: https://www.microsoft.com/en-us/research/publication/program-synthesis/ https://www.microsoft.com/en-us/research/publication/program... I’ve wanted to see the traditional techniques combined with modern ML to sort of drive the search and generation process. Then, we’d still have the advantages of both formal specifications and classic AI (esp traceability). While looking for a synthesis link, I stumbled onto one paper trying to mix the two approaches: https://ojs.aaai.org/index.php/AAAI/article/download/5048/4921 https://ojs.aaai.org/index.php/AAAI/article/download/5048/49...
- ddellacosta 3y agoOh yeah, you just reminded me of this cool talk I saw at Strange Loop a while back. Not about the AI parts but re: program synthesis in Haskell: "Type-Driven Program Synthesis" by Nadia Polikarpova https://www.youtube.com/watch?v=HnOix9TFy1A https://www.youtube.com/watch?v=HnOix9TFy1A Links to more projects and papers by Prof. Polikarpova: https://cseweb.ucsd.edu/~npolikarpova/ https://cseweb.ucsd.edu/~npolikarpova/ I think this is one of the main projects she discusses in the talk: https://github.com/nadia-polikarpova/synquid https://github.com/nadia-polikarpova/synquid EDIT: meant to mention this too, which I think has been around a bit longer, not that I've ever used it in production: https://ucsd-progsys.github.io/liquidhaskell/ https://ucsd-progsys.github.io/liquidhaskell/
- nextos 3y agoLots of related work also by A. Solar-Lezama https://people.csail.mit.edu/asolar https://people.csail.mit.edu/asolar, sometimes in collaboration with N. Polikarpova.
- ddellacosta 3y agoTIL, nice--thanks!
- amiantos 3y ago> Write a type declaration for a function with an expressive type system, e.g. refinement types. Then use LLMs + SAT/SMT to generate provably correct code. This is how I use copilot currently, so I might not be following on what part of this is 'future' facing or relevant to this Fructose project? Not being contrarian, I thought this was an interesting point but as I thought about it more I realized, "wait, they're describing what I already do".
- AgentOrange1234 3y agoHow do you do this? I know nothing but this sounds really interesting.
- nextos 3y agoDo you use Copilot on a language equipped with refinement or dependent types, and use said types to constrain generation of entire functions, in a single step, that are also formally verified?
- trenchgun 3y agoHow!!! Could you think of writing a blog post about it?
- pyinstallwoes 3y agoOddly similar to summoning demons.