Robust_Prover

Robust_Prover
├── README.md
├── .git/
├── .gitattributes
├── .gitignore
├── .venv/
├── Data/
├── Documents/
└── Scripts/

Robust Mathematical Problem Solver

flowchart
    subgraph Prepare
        A(Natural Language Question) --Filter --> C[/Natural Language Question/]
        C'[/Natural Language Answer/]
        
        C -.-> C'
    end

    subgraph Solve
        D[/Lean Language Question/]
        D'[/Lean Language Answer/]
        F[/Answer & Feedback/]
        G{Correct?}
        H[/Final Answer/]

        C --> D
        D --> D'
        C -.-> D'
        C' -.-> D'
        D' -- check --> F
        F --> G
        G -- Yes --> H
        G -- No --> fix --> D'
    end

    H -.-> I(Natural Language Answer)

Info

Programme Cohort: Large Language Models & Generative AI
Course Group: GEA-Group 2
Group Name: Robust Mathematical Problem Solver
Group Members: Liu Peixuan, Long Haobo, Cao Shuhan, Wu Jiayu, Wu Xuanyu, Wei Yanran, Jin Huiyan
Slogan: Logic. Rigor. Automation.

Proposed Workflow

1. Preprocessing for interference removal
2. Generate natural language reasoning
3. Formalize into proof language (e.g. Lean) for automated verification
4. Adjust based on feedback

Extension directions:

1. Fine-tune models for better task performance
2. Design workflows optimized for formalization from existing papers

Development Team:

1. Anti-interference implementation (Python) - Long Haobo
2. Natural language reasoning generation & transformation (LLM & Agent) - Cao Shuhan
3. Auto-correction implementation (Agent) - Wu Jiayu
   Data Team:
4. Math problem dataset collection - Wu Xuanyu
   Evaluation Team:
5. Test framework & metrics - Wei Yanran
6. Results analysis - Jin Huiyan
   Coordination Team:
7. Progress tracking & documentation - Liu Peixuan

Key References

1. DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
2. Cats Confuse Reasoning LLM: Query Agnostic Adversarial Triggers for Reasoning Models
3. A Language-Agent Approach to Formal Theorem-Proving
4. An In-Context Learning Agent for Formal Theorem-Proving
5. Prover Agent: An Agent-based Framework for Formal Mathematical Proofs