Scalable generative AI-based tool infrastructure
Embodiments of the present disclosure include a formal verification method comprising a plurality of custom generative AI-based tools configured in a bottoms up methodology to generate formal verification code using an LLM. In another embodiment, the present disclosure includes a generative AI-based tool architecture comprising an index of code examples. A query from a user is used to retrieve code examples, and the query and code examples are sent to an LLM to generate code corresponding to the query.
1 . A method, comprising:
receiving an input query from a user prompt;
sending the input query to a large language model (LLM);
receiving, from the LLM, an initial representation of the input query;
performing, based on the initial representation, a lookup on an index storing a plurality of entries, wherein each of the plurality of entries in the index follows a domain specific code syntax, and performing the lookup comprises:
retrieving, from the index, a plurality of relevant entries based on the initial representation; and
ranking the plurality of relevant entries according to how each entry matches the input query;
supplementing the input query with at least some of the plurality of relevant entries, including:
determining that a token count of the input query plus a token count of the plurality of relevant entries exceeds an allowed token window of the LLM;
selecting, from the plurality of relevant entries and in accordance with the ranking, a subset of the plurality of relevant entries such that a combined token count of the input query and the subset does not exceed the allowed token window of the LLM; and
combining the input query and the subset of the plurality of relevant entries to generate a supplemented input query:
sending the supplemented input query to the LLM;
receiving, from the LLM, a response corresponding to the supplemented input query; and
presenting the response on a graphical user interface.
2 . The method of claim 1 , wherein the response includes software code that follows the domain specific code syntax.
3 . The method of claim 1 , further comprising:
receiving, from the graphical user interface, an acceptance of the response; and
saving the response along with the input query in the index based on the acceptance.
4 . The method of claim 1 , wherein the lookup on the index is based on at least one field in the initial representation.
5 . The method of claim 4 , wherein the at least one field is a query field, a context field, an instructions field, a module field, a generated response field, an accepted response field, a contributor field, or an ID field.
6 . The method of claim 5 , wherein each of the plurality of entries includes the at least one field.
7 . The method of claim 6 , wherein the plurality of entries includes a code snippet, an API reference, or a code example.
8 . The method of claim 1 , wherein performing the lookup comprises:
generating a vectorized query from the initial representation.
9 . The method of claim 1 , wherein the subset of the plurality of relevant entries comprises highest-ranked entries admitted in rank order according to how each entry matches the input query until adding a further entry would exceed the allowed token window.
10 . A system comprising:
one or more processors;
a non-transitory computer-readable medium storing a program executable by the one or more processors, the program comprising sets of instructions for:
receiving an input query from a user prompt;
sending the input query to a large language model (LLM);
receiving, from the LLM, an initial representation of the input query;
performing, based on the initial representation, a lookup on an index storing a plurality of entries, wherein each of the plurality of entries in the index follows a domain specific code syntax, and performing the lookup comprises:
retrieving, from the index, a plurality of relevant entries based on the initial representation; and
ranking the plurality of relevant entries according to how each entry matches the input query;
supplementing the input query with at least some of the plurality of relevant entries, including:
determining that a token count of the input query plus a token count of the plurality of relevant entries exceeds an allowed token window of the LLM;
selecting, from the plurality of relevant entries and in accordance with the ranking, a subset of the plurality of relevant entries such that a combined token count of the input query and the subset does not exceed the allowed token window of the LLM; and
combining the input query and the subset of the plurality of relevant entries to generate a supplemented input query;
sending the supplemented input query to the LLM;
receiving, from the LLM, a response corresponding to the supplemented input query; and
presenting the response on a graphical user interface.
11 . The system of claim 10 , wherein the response includes software code that follows the domain specific code syntax.
12 . The system of claim 10 , wherein the program further comprises sets of instructions for:
receiving, from the graphical user interface, an acceptance of the response; and
saving the response along with the input query in the index based on the acceptance.
13 . The system of claim 10 , wherein the lookup on the index is based on at least one field in the initial representation.
14 . The system of claim 13 , wherein the at least one field is a query field, a context field, an instructions field, a module field, a generated response field, an accepted response field, a contributor field, or an ID field.
15 . The system of claim 10 , wherein performing the lookup comprises:
generating a vectorized query from the initial representation.
16 . A non-transitory computer-readable medium storing a program executable by one or more processors, the program comprising sets of instructions for:
receiving an input query from a user prompt;
sending the input query to a large language model (LLM);
receiving, from the LLM, an initial representation of the input query;
performing, based on the initial representation, a lookup on an index storing a plurality of entries, wherein each of the plurality of entries in the index follows a domain specific code syntax, and performing the lookup comprises:
retrieving, from the index, a plurality of relevant entries based on the initial representation; and
ranking the plurality of relevant entries according to how each entry matches the input query;
supplementing the input query with at least some of the plurality of relevant entries, including:
determining that a token count of the input query plus a token count of the plurality of relevant entries exceeds an allowed token window of the LLM;
selecting, from the plurality of relevant entries and in accordance with the ranking, a subset of the plurality of relevant entries such that a combined token count of the input query and the subset does not exceed the allowed token window of the LLM; and
combining the input query and the subset of the plurality of relevant entries to generate a supplemented input query;
sending the supplemented input query to the LLM;
receiving, from the LLM, a response corresponding to the supplemented input query; and
presenting the response on a graphical user interface.
17 . The non-transitory computer-readable medium of claim 16 , wherein the program further comprises sets of instructions for:
receiving, from the graphical user interface, an acceptance of the response; and
saving the response along with the input query in the index based on the acceptance.
18 . The non-transitory computer-readable medium of claim 16 , wherein the lookup on the index is based on at least one field in the initial representation.
19 . The non-transitory computer-readable medium of claim 18 , wherein the at least one field is a query field, a context field, an instructions field, a module field, a generated response field, an accepted response field, a contributor field, or an ID field.
20 . The non-transitory computer-readable medium of claim 16 , wherein performing the lookup comprises:
generating a vectorized query from the initial representation.