4 ms·
It translates natural language into Isabelle/HOL specifications, and then tries to fill these up to prove things. One can then use Isabelle code generation faci
by nextos 2y ago
It translates natural language into Isabelle/HOL specifications, and then tries to fill these up to prove things. One can then use Isabelle code generation facilities to extract Scala, OCaml, etc. I think the trick is to have a programmer to guide the whole process, especially decomposition into different modules and abstractions.
- kragen 2y agowhat have you been able to get it to write so far?
- kragen 2y ago(i hope this comment didn't sound skeptical or dismissive)
- nextos 2y agoNo worries! The comment was fine, I was simply gone so I couldn't reply. TBH, I haven't written anything impressive, just toy examples that are formally verified. I imagine making it practical for larger systems would require a lot more work.
- kragen 2y agoi'm curious to know what you mean by toy examples! are we talking about an assignment statement, an arithmetic expression, finding the maximum of a list, insertion sort, mergesort, a parser for a context-free language, a cooperative multithreading system?
- nextos 2y agoSome simple imperative data structures, including simple operations to add, remove, test membership, etc. with formal guarantees.
- kragen 2y agothat sounds awesome! what does the process of getting to one of those proofs look like? is there a lot of back and forth, or is it mostly autonomous?
- nextos 2y agoMostly autonomous, with a bit of guidance, but this might be because the training set has examples that are similar enough, making interpolation easy.
- kragen 2y agofantastic! i hope you decide to share more details; i'd love to hear them
- nextos 2y agoThanks. It's a toy at the minute, there is nothing super impressive. Taking this forward would require a lot more work and funding to pay for computation to fine-tune models further. It's an interesting topic, perhaps good for a startup or a research lab in case one finds a decent monetization stream.
- kragen 2y agopretty sure you'll be able to monetize writing correct software at scale with an llm
- versteegen 2y agoNice. I agree that LLMs will be game-changing for easing the writing of specifications/contracts for verified code; it could become the standard. Interesting that you're using Isabelle/HOL for code generation. I'm working towards auto-formalization of maths using LLM translation to an intermediate language between English and the proof assistant (for which I'm leaning towards Isabelle/HOL) and then a toolbox of techniques (i.e. ATP) for the remaining translation. Formalization is too painful at the moment. It's nearly the same problem as yours. But I'm starting out on simpler problems. So I'm really interested in the "filling up" part, if you have anything to say about it.