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📉 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:
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 🤗
"""
additional_info_prompt = "Explain the above using mathematics, print entire answer in latex format:"
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 $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, 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)
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)
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("🤖 UniMath Examples", open=False):
gr.Markdown("Click a 🤖 UniMath example to load it into the solver.")
for i, example in enumerate([unimath1, unimath2, unimath3, unimath4], start=1):
gr.Button(f"Example {i}", elem_id=f"example{i}").click(fn=set_example, inputs=example, outputs=[question_field, additional_info_field])
submit_button.click(fn=solve_math_problem, inputs=[question, additional_info, max_tokens], outputs=[full_answer_output, final_answer_output])
demo.launch()
if __name__ == "__main__":
main()