File size: 7,003 Bytes
6646102 ac13284 6646102 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 |
import traceback
import gradio as gr
from typing import Optional
from validator import validate
from openai import OpenAI
# CSS for styling
css = """
#search_button {background-color: #FC7B4C; /* Default color for light mode */}
@media (prefers-color-scheme: dark) {#search_button {background-color: #C45127; /* dark mode */}}
.footer {
position: fixed;
bottom: 0;
left: 0;
width: 100vw;
box-sizing: border-box;
text-align: center;
background-color: white;
color: black;
font-size: 12px;
padding: 10px;
border-top: 1px solid #ccc;
z-index: 1000;
}
@media (prefers-color-scheme: dark) {
.footer {
background-color: #333;
color: #ccc;
border-top: 1px solid #444;
}
}
"""
footer_html = """
<div class='footer'>
AI4M Team, BICMR@PKU
</div>
"""
def translate(informal_statement, num_passes):
name='textbook_exercise'
max_tokens=1024
temperature=0.99
client = OpenAI(
base_url="https://console.siflow.cn/siflow/draco/ai4math/ytwang/herald-1/v1",
api_key="herald-cool"
)
template = """Please translate the natural language statement to Lean4 code with the header.
**Name**
{name}
**Informal statement**
{informal_statement}
"""
messages = [
{'role': 'system', 'content': 'You are an expert at Lean 4 and Mathematics.'},
{'role': 'user', 'content': template.format(
name=name,
informal_statement=informal_statement)}
]
completion = client.chat.completions.create(
messages=messages,
model="/AI4M/users/ytwang/LLaMA-Factory/saves/deepseek_7b_flash_math_formal5_resume/full/sft/",
max_tokens=max_tokens,
temperature=temperature,
n=num_passes,
)
generated = [output.message.content for output in completion.choices]
for gen in generated:
print(gen)
return generated
def translate_inv(formal_statement, num_passes):
max_tokens=1024
temperature=0
client = OpenAI(
base_url="https://console.siflow.cn/siflow/draco/ai4math/ytwang/herald-1/v1",
api_key="herald-cool"
)
template = """Please translate the Lean4 code back to natural language.
**Formal statement**
{formal_statement}
"""
messages = [
{'role': 'system', 'content': 'You are an expert at Lean 4 and Mathematics.'},
{'role': 'user', 'content': template.format(
formal_statement=formal_statement)}
]
completion = client.chat.completions.create(
messages=messages,
model="/AI4M/users/ytwang/LLaMA-Factory/saves/deepseek_7b_flash_math_formal5_resume/full/sft/",
max_tokens=max_tokens,
temperature=temperature,
n=num_passes,
)
generated = [output.message.content for output in completion.choices]
for gen in generated:
print(gen)
return generated
def translate_for_gradio(informal_statement, num_passes):
import pandas as pd
generated = translate(informal_statement, num_passes)
generated = [f"```lean\n{gen}\n```" for gen in generated]
df = pd.DataFrame(generated, columns=['Translated Formal Statement'])
df.insert(0, 'Rank', range(1, len(df) + 1))
return df
def translate_inv_for_gradio(formal_statement, num_passes):
import pandas as pd
generated = translate_inv(formal_statement, num_passes)
generated = [f"```lean\n{gen}\n```" for gen in generated]
df = pd.DataFrame(generated, columns=['Translated Natural Language'])
df.insert(0, 'Rank', range(1, len(df) + 1))
return df
def grmain():
with gr.Blocks(theme=gr.themes.Soft(), title="Lean 4 Translator", css=css) as demo:
gr.Markdown("""
<center>
<font size=8> Herald Translator </font><br>
<font size=4> Autoformalize your statement using our latest model</font>
</center>
""")
with gr.Tab("Formalize"):
input_text = gr.Textbox(placeholder="Example: The infinite sum of the sequence `1/n` is not convergent.", label="Query", info="Enter a natural language query")
num_passes = gr.Slider(
minimum=1, maximum=128, value=16, step=16, label="Number of passes", info=f"Choose between 1 and 128")
#num_results = gr.Slider(
# minimum=1, maximum=20, value=10, step=1, label="Number of results", info=f"Choose between 1 and {20}")
with gr.Row():
clear_button = gr.Button("Clear", elem_id="clear")
translate_button = gr.Button("Translate", elem_id="translate_button")
with gr.Tab("Informalize"):
input_text_inv = gr.Textbox(placeholder="Example: theorem not_summable_one_div_natCast : ¬Summable (fun n => 1 / n : ℕ → ℝ) := sorry", label="Formal Statement", info="Enter a formal statement")
num_passes_inv = gr.Slider(
minimum=1, maximum=128, value=8, step=8, label="Number of passes", info=f"Choose between 1 and 128")
with gr.Row():
clear_button_inv = gr.Button("Clear", elem_id="clear_inv")
translate_button_inv = gr.Button("Translate", elem_id="translate_button_inv")
output = gr.DataFrame(datatype="markdown")
gr.HTML(footer_html)
clear_button.click(lambda: [None]*2, outputs=[input_text, output])
translate_button.click(fn=translate_for_gradio, inputs=[input_text, num_passes], outputs=output)
translate_button_inv.click(fn=translate_inv_for_gradio, inputs=[input_text_inv, num_passes_inv], outputs=output)
# input_text.submit(fn=translate_for_gradio, inputs=[input_text, num_passes], outputs=output)
#demo.launch(server_name="0.0.0.0", server_port=9062, share = True)
demo.launch()
if __name__ == "__main__":
informal_statement_easy = "The infinite sum of the sequence `1/n` is not convergent."
informal_statement_medium = "Prove that if $A$ and $B$ are subsets of group $G$ with $A \subset B$ then $C_G(B)$ is a subgroup of $C_G(A)$."
informal_statement_hard = "Let $R$ be a subring of the commutative ring $S$ with $1 \in R$ and let $s \in S$. $s$ is integral over $R$ if and only if $R[s]$ is a finitely generated $R$-module (where $R[s]$ is the ring of all $R$-linear combinations of powers of $s$)."
informal_statement_extreme = "Let \(alpha \in R, K=\mathbb{Q}[alpha]\), and let \(f\) be any monic polynomial over \(\mathbb{Z}\) such that \(f(alpha)=0\). If \(p\) is a prime such that \(p nmid \mathrm{N}_{K} f^{\prime}(alpha)\), then \(p\) is unramified in K."
# translate(informal_statement_easy, num_passes=16)
# # print(informal_statement_extreme)
# main(informal_statement_easy, num_passes=32)
grmain() |