diff --git a/Src/Kernel/FormulaPy/formula.ipynb b/Src/Kernel/FormulaPy/formula.ipynb index 923c13b..32511b0 100644 --- a/Src/Kernel/FormulaPy/formula.ipynb +++ b/Src/Kernel/FormulaPy/formula.ipynb @@ -2,48 +2,203 @@ "cells": [ { "cell_type": "code", - "execution_count": null, + "execution_count": 1, "id": "f1ef8032-ecf3-46f0-9af2-564c8e047e29", "metadata": {}, - "outputs": [], + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Successfully initialized formula.\n" + ] + } + ], "source": [ "%load_ext formula" ] }, { "cell_type": "code", - "execution_count": null, + "execution_count": 2, "id": "6b368acc-9353-45e3-8e52-7fe54c5b087f", "metadata": {}, - "outputs": [], + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "(Compiled) InvalidBatteryChecker.4ml\r\n", + "0.59s.\r\n", + "[]> \n" + ] + } + ], "source": [ - "%load /home/stephen/git/formula/Tst/Tests/Symbolic/MappingExample.4ml" + "%load C:\\Users\\sajtt\\Documents\\InvalidBatteryChecker.4ml" ] }, { "cell_type": "code", - "execution_count": null, + "execution_count": 3, "id": "cbb40c73-5c52-42fa-9786-a07d501786d3", "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Parsing text took: 0\r\n", + "Visiting text took: 0\r\n", + "Started solve task with Id 0.\r\n", + "0.32s.\r\n", + "[]> \n" + ] + } + ], + "source": [ + "%solve invalidBatteryPartialModel 1 BatteryChecker.conforms" + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "id": "32107a2e", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Model not solvable. No unsat core terms generated.\r\n", + "0.00s.\r\n", + "[]> \n" + ] + } + ], + "source": [ + "%extract 0 0 0" + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "id": "b3fed9f2", + "metadata": {}, "outputs": [], "source": [ - "%solve pm 1 Mapping.conforms" + "explain_prompt = \"Given the following Formula DSL program modeling a physical drone,\\\n", + " explain what the invalidBatteryPartialModel partial model is modeling \\\n", + " and give detailed solutions that would decrease the battery consumption in the invalidBatteryPartialModel.\\\n", + " Put the solutions in a list.\"" ] }, { "cell_type": "code", - "execution_count": null, + "execution_count": 6, "id": "aaecf243-7534-4355-908e-375fd02db84f", "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Running executor...\n", + "\n", + "\n", + "\u001b[1m> Entering new AgentExecutor chain...\u001b[0m\n" + ] + }, + { + "name": "stderr", + "output_type": "stream", + "text": [ + "Failed to post https://api.smith.langchain.com/runs in LangSmith API. 401 Client Error: Unauthorized for url: https://api.smith.langchain.com/runs\n", + "{\"detail\":\"Invalid auth\"}\n" + ] + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "\u001b[32;1m\u001b[1;3mThe invalidBatteryPartialModel is modeling a drone mission with a battery that has an unknown capacity (represented by the variable x). The model includes the components of the drone (payload and body) and the locations for each mission item. It also includes the mission items themselves, which consist of a label, source and destination locations, distance, and velocity.\n", + "\n", + "The problem with the invalidBatteryPartialModel is that it does not specify a valid battery capacity. This makes it impossible to calculate the energy consumption and check if the battery capacity is exceeded. To fix this, we need to provide a valid battery capacity value.\n", + "\n", + "Solutions to decrease battery consumption in the invalidBatteryPartialModel:\n", + "1. Optimize the drone's flight path: By optimizing the flight path, the drone can minimize the distance traveled and reduce the overall energy consumption.\n", + "2. Reduce the payload weight: The payload weight directly affects the energy consumption of the drone. By reducing the payload weight, the battery consumption can be decreased.\n", + "3. Improve the drone's efficiency: This can be achieved by using more efficient components and technologies, such as lightweight materials, efficient motors, and aerodynamic designs.\n", + "4. Adjust the drone's velocity: By adjusting the drone's velocity based on the mission requirements, the energy consumption can be optimized. Slower velocities generally result in lower energy consumption.\n", + "5. Implement energy-saving algorithms: Use algorithms that optimize the drone's flight path and energy consumption, taking into account factors such as wind conditions, altitude, and mission requirements.\n", + "6. Increase the battery capacity: If the current battery capacity is insufficient for the mission, consider upgrading to a higher capacity battery to ensure sufficient power for the entire mission.\n", + "\n", + "Note: The specific solutions may vary depending on the requirements and constraints of the drone mission.\u001b[0m\n", + "\n", + "\u001b[1m> Finished chain.\u001b[0m\n" + ] + } + ], + "source": [ + "%explain --explain-prompt \"$explain_prompt\"" + ] + }, + { + "cell_type": "code", + "execution_count": 13, + "id": "ac31c0b2", + "metadata": {}, "outputs": [], "source": [ - "%explain" + "repair_prompt = \"Repair the invalidBatteryPartialModel by reducing the payload1 and body component weights \\\n", + " so that the sum of the missionConsumptions will be below the batteryCapacity. Edit the code and enclose in triple backticks.\"" + ] + }, + { + "cell_type": "code", + "execution_count": 14, + "id": "50f00b79", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Running repair...\n", + "\n", + "\n", + "\u001b[1m> Entering new AgentExecutor chain...\u001b[0m\n", + "\u001b[32;1m\u001b[1;3mThe invalidBatteryPartialModel is not solvable because the sum of the missionConsumptions exceeds the batteryCapacity. To fix this, we need to reduce the weights of the payload1 and body components so that the sum of the missionConsumptions will be below the batteryCapacity.\n", + "\n", + "Here is the corrected code:\n", + "\n", + "```formula\n", + "partial model invalidBatteryPartialModel of BatteryChecker\n", + "[solver_RecursionBound = 200]\n", + "{\n", + " Component(\"payload1\", 5). // Reduce the weight of payload1 to 5\n", + " Component(\"body\", 5). // Reduce the weight of body to 5\n", + " Battery(\"battery1\", 10, x).\n", + "\n", + " // Rest of the code remains the same\n", + " ...\n", + "}\n", + "```\n", + "\n", + "By reducing the weights of the payload1 and body components to 5, the sum of the missionConsumptions will be below the batteryCapacity and the model will be solvable.\u001b[0m\n", + "\n", + "\u001b[1m> Finished chain.\u001b[0m\n" + ] + } + ], + "source": [ + "%repair --repair-prompt \"$repair_prompt\"" ] }, { "cell_type": "code", "execution_count": null, - "id": "7a72c0a0-e898-4f08-9737-147725f20987", + "id": "031a42f0", "metadata": {}, "outputs": [], "source": [] @@ -65,7 +220,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.10.12" + "version": "3.10.13" } }, "nbformat": 4, diff --git a/Src/Kernel/FormulaPy/formula/__init__.py b/Src/Kernel/FormulaPy/formula/__init__.py index 67133f4..b0247b1 100644 --- a/Src/Kernel/FormulaPy/formula/__init__.py +++ b/Src/Kernel/FormulaPy/formula/__init__.py @@ -4,7 +4,7 @@ load("coreclr") import clr d = __file__.replace("__init__.py","") -clr.AddReference(d + "CommandLine/CommandLine.dll") +clr.AddReference(d + "CommandLine/VUISIS.Formula.x64.dll") from .formula_magic import FormulaMagics diff --git a/Src/Kernel/FormulaPy/formula/formula_agent.py b/Src/Kernel/FormulaPy/formula/formula_agent.py index 48c11fb..5b54835 100644 --- a/Src/Kernel/FormulaPy/formula/formula_agent.py +++ b/Src/Kernel/FormulaPy/formula/formula_agent.py @@ -4,11 +4,15 @@ from langchain.agents.openai_functions_agent.base import OpenAIFunctionsAgent from langchain.schema.messages import SystemMessage from langchain.memory import ConversationBufferMemory -from .formula_tools import DebugFormulaCodeLLM, LoadFormulaCode, QueryFormulaCode, DecodeFormulaCodeLLM +from .formula_tools import FormulaCodeLLM, RepairFormulaCodeLLM from .config import cfg -from .prompts import FIX_CODE_PREFIX, QUERY_PROMPT +from .prompts import FIX_CODE_PREFIX, REPAIR_CODE_PREFIX os.environ["OPENAI_API_KEY"] = cfg["OPENAI_API_KEY"] +#os.environ["OPENAI_API_TYPE"] = "azure" +#os.environ["OPENAI_API_VERSION"] = "2023-08-24" +#os.environ["OPENAI_API_BASE"] = "https://apim.app.vanderbilt.edu/openai-students/deployments/gpt-35-turbo/chat/completions?api-version=2023-08-24" + if cfg["LANGCHAIN_API_KEY"] != "": @@ -18,32 +22,51 @@ os.environ["LANGCHAIN_PROJECT"] ="pt-oily-sultan-99" -llm = ChatOpenAI(temperature=0, model="gpt-3.5-turbo-16k") +llm = ChatOpenAI(temperature=0, model_name="gpt-3.5-turbo-16k") system_message = SystemMessage(content=FIX_CODE_PREFIX) _prompt = OpenAIFunctionsAgent.create_prompt(system_message=system_message) -memory = ConversationBufferMemory(memory_key="chat_history", return_messages=True) -tools = [LoadFormulaCode, QueryFormulaCode, DecodeFormulaCodeLLM(llm=llm), DebugFormulaCodeLLM(llm=llm)] +repair_system_message = SystemMessage(content=REPAIR_CODE_PREFIX) +_repair_prompt = OpenAIFunctionsAgent.create_prompt(system_message=system_message) + +explain_tools = [FormulaCodeLLM(llm=llm)] agent = OpenAIFunctionsAgent( llm=llm, prompt=_prompt, - tools=tools, - memory=memory, + tools=explain_tools, verbose=True - ) +) agent_executor = AgentExecutor.from_agent_and_tools( agent=agent, - tools=tools, + tools=explain_tools, verbose=True, - ) - -def run_agent_executor(code, output, additional_details): - query = QUERY_PROMPT.format(code=code, interpreter_output=output) - if additional_details: - query += f"\n\nHere are some additional details to keep in mind when trying to figure \ -out what is wrong with the code:\n\n{additional_details}" - agent_executor.run(query) \ No newline at end of file +) + +repair_tools = [RepairFormulaCodeLLM(llm=llm)] + +agent_repair = OpenAIFunctionsAgent( + llm=llm, + prompt=_repair_prompt, + tools=repair_tools, + verbose=True +) + +agent_executor_repair = AgentExecutor.from_agent_and_tools( + agent=agent_repair, + tools=repair_tools, + verbose=True, +) + +def run_agent_executor(code, output, explain_prompt): + prompts = "{explain_prompt}\n\n{code}\n\n{output}".format(code=code, output=output, explain_prompt=explain_prompt) + prompts.encode('unicode_escape') + agent_executor.run(prompts) + +def run_agent_executor_repair(code, output, repair_prompt): + prompts = "{repair_prompt}\n\n{code}\n\n{output}".format(code=code, output=output, repair_prompt=repair_prompt) + prompts.encode('unicode_escape') + agent_executor_repair.run(prompts) \ No newline at end of file diff --git a/Src/Kernel/FormulaPy/formula/formula_magic.py b/Src/Kernel/FormulaPy/formula/formula_magic.py index c33d30c..6758cbd 100644 --- a/Src/Kernel/FormulaPy/formula/formula_magic.py +++ b/Src/Kernel/FormulaPy/formula/formula_magic.py @@ -1,13 +1,15 @@ from __future__ import print_function +from pickle import TRUE from IPython.core.magic import (Magics, magics_class, line_magic) +from IPython.core.magic_arguments import (argument, magic_arguments, parse_argstring) -from pathlib import Path +import re, os from Microsoft.Formula.CommandLine import CommandInterface, CommandLineProgram from System.IO import StringWriter from System import Console -from .formula_agent import run_agent_executor +from .formula_agent import run_agent_executor, run_agent_executor_repair @magics_class class FormulaMagics(Magics): @@ -15,12 +17,14 @@ class FormulaMagics(Magics): def __init__(self, shell, data=None): super(FormulaMagics, self).__init__(shell) self.sw = StringWriter() - self.total_sw_output = "" + self.total_sw_output = "END" Console.SetOut(self.sw) Console.SetError(self.sw) - self.file = None - self.explain = False - + self.file_txt = None + self.explain_ran = False + self.solve_ran = False + self.repair_ran = False + sink = CommandLineProgram.ConsoleSink() chooser = CommandLineProgram.ConsoleChooser() self.ci = CommandInterface(sink, chooser) @@ -29,37 +33,37 @@ def __init__(self, shell, data=None): print("Successfully initialized formula.") @line_magic - def help(self): + def help(self, line): print("Formula magic commands:") - print("%load filepath - Loads and compiles a file that is not yet loaded. Use: load filepath.") - print("%help - Prints this message.") - print("%ls - Lists environment objects. Use: ls [vars | progs | tasks]") - print("%extract - Extract and install a result. Use: extract (app_id | solv_id n) output_name [render_class render_dll]") - print("%query - Start a query task. Use: query model goals") - print("%solve - Start a solve task. Use: solve partial_model max_sols goals") - print("%explain - Runs an LLM to generate an explaination for the solution.") - print("%repair - Runs an LLM to repair the loaded formula DSL program.") - print("%set - Sets a variable. Use: set var term.") - print("%delete - Deletes a variable. Use: del var.") - print("%save - Saves the module modname into file.") - print("%unload - Unloads an installed program and all dependent programs. Use: unload [prog | *]") - print("%tunload - Unloads a task. Use: tunload [id | *]") - print("%reload - Reloads an installed program and all dependent programs. Use: reload [prog | *]") - print("%print - Prints the installed program with the given name. Use: print progname") - print("%det - Prints details about the compiled module with the given name. Use: det modname") - print("%types - Prints inferred variable types. Use: types modname") - print("%render - Tries to render the module. Use: render modname") - print("%verbose - Changes verbosity. Use: verbose (on | off)") - print("%wait - Changes waiting behavior. Use: wait (on | off) to block until task completes") - print("%apply - Start an apply task. Use: apply transformstep") - print("%stats - Prints task statistics. Use: stats task_id [top_k_rule]") - print("%generate - Generate C# data model. Use: generate modname") - print("%truth - Test if a ground term is derivable under a model/apply. Use: truth task_id [term]") - print("%proof - Enumerate proofs that a ground term is derivable under a model/apply. Use: proof task_id [term]") - print("%confhelp - Provides help about module configurations and settings") - print("%watch - Use: watch [off | on | prompt] to control watch behavior") - print("%core - Prints reduced rule set for domains / transforms. Use: core module_name") - print("%downgrade - Attempts to downgrade a (partial) model to Formula V1. Use: downgrade module_name") + print("%load (l) - Loads and compiles a file that is not yet loaded. Use: load filepath.") + print("%help (h) - Prints this message.") + print("%list (ls) - Lists environment objects. Use: ls [vars | progs | tasks]") + print("%extract (ex) - Extract and install a result. Use: extract (app_id | solv_id n) output_name [render_class render_dll]") + print("%query (qr) - Start a query task. Use: query model goals") + print("%solve (sl) - Start a solve task. Use: solve partial_model max_sols goals") + print("%explain (exp) - Runs an LLM to generate an explaination for the solution. Use: exp solv_id prompt") + print("%repair (rep) - Runs an LLM to repair the loaded formula DSL program. Use: rep solv_id") + print("%set (s) - Sets a variable. Use: set var term.") + print("%delete (d) - Deletes a variable. Use: del var.") + print("%save (sv) - Saves the module modname into file.") + print("%unload (ul) - Unloads an installed program and all dependent programs. Use: unload [prog | *]") + print("%tunload (tul) - Unloads a task. Use: tunload [id | *]") + print("%reload (rl) - Reloads an installed program and all dependent programs. Use: reload [prog | *]") + print("%print (p) - Prints the installed program with the given name. Use: print progname") + print("%det (dt) - Prints details about the compiled module with the given name. Use: det modname") + print("%types (typ) - Prints inferred variable types. Use: types modname") + print("%render (r) - Tries to render the module. Use: render modname") + print("%verbose (v) - Changes verbosity. Use: verbose (on | off)") + print("%wait (w) - Changes waiting behavior. Use: wait (on | off) to block until task completes") + print("%apply (ap) - Start an apply task. Use: apply transformstep") + print("%stats (st) - Prints task statistics. Use: stats task_id [top_k_rule]") + print("%generate (gn) - Generate C# data model. Use: generate modname") + print("%truth (tr) - Test if a ground term is derivable under a model/apply. Use: truth task_id [term]") + print("%proof (pr) - Enumerate proofs that a ground term is derivable under a model/apply. Use: proof task_id [term]") + print("%confhelp (ch) - Provides help about module configurations and settings") + print("%watch (wch) - Use: watch [off | on | prompt] to control watch behavior") + print("%core (cr) - Prints reduced rule set for domains / transforms. Use: core module_name") + print("%downgrade (dg) - Attempts to downgrade a (partial) model to Formula V1. Use: downgrade module_name") def run_command(self, cmd, args=None): line = "" @@ -72,155 +76,280 @@ def run_command(self, cmd, args=None): temp_str = self.sw.ToString() if cmd == "extract": - self.total_sw_output += temp_str - elif cmd == "load" and self.file != None: - f = open(self.file.absolute(), 'r') - self.total_sw_output += f.read() - f.close() + self.total_sw_output = temp_str + self.sw.GetStringBuilder().Clear() print(temp_str) @line_magic - def load(self, line=None): - if line == None: - print("No 4ml file passed to load.") + def load(self, line): + if self.file_txt != None: + print("A Formula DSL program is already loaded.") return - file = Path(line) - if file.is_file(): - self.run_command("load", file.absolute()) - self.file = file + file = os.path.abspath(line) + if os.path.isfile(file): + f = open(file, 'r') + try: + self.file_txt = f.read() + finally: + f.close() + self.run_command("load", file) return print("File is invalid or does not exist.") + + @line_magic + def l(self, line): + self.load(line) @line_magic - def ls(self): - self.run_command("ls") + def list(self, line): + self.run_command("list", line) + + @line_magic + def ls(self, line): + self.list(line) @line_magic - def extract(self, line=None): + def extract(self, line): self.run_command("extract", line) + + @line_magic + def ex(self, line): + self.extract_ran(line) @line_magic - def query(self, line=None): + def query(self, line): self.run_command("query", line) + + @line_magic + def qr(self, line): + self.query(line) @line_magic - def solve(self, line=None): - if self.file == None: + def solve(self, line): + if self.file_txt == None: print("Load 4ml file to proceed.") return self.run_command("solve", line) - + self.solve_ran = True + + @line_magic + def sl(self, line): + self.solve(line) + + @magic_arguments() + @argument( + "--explain-prompt", + "-ep", + required=True, + help=("Input explain prompt."), + ) @line_magic - def explain(self, line=None): - if self.file == None: + def explain(self, line): + if self.file_txt == None: print("Load 4ml file to proceed.") return - f = open(self.file, 'r') - txt = "" - try: - txt = f.read() - finally: - f.close() - + + args = parse_argstring(self.explain, line) + print('Running executor...') - run_agent_executor(txt, self.total_sw_output, line) - self.explain = True + run_agent_executor(self.file_txt, self.total_sw_output, args.explain_prompt) + self.explain_ran = True + + @line_magic + def exp(self, line): + self.explain(line) + @magic_arguments() + @argument( + "--repair-prompt", + "-rp", + required=True, + help=("Input repair prompt."), + ) @line_magic - def repair(self): - if self.explain: - print("Repair") + def repair(self, line): + if self.explain_ran: + print('Running repair...') + + args = parse_argstring(self.repair, line) + + run_agent_executor_repair(self.file_txt, self.total_sw_output, args.repair_prompt) else: - print("Run explain first") - + print("Run explain magic function first.") + @line_magic - def explain_and_repair(self): - print("Explain and repair.") + def rep(self, line): + self.repair(line) @line_magic - def set(self, line=None): + def set(self, line): self.run_command("set", line) + + @line_magic + def s(self, line): + self.set(line) @line_magic - def delete(self, line=None): + def delete(self, line): self.run_command("del", line) + + @line_magic + def d(self, line): + self.delete(line) @line_magic - def unload(self, line=None): - self.file = None + def unload(self, line): + self.file_txt = None + self.total_sw_output = "END" self.run_command("unload", line) + + @line_magic + def ul(self, line): + self.unload(line) @line_magic - def tunload(self, line=None): + def tunload(self, line): self.run_command("tunload", line) @line_magic - def reload(self): + def tul(self, line): + self.tunload(line) + + @line_magic + def reload(self, line): self.run_command("reload") + + @line_magic + def rl(self, line): + self.reload() @line_magic - def save(self, line=None): + def save(self, line): self.run_command("save", line) + + @line_magic + def sv(self, line): + self.save(line) @line_magic - def print(self, line=None): + def print(self, line): self.run_command("print", line) + + @line_magic + def p(self, line): + self.print(line) @line_magic - def det(self, line=None): + def det(self, line): self.run_command("det", line) + + @line_magic + def dt(self, line): + self.det(line) @line_magic - def render(self, line=None): + def render(self, line): self.run_command("render", line) + + @line_magic + def r(self, line): + self.render(line) @line_magic - def verbose(self, line=None): + def verbose(self, line): self.run_command("verbose", line) + + @line_magic + def v(self, line): + self.verbose(line) @line_magic - def wait(self, line=None): + def wait(self, line): self.run_command("wait", line) @line_magic - def watch(self, line=None): + def w(self, line): + self.wait(line) + + @line_magic + def watch(self, line): self.run_command("watch", line) @line_magic - def types(self, line=None): + def wch(self, line): + self.watch(line) + + @line_magic + def types(self, line): self.run_command("type", line) @line_magic - def truth(self, line=None): + def typ(self, line): + self.types(line) + + @line_magic + def truth(self, line): self.run_command("truth", line) + + @line_magic + def tr(self, line): + self.truth(line) @line_magic - def proof(self, line=None): + def proof(self, line): self.run_command("proof", line) + + @line_magic + def pr(self, line): + self.proof(line) @line_magic - def apply(self, line=None): + def apply(self, line): self.run_command("apply", line) + + @line_magic + def ap(self, line): + self.apply(line) @line_magic - def stats(self, line=None): + def stats(self, line): self.run_command("stats", line) + + @line_magic + def st(self, line): + self.stats(line) @line_magic - def generate(self, line=None): + def generate(self, line): self.run_command("generate", line) + + @line_magic + def gn(self, line): + self.generate(line) @line_magic - def confhelp(self, line=None): + def confhelp(self, line): self.run_command("confhelp", line) + + @line_magic + def ch(self, line): + self.confhelp(line) @line_magic - def core(self, line=None): + def core(self, line): self.run_command("core", line) + + @line_magic + def cr(self, line): + self.core(line) @line_magic - def downgrade(self, line=None): + def downgrade(self, line): self.run_command("downgrade", line) + + @line_magic + def dg(self, line): + self.downgrade(line) diff --git a/Src/Kernel/FormulaPy/formula/formula_tools.py b/Src/Kernel/FormulaPy/formula/formula_tools.py index 895b954..67b1e68 100644 --- a/Src/Kernel/FormulaPy/formula/formula_tools.py +++ b/Src/Kernel/FormulaPy/formula/formula_tools.py @@ -7,140 +7,42 @@ from langchain.chains import SequentialChain from langchain.tools.base import BaseTool from .prompts import ( - DEBUG_FORMULA_CODE_LLM_DESC, - DEBUG_FORMULA_CODE_LLM_PROMPT, - DEBUG_FORMULA_CODE_LLM_RETURN, - DECODE_FORMULA_CODE_EXPLAIN_PROMPT, - DECODE_FORMULA_CODE_LLM_DESC, - DECODE_FORMULA_CODE_LLM_RETURN, - DECODE_FORMULA_CODE_PAINPOINTS_PROMPT, - LOAD_FORMULA_CODE, - QUERY_FORUMULA_CODE + EXPLAIN_QUERY_PROMPT, + REPAIR_OUTPUT_RETURN, + OUTPUT_RETURN, + REPAIR_QUERY_PROMPT, + FORMULA_CODE_LLM_DESC, + REPAIR_FORMULA_CODE_LLM_DESC ) from langchain import LLMChain, PromptTemplate from langchain.tools import BaseTool, Tool -from Microsoft.Formula.CommandLine import CommandInterface, CommandLineProgram -from System.IO import StringWriter -from System import Console - -sink = CommandLineProgram.ConsoleSink() -chooser = CommandLineProgram.ConsoleChooser() -ci = CommandInterface(sink, chooser) - -sw = StringWriter() -Console.SetOut(sw) -Console.SetError(sw) - -if not ci.DoCommand("wait on"): - raise Exception("Wait on command failed.") - -if not ci.DoCommand("unload *"): - raise Exception("Unload command failed.") - - -def _LoadFormulaCode(query: str): - # Put the query string into a file ./temp.4ml - with open("./temp.4ml", "w") as f: - f.write(query) - - # Load the file into the FORMULA program - if not ci.DoCommand("unload"): - raise Exception("Unload command failed.") - - if not ci.DoCommand("load ./temp.4ml"): - raise Exception("Load command failed.") - - output = sw.ToString() - sw.GetStringBuilder().Clear() - - # if output contains the word "failed" case insensitive return false - if "failed" in output.lower(): - return f"Failed to load FORMULA code, you probably have an syntax error in your code. \ - Please check your code and try again.\n\nHere is the output from the FORMULA program:\n{output}" - - return "Successfully loaded FORMULA code, make sure that you now query the code using \ - the QueryFormulaCode tool to assert that the code is working as expected now." - - -LoadFormulaCode = Tool.from_function( - func=_LoadFormulaCode, name="LoadFormulaCode", description=LOAD_FORMULA_CODE -) - - -def _QueryFormulaCode(query: str): - sw.GetStringBuilder().Clear() - if not ci.DoCommand(query): - raise Exception("Query command failed.") - - output = sw.ToString() - sw.GetStringBuilder().Clear() - - if "not solvable" in output.lower(): - return f""" \ -Your code is not solvable. This means that the code is broken and you need to fix it. -Here was the output from the FORMULA program: - -{output} - -Make sure to try to regenerate your code, using the DebugFormulaCodeLLM tool if needed, and then re run the program again -using the LoadFormulaCode tool / QueryFormulaCode Formula REPL tools. -""" - - return output - - -QueryFormulaCode = Tool.from_function( - func=_QueryFormulaCode, name="QueryFormulaCode", description=QUERY_FORUMULA_CODE -) - - -class DecodeFormulaCodeLLM(BaseTool): - name = "DecodeFormulaCodeLLM" - description = DECODE_FORMULA_CODE_LLM_DESC +class FormulaCodeLLM(BaseTool): + name = "FormulaCodeLLM" + description = FORMULA_CODE_LLM_DESC llm: BaseChatModel - def _run( - self, - query: str = None, - run_manager: Optional[CallbackManagerForToolRun] = None, - **kwargs, - ) -> Any: - parsed_code = kwargs - code = parsed_code["code"] - interpreter_output = parsed_code["interpreter_output"] - - code_description_template = DECODE_FORMULA_CODE_EXPLAIN_PROMPT + def _run(self, **kwargs) -> Any: + explain_prompt = kwargs["explain_prompt"] + code = kwargs["code"] + output = kwargs["output"] - code_painpoints_template = DECODE_FORMULA_CODE_PAINPOINTS_PROMPT + explain_template = EXPLAIN_QUERY_PROMPT + solutions_template = SOLUTIONS_QUERY_PROMPT + prompt_template = PromptTemplate( - input_variables=["code", "interpreter_output"], - template=code_description_template, + input_variables=["explain_prompt", "code", "output"], + template=explain_template, ) + code_understander_chain = LLMChain( llm=self.llm, prompt=prompt_template, output_key="explanation" ) - prompt_template = PromptTemplate( - input_variables=["code", "interpreter_output", "explanation"], - template=code_painpoints_template, - ) - painpoints_chain = LLMChain( - llm=self.llm, prompt=prompt_template, output_key="pain_points" - ) - - overall_chain = SequentialChain( - chains=[code_understander_chain, painpoints_chain], - input_variables=["code", "interpreter_output"], - # Here we return multiple variables - output_variables=["explanation", "pain_points"], - verbose=True, - ) - - output = overall_chain(parsed_code) + out = code_understander_chain(kwargs) - return_output = DECODE_FORMULA_CODE_LLM_RETURN.format(output=output['explanation']) + return_output = OUTPUT_RETURN.format(explanation=out['explanation']) return return_output @@ -149,19 +51,30 @@ async def _arun( ): raise NotImplementedError("custom_search does not support async") - -class DebugFormulaCodeLLM(BaseTool): - name = "DebugFormulaCodeLLM" - description = DEBUG_FORMULA_CODE_LLM_DESC +class RepairFormulaCodeLLM(BaseTool): + name = "RepairFormulaCodeLLM" + description = REPAIR_FORMULA_CODE_LLM_DESC llm: BaseChatModel def _run(self, **kwargs) -> Any: - parsed_code = kwargs - prompt = DEBUG_FORMULA_CODE_LLM_PROMPT.format(**parsed_code) + repair_prompt = kwargs["repair_prompt"] + code = kwargs["code"] + output = kwargs["output"] + + repair_template = REPAIR_QUERY_PROMPT - output = self.llm.predict(prompt) + prompt_template = PromptTemplate( + input_variables=["repair_prompt", "code", "output"], + template=repair_template, + ) + + repair_chain = LLMChain( + llm=self.llm, prompt=prompt_template, output_key="repair" + ) + + out = repair_chain(kwargs) - return_output = DEBUG_FORMULA_CODE_LLM_RETURN.format(output=output) + return_output = REPAIR_OUTPUT_RETURN.format(repair=out['repair']) return return_output diff --git a/Src/Kernel/FormulaPy/formula/prompts.py b/Src/Kernel/FormulaPy/formula/prompts.py index 6188127..004f6fd 100644 --- a/Src/Kernel/FormulaPy/formula/prompts.py +++ b/Src/Kernel/FormulaPy/formula/prompts.py @@ -1,326 +1,65 @@ FIX_CODE_PREFIX = """ \ - SYSTEM MESSAGE: -You are an agent designed to read, write, execute, and more importantly fix and \ -be able to execute FORMULA code. - -Formula is a novel formal specification language based on open-world logic programs -and behavioral types. Its goals are (1) succinct specifications of domain-specific abstractions -and compilers, (2) efficient reasoning and compilation of input programs, (3) diverse syn- -thesis and fast verification. It takes a unique approach towards achieving these goals: -Specifications are written as strongly-typed open-world logic programs. They are highly -declarative and easily express rich synthesis / verification problems. Automated reason- -ing is enabled by efficient symbolic execution of logic programs into constraints. The language -is similar to datalog, and can help one model DSL (domain specific languages). - -You have access to a Formula REPL, which you can use to evaluate FORMULA code. -If you get an error, debug your code and try again. -You might know the answer without running any code, but you should still run the code to get the answer. -If it does not seem like you can write code to answer the question, just return "I don't know" as the answer. - -FORMULA code may be broken when there are constraints that are conflicting with each other, for example there \ -is one constraint that states x < 0 and x > 0, which would make it impossible for a possible x to exist. Your first goal \ -is given the code try to understand what the code is doing. You can do this by invoking the decode formula code tool. \ - -Then after that you are tasked to figure out given the error messages given by the FORMULA interpreter to figure out \ -what are some of the possible statements that might be broken, after that your next goal is to fix those broken parts of the code. \ +You will be provided a Formula DSL program and unsat core (delimited with XML tags labelled code). You will explain why the program is broken and give solutions to fixing it. -After that you have to load the code into FORMULA using the load formula code tool, then after that you \ -are tasked with querying the formula code using the query formula code tool. Inspect the results, if no error message \ -comes out then you are finished and respond with what you have found, but if an error message comes out then restart \ -your progress and further debug the code. \ +END OF SYSTEM MESSAGE""" -END OF SYSTEM MESSAGE - - -""" - -LOAD_FORMULA_CODE = """ \ -This is a Formula Loading tool. Use this tool to load your FORMULA code into the FORMULA program -(this much be done before you and execute any queries on your FORMULA code) -Input must be valid FORMULA code. -""" - -QUERY_FORUMULA_CODE = """ \ -This is a Formula querying tool. Use this tool to query your loaded FORMULA code -Use this tool by invoking it with a just a singular FORMULA query. - - -Below, delimited by ```, is an example of some commands that you can use. -``` -solve pm 1 Mapping.conforms // Try to complete the partial model named pm -ex 0 1 out.4ml // Extract and print the 1st solution from solve task 0 -query m badMapping // Does model m have a badMapping? -list // lists out all tasks -pr 0 //Show a proof for task 0 -help //displays available commands -``` -""" - -DECODE_FORMULA_CODE_LLM_DESC = """ \ -This is a Formula Decoding Tool. Use this tool to decode what the FORMULA code does, then further \ -this tool will identify where the issues are in the code, and it would generate possible solutions \ -to fix the code. +REPAIR_CODE_PREFIX = """ \ +SYSTEM MESSAGE: -Make sure to use this tool before trying to fix the code, as you need to figure out what the code does first \ -and think up of different ways we can try to fix the code. +You will be provided a Formula DSL program and unsat core (delimited with XML tags labelled code). You will give repairs of the code in the Formula DSL language enclosed in triple backticks. -To invoke this tool, make sure you call it in a JSON format in the following format: +END OF SYSTEM MESSAGE""" -{ - "code": "FORMULA CODE HERE", - "interpreter_output": "FORMULA INTERPRETER OUTPUT HERE", -} +EXPLAIN_QUERY_PROMPT = """ \ +{explain_prompt} -Make sure you only call this function with a JSON format, otherwise it will not work. -And make sure you include both the formula code and the formula interpreter output. -""" +{code} -# Deprecated -DECODE_FORMULA_CODE_LLM_PROMPT = """ \ -Please decode the following FORMULA code delimited by ``` into a natural language description. -``` -{code} -``` +{output} """ -DECODE_FORMULA_CODE_EXPLAIN_PROMPT = """ -You are a chatbot who is an expert at programming in Prolog and Formula, -designed to read FORMULA code, understand what the code does. The code is also going to be broken, -and you are tasked with trying to figure out how to fix it. - -Your goal is to describe what the code is exactly doing, and what each interpreter output is saying. - -Formula is a novel formal specification language based on open-world logic programs -and behavioral types. Its goals are (1) succinct specifications of domain-specific abstractions -and compilers, (2) efficient reasoning and compilation of input programs, (3) diverse syn- -thesis and fast verification. It takes a unique approach towards achieving these goals: -Specifications are written as strongly-typed open-world logic programs. They are highly -declarative and easily express rich synthesis / verification problems. Automated reason- -ing is enabled by efficient symbolic execution of logic programs into constraints. The language -is similar to datalog, and can help one model DSL (domain specific languages). +REPAIR_QUERY_PROMPT = """ \ +{repair_prompt} -Here is the code and interpreter output delimited by ``` +{code} -code: -``` -{code} -``` - -interpreter output: -``` -{interpreter_output} -``` +{output} """ -DECODE_FORMULA_CODE_PAINPOINTS_PROMPT = """ -You are a chatbot who is an expert at programming in Prolog and Formula, -designed to read FORMULA code, understand what the code does. The code is also going to be broken, -and you are tasked with trying to figure out how to fix it. - -You will be given the code, the interpreter output, and an example of what the code is doing. -Your goal is to figure out where are all the possible places where the code is broken. - - -Formula is a novel formal specification language based on open-world logic programs -and behavioral types. Its goals are (1) succinct specifications of domain-specific abstractions -and compilers, (2) efficient reasoning and compilation of input programs, (3) diverse syn- -thesis and fast verification. It takes a unique approach towards achieving these goals: -Specifications are written as strongly-typed open-world logic programs. They are highly -declarative and easily express rich synthesis / verification problems. Automated reason- -ing is enabled by efficient symbolic execution of logic programs into constraints. The language -is similar to datalog, and can help one model DSL (domain specific languages). - -Here is the code and interpreter output delimited by ``` - -code: -``` -{code} -``` - -interpreter output: -``` -{interpreter_output} -``` - -what the code is doing: -``` +OUTPUT_RETURN = """ \ {explanation} -``` """ -# Below is a deprecated prompt for the return value - -# return_output = f""" \ -# Here is what the code is doing: {output['explanation']}\n\nHere are the possible places where we can \ -# fix the code: \ {output['pain_points']}. - -# Your next step now is to generate a piece of code implementing one of the example fixes, and then testing if the code -# actually works with running the FORMULA REPL. If the code works, then your job is done and you should return the code -# as well as an explanation of what the fixes you made were. If the code does not work, then you should try to debug the code. - -# Remember the above task is for YOU, the chatbot and master formula programmer to do. You, the chatbot, have access to the -# FORMULA repl commands with the LoadFormulaCode and QueryFormulaCode tools. You can also use the DecodeFormulaCodeLLM tool again if need be. -# """ - -DECODE_FORMULA_CODE_LLM_RETURN = """ \ -Here is what the code is doing: -{output} - -Your next step now is to generate a piece of code implementing one of the example fixes, and then testing if the code -actually works with running the FORMULA REPL. If the code works, then your job is done and you should return the code -as well as an explanation of what the fixes you made were. If the code does not work, then you should try to debug the code. - -Remember the above task is for YOU, the chatbot and master formula programmar to do. You, the chatbot, have access to the -FORMULA repl commands with the LoadFormulaCode and QueryFormulaCode tools. You can also use the DecodeFormulaCodeLLM tool again if need be. +REPAIR_OUTPUT_RETURN = """ \ +{repair} """ - -DEBUG_FORMULA_CODE_LLM_DESC = """ \ -This is a Formula debugging Tool. Use this tool to debugging your FORMULA code. -This tool is most useful when you are trying to generate a new FORMULA code, but your code \ -is not able to get loaded because of a syntax error. +FORMULA_CODE_LLM_DESC = """ \ +This is a Formula debugging tool. To invoke this tool, make sure you call it in a JSON format in the following format: { + "prompt": "FORMULA REQUEST HERE", "code": "FORMULA CODE HERE", - "interpreter_output": "FORMULA INTERPRETER OUTPUT HERE", + "output": "FORMULA INTERPRETER OUTPUT HERE" } Make sure you only call this function with a JSON format, otherwise it will not work. -And make sure you include both the formula code and the formula interpreter output. -""" - -DEBUG_FORMULA_CODE_LLM_PROMPT = """ \ -You are a chatbot who is an expert at programming in Prolog and Formula, -designed to read broken FORMULA code and understand what the error is. - -Formula is a novel formal specification language based on open-world logic programs -and behavioral types. Its goals are (1) succinct specifications of domain-specific abstractions -and compilers, (2) efficient reasoning and compilation of input programs, (3) diverse syn- -thesis and fast verification. It takes a unique approach towards achieving these goals: -Specifications are written as strongly-typed open-world logic programs. They are highly -declarative and easily express rich synthesis / verification problems. Automated reason- -ing is enabled by efficient symbolic execution of logic programs into constraints. The language -is similar to datalog, and can help one model DSL (domain specific languages). - -You will be given the code and the interpreter output. Your goal is to flesh out the debug message -and figure out what the error is. - -Some error messages might be because there is an error in the code and the model is not solvable. -Other errors might be syntactical errors where the code is not formatted properly. -Another error might be that you are using the code wrong (for example adding too many or too little variables to a function call). - -Here is the code that is broken: -``` -{code} -``` - -and the interpreter output: - -``` -{interpreter_output} -``` - -""" - -DEBUG_FORMULA_CODE_LLM_RETURN = """ \ -Here is some debugging information: {output}. - -Your next step now is to generate a piece of code implementing one of the example fixes, and then testing if the code -actually works with running the FORMULA REPL. If the code works, then your job is done and you should return the code -as well as an explanation of what the fixes you made were. If the code does not work, then you should try to debug the code. - -Remember the above task is for YOU, the chatbot and master formula programmer to do. You, the chatbot, have access to the -FORMULA repl commands with the LoadFormulaCode and QueryFormulaCode tools. You can also use the DecodeFormulaCodeLLM tool again if need be. -""" - -QUERY_PROMPT = """ \ -Can you explain why the following code delimited in ``` is not solvable? -Could you then try to fix the code? - -Here is the code: -``` -{code} -``` - -And here is what the FORMULA interpreter says: - -``` -{interpreter_output} -``` """ -SAMPLE_QUERY = """\ +REPAIR_FORMULA_CODE_LLM_DESC = """ \ +This is a Formula repair tool. -Can you explain why the following code delimited in ``` is not solvable? -Could you then try to fix the code? - -Here is the code: -``` -domain Mapping -{ - Component ::= new (id: Integer, utilization: Real). - Processor ::= new (id: Integer). - Mapping ::= new (c: Component, p: Processor). - - // The utilization must be > 0 - invalidUtilization1 :- c is Component, c.utilization <= 0. - invalidUtilization2 :- c is Component, c.utilization > 0. - - badMapping :- p is Processor, - s = sum(0.0, { c.utilization | - c is Component, Mapping(c, p) }), s > 100. - - conforms no badMapping, no invalidUtilization1, no invalidUtilization2. -} +To invoke this tool, make sure you call it in a JSON format in the following format: -partial model pm of Mapping { - c1 is Component(0, x). - c2 is Component(1, y). - p1 is Processor(0). - Mapping(c1, p1). - Mapping(c2, p1). + "prompt": "FORMULA REQUEST HERE", + "code": "FORMULA CODE HERE", + "output": "FORMULA INTERPRETER OUTPUT HERE" } -``` - -And here is what the FORMULA interpreter output is: - -``` -[]> solve pm 1 Mapping.conforms -Parsing text took: 1 -Visiting text took: 0 -Started solve task with Id 0. -0.06s. -[]> ls - -Environment variables - -Programs in file root - +-- / - | tmp_file.4ml - -Programs in env root - +-- / - -All tasks - Id | Kind | Status | Result | Started | Duration -----|-------|--------|--------|-------------------|---------- - 0 | Solve | Done | false | 7/14/2023 3:44 PM | 0.28s -0.02s. -[]> ex 0 1 out.4ml -Model not solvable. Unsat core terms below. -Conflicts: Mapping.invalidUtilization2 -Conflicts: Mapping.invalidUtilization1 - -0.01s. -``` - -The code seems to be broken because theres a conflict in some of the constraints, if you could try to make it so there -is no conflicts in the constraints that would be great. - -""" +Make sure you only call this function with a JSON format, otherwise it will not work. +""" \ No newline at end of file diff --git a/Src/Kernel/FormulaPy/setup.py b/Src/Kernel/FormulaPy/setup.py index b0360d2..2080d30 100644 --- a/Src/Kernel/FormulaPy/setup.py +++ b/Src/Kernel/FormulaPy/setup.py @@ -8,7 +8,5 @@ author_email='stephen.johnson@vanderbilt.edu', packages=['formula'], install_requires=['pythonnet','jupyter','langchain==0.0.239', "openai"], -# install_requires=['pythonnet','jupyter','xturing','langchain', "openai"] - py_modules=['formula.SelfRepairLLM'], - package_data={'formula': ['CommandLine/*'], 'formula': ['SelfRepairLLM/src/*.py']} + package_data={'formula': ['CommandLine/*']} ) \ No newline at end of file