Responsibilities include:

• Hold a new research project
• Create and integrate plugin for LeanCopilot

Responsibilities include:

• Built critic model for expert iteration on Lean dataset(Lean workbook & Lean github)
• Replaced Best first search method with critic model guided search in tactic selection
• Contruct a new comprehensive dataset by expert iteration searching
• Finished one SOTA paper in LLM for theorem proving

Responsibilities include:

• Proposed a scalable, active paradigm in query-based camera-only collaboration task, which reduced the cost in feature transfer
• Implemented a pose-guided selection network in deformable attention in camera-based perception, which greatly reduced the number of BEV queries with effective selection
• Completed all experiments in multi-agent dataset, analyzed the results, and improved scalability
• Submitted a paper to ICRA 2024 as first author