MathlibPR

速報

MathlibPR：以 LLM 評估 Lean/Mathlib Pull Request 的基準初探

背景：Lean與Mathlib為LLM輔助形式化推理的主流。方法：提出MathlibPR基準，從Mathlib4真實PR歷史擷取資料並設計分階段評估，測試多款大型語言模型與代理人。結果：模型難以區分可合併PR與僅通過建置但未合併的PR，MathlibPR提供審查輔助的監督信號。