Added real prompt templates for explanation

Author: hweichelt

src/explaidllm/cli/clingo_app.py

@@ -106,5 +106,5 @@ def main(self, control: clingo.Control, files: Sequence[str]) -> None:
 
         llm = OpenAIModel(ModelTag.GPT_4O_MINI)
         logger.info("Prompting Model")
-        response = llm.prompt_template(ExplainTemplate(program="", mus=mus))
+        response = llm.prompt_template(template=ExplainTemplate(program="", assumptions=ap.assumptions, mus=mus, unsatisfiable_constraints=ucs.values()))
         logger.info(f"Received Response:\n{response}")

src/explaidllm/llms/templates/explain.py

@@ -1,8 +1,9 @@
 """Basic Explanation Prompt Template"""
-
 from pathlib import Path
+from typing import Iterable, Set, Tuple
 
 from clingexplaid.mus.core_computer import UnsatisfiableSubset
+from clingo import Symbol
 
 from .base import Template
 
@@ -13,18 +14,23 @@
 class ExplainTemplate(Template):
     """Basic Explanation Prompt Template"""
 
-    def __init__(self, program: str, mus: UnsatisfiableSubset):
+    def __init__(self, program: str, assumptions: Set[Tuple[Symbol, bool]], mus: UnsatisfiableSubset, unsatisfiable_constraints: Iterable[str]):
         self._program: str = program
+        self._assumptions: Set[Tuple[Symbol, bool]] = assumptions
         self._mus: UnsatisfiableSubset = mus
+        self._unsatisfiable_constraints = unsatisfiable_constraints
 
     def compose_instructions(self) -> str:
         with open(Path(__file__).parent / PROMPT_FILE_INSTRUCTIONS, "r", encoding="utf-8") as prompt_file:
             prompt_template = prompt_file.read()
-        prompt = prompt_template.format()
+        prompt = prompt_template
         return prompt
 
     def compose_input(self) -> str:
         with open(Path(__file__).parent / PROMPT_FILE_INPUT, "r", encoding="utf-8") as prompt_file:
             prompt_template = prompt_file.read()
-        prompt = prompt_template.format(program=self._program, mus=self._mus)
+        p_assumptions = ", ".join([f"({str(a[0])},{a[1]})" for a in self._assumptions])
+        p_mus = ", ".join([f"({str(a.symbol)},{a.sign})" for a in self._mus.assumptions])
+        p_ucs = ", ".join([f"'{uc}'" for uc in self._unsatisfiable_constraints])
+        prompt = prompt_template.format(program=self._program, assumptions=p_assumptions, mus=p_mus, ucs=p_ucs)
         return prompt

src/explaidllm/llms/templates/prompt_templates/explain_input.txt

@@ -1 +1,7 @@
-This is a placeholder input. Just say "Hello World!" back
+User Input:
+{{
+    "program": "{program}",
+    "assumptions": [{assumptions}],
+    "mus": [{mus}],
+    "unsatisfiable_constraints": [{ucs}],
+}}

src/explaidllm/llms/templates/prompt_templates/explain_instructions.txt

@@ -1 +1,43 @@
-This is a placeholder instruction
+You are an expert debugger of Answer Set Programming. You will receive an ASP program that is unsatisfiable under a set
+of assumptions. In addition to the program rules and assumptions, you will receive a Minimal Unsatisfiable Subset (mus)
+of these assumptions that leads to the program becoming unsatisfiable. There will also be one or more unsatisfiable
+constraints provided, which are the ones from the program that fire to make it unsatisfiable.
+
+Your task is to provide a simple and short natural language explanation to the user that explains what the
+unsatisfiability is and why it occurs. Follow the structure of the examples below.
+
+EXAMPLE 1 START
+
+Input:
+{
+    "program": "
+        number(1..4).
+
+        sudoku(X,Y,V) :- initial(X,Y,V).
+        {sudoku(X,Y,N): number(N)}=1 :- number(X) ,number(Y).
+        cage(X1,Y1,X2,Y2) :- sudoku(X1,Y1,_), sudoku(X2,Y2,_),
+                             ((X1-1)/2)==((X2-1)/2),
+                             ((Y1-1)/2)==((Y2-1)/2).
+
+        :- sudoku(X,Y1,N), sudoku(X,Y2,N), Y1 != Y2.
+        :- sudoku(X1,Y,N), sudoku(X2,Y,N), X1 != X2.
+        :- cage(X1,Y1,X2,Y2), sudoku(X1,Y1,N), sudoku(X2,Y2,N), X1!=X2, Y1!=Y2.
+
+        #show sudoku/3.
+    ",
+    "assumptions": [("sudoku(1,1,1)", True), ("sudoku(3,2,2)", True), ("sudoku(2,3,4)", True), ("sudoku(4,3,4)", True)],
+    "mus": [("sudoku(2,3,4)", True), ("sudoku(4,3,4)", True)],
+    "unsatisfiable_constraints": [
+        ":- sudoku(X1,Y,N), sudoku(X2,Y,N), X1 != X2."
+    ]
+}
+Output:
+{
+    "explanation": "
+        The program is unsatisfiable because sudoku(2,3,4) and sudoku(4,3,4) trigger the constraint
+        ':- sudoku(X1,Y,N), sudoku(X2,Y,N), X1 != X2.' which prohibits having the same value N two times with the same Y
+        value.
+    "
+}
+
+EXAMPLE 1 END