|
import traceback
|
|
import gradio as gr
|
|
from typing import Optional
|
|
from validator import validate
|
|
from openai import OpenAI
|
|
|
|
|
|
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")
|
|
|
|
|
|
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)
|
|
|
|
|
|
|
|
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."
|
|
|
|
|
|
|
|
grmain() |
