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 examples = [ [unimath1, additional_info_prompt, 1200], [unimath2, additional_info_prompt, 1200], [unimath3, additional_info_prompt, 1200], [unimath4, additional_info_prompt, 1200] ] 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(): iface = gr.Interface( title="👋🏻Welcome to🌟Tonic's 🔮DeepSeekMath📉", description="""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: