Update app.py

app.py

@@ -1,38 +1,157 @@
 import spaces
+import re 
 import gradio as gr
 from transformers import AutoTokenizer, AutoModelForCausalLM, GenerationConfig
 import torch
 
 title = """# 🙋🏻‍♂️Welcome to🌟Tonic's🔮DeepSeekMath📉
-You can build with this endpoint using🔮DeepSeekMath📉. The demo is still a work in progress and we're looking forward to build downstream tasks that showcase outstanding mathematical reasoning. Have any ideas ? join us below !
+You can build with this endpoint using🔮DeepSeekMath📉 available here : [deepseek-ai/deepseek-math-7b-instruct](https://huggingface.co/deepseek-ai/deepseek-math-7b-instruct). We're using 🤖[introspector/unimath](https://huggingface.co/datasets/introspector/unimath) for cool examples, check it out below ! The demo is still a work in progress and we're looking forward to build downstream tasks that showcase outstanding mathematical reasoning. Have any ideas ? join us below !
 You can also use 🔮DeepSeekMath📉 by cloning this space. Simply click here: <a style="display:inline-block" href="https://huggingface.co/spaces/Tonic/Math?duplicate=true"><img src="https://img.shields.io/badge/-Duplicate%20Space-blue?labelColor=white&style=flat&logo=data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAABAAAAAQCAYAAAAf8/9hAAAAAXNSR0IArs4c6QAAAP5JREFUOE+lk7FqAkEURY+ltunEgFXS2sZGIbXfEPdLlnxJyDdYB62sbbUKpLbVNhyYFzbrrA74YJlh9r079973psed0cvUD4A+4HoCjsA85X0Dfn/RBLBgBDxnQPfAEJgBY+A9gALA4tcbamSzS4xq4FOQAJgCDwV2CPKV8tZAJcAjMMkUe1vX+U+SMhfAJEHasQIWmXNN3abzDwHUrgcRGmYcgKe0bxrblHEB4E/pndMazNpSZGcsZdBlYJcEL9Afo75molJyM2FxmPgmgPqlWNLGfwZGG6UiyEvLzHYDmoPkDDiNm9JR9uboiONcBXrpY1qmgs21x1QwyZcpvxt9NS09PlsPAAAAAElFTkSuQmCC&logoWidth=14" alt="Duplicate Space"></a></h3> 
 Join us : 🌟TeamTonic🌟 is always making cool demos! Join our active builder's 🛠️community 👻 [![Join us on Discord](https://img.shields.io/discord/1109943800132010065?label=Discord&logo=discord&style=flat-square)](https://discord.gg/GWpVpekp) On 🤗Huggingface: [TeamTonic](https://huggingface.co/TeamTonic) & [MultiTransformer](https://huggingface.co/MultiTransformer) Math with [introspector](https://huggingface.co/introspector) On 🌐Github: [Tonic-AI](https://github.com/tonic-ai) & contribute to🌟 [SciTonic](https://github.com/Tonic-AI/scitonic)🤗Big thanks to Yuvi Sharma and all the folks at huggingface for the community grant 🤗
 """
 
+unimath1 = """Goal:
+  
+  X : UU
+  Y : UU
+  P : UU
+  xp : (X → P) → P
+  yp : (Y → P) → P
+  X0 : X × Y → P
+  x : X
+  ============================
+   (Y → P)
+
+
+DEBUG:Going to execute:
+PTRDEBUGTAC<coq-core.plugins.ltac::intro@1> $1
+DEBUG LTAC Evaluated term: yp
+
+TcDebug (0) > NONE??? LtacNotationCall (no location),/mnt/data1/2024/01/05/UniMath/UniMath/Foundations/PartA.v:234
+"""
+# source : unimath/unimath/batch2/data08
+
+unimath2 = """Goal:
+    R : ring  M : module R
+  ============================
+   (islinear (idfun M))
+
+
+DEBUG:Going to execute:
+PTRDEBUGTACapply pathsinv0; trivial
+Level 0: Backtrace:
+
+Proof is not complete.
+Level 0: Backtrace:
+
+Proof is not complete.
+
+TcDebug (0) > NONE??? LtacNotationCall (no location),/mnt/data1/2024/01/05/UniMath/UniMath/MoreFoundations/Tactics.veasy:19, Tactics  (UniMath.MoreFoundations),/mnt/data1/2024/01/05/UniMath/UniMath/Algebra/Modules/Examples.v:27
+
+"""
+# source : unimath/unimath/batch2/data_22/BATCH122007
+
+unimath3 = """Goal:
+    X : UU  i : nat  b : hProptoType (i < S i)  x : Vector X (S i)  r : i = i
+  ============================
+   (pr1 lastelement = pr1 (i,, b))
+
+
+DEBUG:Going to execute:
+PTRDEBUGTACsimpl
+DEBUG LTAC Evaluated term: isinjstntonat
+
+TcDebug (0) > /mnt/data1/2024/01/05/UniMath/UniMath/Combinatorics/FiniteSequences.v:114
+"""
+# source : unimath/unimath/batch2/data_12/BATCH112026
+
+unimath4 = """Goal:
+    X : dcpo  CX : continuous_dcpo_struct X  x : pr1hSet X  y : pr1hSet X
+  ============================
+   (x ⊑ y
+    ≃ (∀ i : approximating_family CX x, approximating_family CX x i ⊑ y))
+
+
+DEBUG:Going to execute:
+PTRDEBUGTACsimple refine (p _ _ _) ||
+             simple refine (p _ _ _ _) ||
+               simple refine (p _ _ _ _ _) ||
+                 simple refine (p _ _ _ _ _ _) ||
+                   simple refine (p _ _ _ _ _ _ _) ||
+                     simple refine (p _ _ _ _ _ _ _ _) ||
+                       simple refine (p _ _ _ _ _ _ _ _ _) ||
+                         simple refine (p _ _ _ _ _ _ _ _ _ _) ||
+                           simple refine (p _ _ _ _ _ _ _ _ _ _ _) ||
+                             simple refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
+                               simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+                                 simple refine
+                                  (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) || simple
+                                  refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)
+Level 0: Backtrace:
+
+In environment
+X : dcpo
+CX : continuous_dcpo_struct X
+x, y : X
+The term "weqimplimpl ?f ?g" has type "isaprop ?X → isaprop ?Y → ?X ≃ ?Y"
+while it is expected to have type
+ "x ⊑ y ≃ (∀ i : approximating_family CX x, approximating_family CX x i ⊑ y)".
+Level 0: Backtrace:
+
+In environment
+X : dcpo
+CX : continuous_dcpo_struct X
+x, y : X
+The term "weqimplimpl ?f ?g" has type "isaprop ?X → isaprop ?Y → ?X ≃ ?Y"
+while it is expected to have type
+ "x ⊑ y ≃ (∀ i : approximating_family CX x, approximating_family CX x i ⊑ y)".
+
+TcDebug (0) > NONE??? LtacNotationCall (no location),/mnt/data1/2024/01/05/UniMath/UniMath/Foundations/Init.vsimple_rapply:174, Init  (UniMath.Foundations),/mnt/data1/2024/01/05/UniMath/UniMath/Foundations/Init.v??? LtacNotationCall:189, Init  (UniMath.Foundations),/mnt/data1/2024/01/05/UniMath/UniMath/OrderTheory/DCPOs/Basis/Continuous.v:166
+"""
+# source : unimath/unimath/batch2/data_42/BATCH142042
+
+unimath_examples = [unimath1, unimath2, unimath3, unimath4]
+
 model_name = "deepseek-ai/deepseek-math-7b-instruct"
 tokenizer = AutoTokenizer.from_pretrained(model_name)
 model = AutoModelForCausalLM.from_pretrained(model_name, torch_dtype=torch.bfloat16, device_map="auto")
 model.generation_config = GenerationConfig.from_pretrained(model_name)
 model.generation_config.pad_token_id = model.generation_config.eos_token_id
 
+def parse_full_answer(answer):
+    """Parses the assistant's answer, excluding any text before 'Assistant :'."""
+    match = re.search(r"Assistant\s*:\s*(.*)", answer, re.DOTALL)
+    return match.group(1).strip() if match else "No assistant answer found."
+
+def parse_final_answer(answer):
+    """Extracts the final answer enclosed within \boxed{}."""
+    match = re.search(r"\\boxed\{([^}]+)\}", answer)
+    return match.group(1) if match else "No final answer found."
+
 @spaces.GPU
-def solve_math_problem(question, max_tokens):
-    prompt = f"User: {question}\nPlease reason step by step, and put your final answer within \\boxed{{}}.\nAssistant:"
+def solve_math_problem(question, additional_info, max_tokens):
+    prompt = f"User: {question}\n{additional_info}.\nAssistant:"
     input_ids = tokenizer(prompt, return_tensors="pt").input_ids.to(model.device)
     outputs = model.generate(input_ids, max_length=max_tokens + input_ids.shape[1], pad_token_id=model.generation_config.pad_token_id)
     result = tokenizer.decode(outputs[0], skip_special_tokens=True)
-    return result
+    full_answer = parse_full_answer(result)
+    final_answer = parse_final_answer(result)
+    return full_answer, final_answer
 
 def main():
     with gr.Blocks() as demo:
         gr.Markdown(title)
-        with gr.Row():
-            question = gr.Code(language='python', value='what is the integral of x^2 from 0 to 2?', label="Enter your math problem")
-            max_tokens = gr.Slider(minimum=150, maximum=1200, value=250, label="Max Tokens")
-        submit_button = gr.Button("Solve")
-        output = gr.Code(label="🔮DeepSeekMath📉", interactive=False)
-
-        submit_button.click(fn=solve_math_problem, inputs=[question, max_tokens], outputs=output)
+        final_answer_output = gr.Textbox(label="🔮DeepSeekMath📉")
+        full_answer_output = gr.Code(label="🔮TonicsMathAssistant📉", interactive=False)
+        max_tokens = gr.Slider(minimum=150, maximum=1200, value=250, label="Max Tokens")
+        submit_button = gr.Button("📉Solve")
+        question = gr.Code(language='python', value='what is the integral of x^2 from 0 to 2?', label="🤔Enter your math problem")
+        additional_info = gr.Text(value='Please reason step by step, and put your final answer within \\boxed{{}}', label="🪜Optional train-of-thought")
+        with gr.Accordion("🤖metaintrospector/UniMath Examples"):
+            for example in unimath_examples:
+                gr.Textbox(value=example, label="Example", readonly=True, lines=10)
+        
+        submit_button.click(fn=solve_math_problem, inputs=[question, additional_info, max_tokens], outputs=[full_answer_output, final_answer_output])
 
     demo.launch()