Create app.py

app.py

@@ -0,0 +1,106 @@
+import gradio as gr
+import chromadb
+from typing import List, Dict
+
+# ChromaDB 配置
+client = chromadb.PersistentClient(path="chroma_data")
+
+# 加载集合
+embed_collection = client.get_collection(name="embed_data")
+answer_collection = client.get_collection(name="answer_data")
+
+
+def search_embed_and_answer(label: str):
+    def search_top_answers(target_embedding: List[float], top_n: int = 10) -> List[Dict]:
+        """使用ChromaDB进行相似度搜索"""
+        print("正在执行相似度搜索...")
+        results = answer_collection.query(
+            query_embeddings=[target_embedding],
+            n_results=top_n,
+            include=["metadatas", "documents", "distances"]
+        )
+    
+        # 处理结果
+        answers = []
+        for meta, doc, dist in zip(
+            results['metadatas'][0],
+            results['documents'][0],
+            results['distances'][0]
+        ):
+            answers.append({
+                "formal_name": meta['formal_name'],
+                "formal_statement": meta['formal_statement'],
+                "informal_name": meta['informal_name'],
+                "informal_statement": doc,
+                "similarity": 1 - dist
+            })
+        print("相似度搜索完成！")
+        return answers
+        
+    """主搜索函数"""
+    print("开始处理搜索请求...")
+    
+    # 在 embed 集合中查找目标条目
+    print("正在查询目标定理的元数据...")
+    results = embed_collection.query(
+        query_texts=[label],
+        n_results=1,
+        include=["metadatas", "embeddings"]
+    )
+    
+    if not results['ids'][0]:
+        print(f"未找到 label 为 {label} 的定理。")
+        return f"未找到 label 为 {label} 的定理。", ""
+    
+    # 提取目标条目
+    print("正在提取目标定理的特征...")
+    target_metadata = results['metadatas'][0][0]
+    target_embedding = results['embeddings'][0][0]
+    
+    # 执行搜索
+    print("正在执行相似度搜索...")
+    top_answers = search_top_answers(target_embedding)
+    
+    # 格式化结果
+    print("正在格式化搜索结果...")
+    latex_output = f"目标定理的 tag: {target_metadata['tag']}\nLaTeX 渲染结果: {target_metadata['latex']}"
+    
+    answer_output = "最吻合的前十个定理：\n"
+    for i, ans in enumerate(top_answers, 1):
+        answer_output += (
+            f"{i}. Formal Name: {ans['formal_name']}\n"
+            f"   Formal Statement: {ans['formal_statement']}\n"
+            f"   Informal Name: {ans['informal_name']}\n"
+            f"   Informal Statement: {ans['informal_statement']}\n"
+            f"   相似度: {ans['similarity']:.4f}\n\n"
+        )
+    
+    print("搜索请求处理完成！")
+    return latex_output, answer_output
+
+print("初始化 Gradio 界面...")
+with gr.Blocks(theme=gr.themes.Soft(), title="Mathlib4 Search") as demo:
+    gr.Markdown("""<center><font size=8> ReasLab Smart Search</font></center>""")
+        
+    with gr.Tab("Theorem Search"):
+        label_input = gr.Textbox(
+            placeholder="Example: quadratic_formula", 
+            label="Label",
+            info="Enter a theorem label from embed.json"
+        )
+        search_button = gr.Button("Search")
+        latex_output = gr.Textbox(label="LaTeX and Tag", interactive=False)
+        answer_output = gr.Textbox(label="Top Matching Theorems", interactive=False)
+            
+        search_button.click(
+            fn=search_embed_and_answer,
+            inputs=label_input,
+            outputs=[latex_output, answer_output]
+        )
+    
+print("启动 Gradio 服务...")
+try:
+    demo.launch(server_name="0.0.0.0", server_port=9071, share=False,debug=True)
+    print("Gradio 服务已启动！")
+except Exception as e:
+    print(f"启动 Gradio 服务失败: {e}")