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 = """
"""
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("""
Herald Translator
Autoformalize your statement using our latest model
""")
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()