Upload folder using huggingface_hub

README.md

@@ -1,12 +1,6 @@
 ---
-title: Herald
-emoji: 💻
-colorFrom: green
-colorTo: blue
+title: herald
+app_file: herald_gui.py
 sdk: gradio
 sdk_version: 5.9.0
-app_file: app.py
-pinned: false
 ---
-
-Check out the configuration reference at https://huggingface.co/docs/hub/spaces-config-reference

herald_gui.py

@@ -0,0 +1,167 @@
+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)
+
+
+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()