|
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: <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 🤗 |
|
""" |
|
|
|
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<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 |
|
""" |
|
|
|
|
|
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 |
|
|
|
""" |
|
|
|
|
|
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 |
|
""" |
|
|
|
|
|
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 |
|
""" |
|
|
|
|
|
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: <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 🤗""", |
|
fn=solve_math_problem, |
|
outputs=[ |
|
gr.Code(label="🔮TonicsMathAssistant📉", interactive=False), |
|
gr.Textbox(label="Final Answer") |
|
], |
|
inputs=[ |
|
gr.Textbox(label="🤔Enter your math problem", lines=7), |
|
gr.Textbox(value=additional_info_prompt, label="🪜Optional train-of-thought"), |
|
gr.Slider(minimum=150, maximum=1200, value=650, label="🪙Max Tokens") |
|
], |
|
examples=examples |
|
) |
|
|
|
iface.launch() |
|
|
|
if __name__ == "__main__": |
|
main() |