51–60 of 105 posts
Another project I'm excited about in this area is GPTScript, which launched last week: http://github.com/gptscript-ai/gptscript.
> not unlike other packages such as marvin This feels pretty much identical to Marvin? Like the entire API? From a genuine place of curiosity: I get that your prompts are different, but like why in the name of open source would you just not contribute to these libraries instead of starting your own from scratch?
Earlier quoted context omitted.
Not 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.
Is 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)
In fact, synthesis has a relatively rich history using SAT/SMT solvers.
Earlier quoted context omitted.
here's an awesome post on the landscape https://hamel.dev/blog/posts/prompt/
I remember reading that, good stuff. I'd like to see an injectable mitm like proxy that can rewrite payloads. Many of these frameworks are useful, but when they go off the rails, they hard to modify and introspect. It would be nice if LLMs had a way to speak an annotated format, like XML that was able to encode higher level information in a coherent manner over "well formed" addhoc text. LLM libraries are in a crazy…
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…
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.
Earlier quoted context omitted.
Is 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)
Decoupling 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.
Earlier quoted context omitted.
All of these acronyms are so confusing. I'm assuming LLVM isn't the compiler tool, but searching "LLVM ai" doesn't give me any good results.
They probably meant vLLM https://docs.vllm.ai/en/latest/
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…
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/49...
Instead of this:
@ai() def describe(animals: list[str]) -> str: """ Given a list of animals, use one word that'd describe them all. """
it would seem a lot more intuitive to do this:
def describe(animals: list[str]) -> str: return ai("""Given a list of animals, use one word that'd describe them all.""", animals)
Does anyone else get bothered by how this seemingly results in code that won't compile? Instead of this: @ai() def describe(animals: list[str]) -> str: """ Given a list of animals, use one word that'd describe them all. """ it would seem a lot more intuitive to do this: def describe(animals: list[str]) -> str: return ai("""Given a list of animals, use one word that'd describe them all.""", animals)
For your suggestion, the decorator would still be required to overload the function execution with the remote call, otherwise you'd just be calling the function body, but we have considered special wrapper return types to help play better with pyright (and also give programmatic access to debug details of the call), but that'd add bloat to the package and subtract from the more native python feel we're aiming for.