| <!DOCTYPE html> |
| <html lang="zh"> |
| <head> |
| <meta charset="UTF-8"> |
| <meta name="viewport" content="width=device-width, initial-scale=1.0"> |
| <title>StatProver - Automated Statistical Proof Assistant</title> |
| <link href="https://fonts.googleapis.com/css2?family=Inter:wght@400;600;800&display=swap" rel="stylesheet"> |
| <style> |
| |
| :root { |
| --primary: #059669; |
| --primary-dark: #047857; |
| --text-main: #1f2937; |
| --text-light: #6b7280; |
| --bg: #ffffff; |
| } |
| body { |
| font-family: 'Inter', system-ui, -apple-system, sans-serif; |
| color: var(--text-main); |
| background: var(--bg); |
| margin: 0; |
| padding: 0; |
| line-height: 1.7; |
| font-size: 18px; |
| } |
| |
| |
| .hero { |
| text-align: center; |
| padding: 80px 20px 60px; |
| background: linear-gradient(to bottom, #f0fdf4, #ffffff); |
| border-bottom: 1px solid #e5e7eb; |
| } |
| .hero img { |
| max-width: 280px; |
| margin-bottom: 24px; |
| } |
| .hero h1 { |
| font-size: 2.8rem; |
| font-weight: 800; |
| margin: 0 0 16px; |
| color: #111827; |
| letter-spacing: -0.02em; |
| } |
| .hero p.subtitle { |
| font-size: 1.25rem; |
| color: var(--text-light); |
| max-width: 700px; |
| margin: 0 auto 35px; |
| } |
| |
| .cta-button { |
| display: inline-block; |
| background-color: var(--primary); |
| color: white !important; |
| padding: 16px 40px; |
| border-radius: 50px; |
| text-decoration: none; |
| font-weight: 600; |
| font-size: 1.15rem; |
| transition: all 0.3s ease; |
| box-shadow: 0 4px 14px 0 rgba(5, 150, 105, 0.39); |
| } |
| .cta-button:hover { |
| background-color: var(--primary-dark); |
| transform: translateY(-2px); |
| box-shadow: 0 6px 20px rgba(5, 150, 105, 0.4); |
| } |
| |
| |
| .content-container { |
| max-width: 850px; |
| margin: 0 auto; |
| padding: 50px 20px 80px; |
| } |
| .content-container h2 { |
| font-size: 1.8rem; |
| font-weight: 600; |
| border-bottom: 2px solid #f3f4f6; |
| padding-bottom: 12px; |
| margin-top: 45px; |
| color: #111827; |
| } |
| .content-container h3 { |
| font-size: 1.4rem; |
| margin-top: 35px; |
| } |
| .content-container p { |
| font-size: 1.1rem; |
| color: #4b5563; |
| } |
| .content-container a { |
| color: var(--primary); |
| text-decoration: none; |
| font-weight: 500; |
| } |
| .content-container a:hover { |
| text-decoration: underline; |
| } |
| |
| pre { background: #f3f4f6; padding: 15px; border-radius: 8px; overflow-x: auto; } |
| code { font-family: ui-monospace, monospace; font-size: 0.9em; } |
| |
| |
| .content-container img { |
| max-width: 100%; |
| height: auto; |
| border-radius: 8px; |
| box-shadow: 0 4px 12px rgba(0,0,0,0.1); |
| margin: 20px 0; |
| display: block; |
| } |
| |
| @keyframes breathe { |
| 0% { |
| transform: scale(1); |
| filter: drop-shadow(0 0 0 rgba(5, 150, 105, 0)); |
| } |
| 50% { |
| transform: scale(1.08); |
| filter: drop-shadow(0 0 25px rgba(5, 150, 105, 0.6)); |
| } |
| 100% { |
| transform: scale(1); |
| filter: drop-shadow(0 0 0 rgba(5, 150, 105, 0)); |
| } |
| } |
| |
| |
| .breathing-logo { |
| display: inline-block; |
| animation: breathe 3.5s ease-in-out infinite; |
| } |
| </style> |
| </head> |
| <body> |
|
|
| <div class="hero"> |
| <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/font-awesome/6.0.0/css/all.min.css"> |
| |
| <div class="breathing-logo" style="font-size: 80px; color: var(--primary); margin-bottom: 24px;"> |
| <i class="fas fa-project-diagram"></i> |
| </div> |
| |
| <h1>StatProver</h1> |
| |
| <p class="subtitle"> |
| An Automated Statistical Proof Assistant developed by |
| <a href="https://statai-lab.github.io/" target="_blank" style="color: var(--primary); font-weight: 600; text-decoration: none;">StatAI Lab</a>, |
| led by |
| <a href="https://mlzxzhou.github.io/" target="_blank" style="color: var(--primary); font-weight: 600; text-decoration: none;">Prof. Fan Zhou</a> |
| at the School of Statistics and Data Science, Shanghai University of Finance and Economics. |
| </p> |
| |
| <a href="https://statprover.com" target="_blank" class="cta-button"> |
| Launch StatProver |
| </a> |
| </div> |
|
|
| <div class="content-container" id="content"> |
| 加载中... |
| </div> |
|
|
| <script type="text/markdown" id="md-source"> |
| |
| ## What StatProver Does |
| |
| StatProver provides a structured workflow for automated proof generation and self-correction, helping users transform a statistical proposition or source document into a complete LaTeX proof. Built on the comprehensive statistical reasoning benchmark **[StatEval](https://statai-lab.github.io/StatEval.github.io/)**, StatProver retrieves relevant references to refine proof skeletons and performs self-correction by learning from the strategies and details of similar theoretical proofs. |
| |
| <video width="100%" autoplay loop muted playsinline> |
| <source src="https://raw.githubusercontent.com/StatAI-Lab/StatProver_doc/main/videos/demo.mp4" type="video/mp4"> |
| </video> |
| |
| The system supports both end-to-end automated proof construction and flexible human-in-the-loop interaction. Users can intervene at key stages such as problem refinement, framework selection, and error correction, making the proof process both efficient and controllable. |
| |
| |
| |
| ## How StatProver Works |
| |
| StatProver does not rely on one-shot proof generation. Instead, it organizes the derivation process into a six-stage pipeline that supports both automated execution and human intervention at key checkpoints. |
| |
|  |
| |
| * **Step 1. Interactive Problem Refinement** |
| |
| The system first checks whether the input problem is complete and identifies missing assumptions, definitions, or notation. Users can supplement these details manually or let the model help complete them, producing a structured problem description with explicit prerequisites and proof goals. |
| |
| * **Step 2. Candidate Retrieval and User Verification** |
| |
| StatProver extracts core keywords from the problem and retrieves relevant reference cases from a large statistical problem database using embedding-based similarity. It then narrows these candidates and presents the most relevant ones for user verification before they are used in later stages. |
| |
| * **Step 3. Dynamic Framework Refinement** |
| |
| Using the verified reference cases, the system evaluates whether their proof frameworks provide useful methodological guidance for the current task. When appropriate, it refines the initial proof skeleton by incorporating helpful proof strategies while keeping the target problem itself as the primary source of structure. |
| |
| * **Step 4. Draft Proof Generation** |
| |
| Based on the refined framework and the completed problem description, StatProver generates a full draft proof with detailed intermediate derivation steps rather than a short final answer. |
| |
| * **Step 5. Data-Driven Snippet-Level Diagnosis** |
| |
| The generated proof is segmented into fine-grained logical units and checked against a repository of historical error patterns. This allows the system to detect local reasoning flaws, logical jumps, and other proof-level inconsistencies that are often missed by generic self-reflection. |
| |
| * **Step 6. Global Correction and Final Output** |
| |
| Finally, StatProver performs targeted correction based on the diagnosed issues and consolidates the revised reasoning into a rigorous final proof in LaTeX format. |
| |
| ## Key Contributions |
| |
| **Contribution 1. Retrieval-Driven Framework Refinement** |
| |
| StatProver retrieves reference cases from a database of **40,366** research-level statistical problems drawn from **[StatEval](https://statai-lab.github.io/StatEval.github.io/)**. Through similarity-based retrieval and framework verification, the system refines the initial proof skeleton and improves the global structure of the derivation. |
| |
| **Contribution 2. Data-Driven Snippet-Level Self-Correction** |
| |
| StatProver also uses a large empirical fault repository containing over **80,000** error snippets, constructed from LLM failure trajectories on **[StatEval’s](https://statai-lab.github.io/StatEval.github.io/)** research-level data. This repository supports fine-grained diagnosis and targeted correction, allowing the system to identify subtle logical gaps and proof errors beyond standard self-reflection. |
| |
| **Contribution 3. Interactive Proof Assistant Platform** |
| |
| StatProver integrates these components into a unified proof assistant that supports both fully automated generation and flexible human-in-the-loop workflows. The platform is publicly available and designed to assist researchers in producing rigorous statistical proofs more efficiently and reliably. This system is officially deployed and publicly accessible at **[https://statprover.com](https://statprover.com)**. |
| |
| ## Try It Out! |
| |
| **[Official Website](https://statprover.com) : 3 free use on registry, 1 free use per day!** |
| |
| **[Download Full StatProver Technical Report (PDF)](https://raw.githubusercontent.com/StatAI-Lab/StatProver_doc/main/StatProver_Technical_Report.pdf)** |
| |
| ## Contact Us |
| |
| If you have any questions or are interested in collaboration, please feel free to reach out to our laboratory: |
| |
| * **[StatAI Lab](https://statai-lab.github.io/)**: [statai@163.com](mailto:statai@163.com) |
| * **[Prof. Fan Zhou](https://mlzxzhou.github.io/)** (Project Leader): [zhoufan@mail.shufe.edu.cn](mailto:zhoufan@mail.shufe.edu.cn) |
| </script> |
|
|
| <script src="https://cdn.jsdelivr.net/npm/marked/marked.min.js"></script> |
| <script> |
| const mdText = document.getElementById('md-source').innerHTML.trim(); |
| document.getElementById('content').innerHTML = marked.parse(mdText); |
| </script> |
| </body> |
| </html> |
