IXThinker·2025-07-31 13:02

CriticLean開源 數學形式化準確率至84%

讓機器理解並證明數學定理，一直是科研界的重大難題。字節跳動Seed團隊與南京大學聯合發布CriticLean框架，將數學自然語言到Lean4代碼的形式化準確率從38%大幅提升至84%。

核心挑戰

將自然語言描述的數學命題轉化為機器可驗證的形式化代碼，是數學形式化領域的核心難關，長期制約人工智能在定理證明上的發展。此前同類轉換的準確率僅為38%，遠遠無法滿足實際科研需要。