上海
品玩3月24日訊，據美團龍貓官方消息，美團開源了專門用于數學形式化與定理證明的模型——LongCat-Flash-Prover。該模型致力于解決大語言模型在數學證明任務中邏輯嚴謹性不足的問題，通過將形式化推理拆解為自動形式化、草稿生成與證明生成三大原子能力，并采用工具集成推理策略，顯著提升了證明的可靠性。
實驗數據顯示，模型性能卓越。在MiniF2F?Test數據集上，僅需72次推理預算，通過率即達97.1%，刷新開源模型最佳記錄。在超難競賽級任務MathOlympiad?Bench與PutnamBench上，其通過率分別達到46.7%與41.5%，同樣領先于現有開源方案。研究表明，其采用的“草稿生成”策略可平均提升證明準確率約10%。
該模型還引入了多層驗證機制，有效應對了AI在證明過程中可能出現的多種“作弊”行為，確保了證明過程的嚴格性。此舉標志著AI在數學定理證明領域，正從“猜測答案”轉向構建可逐行驗證的嚴謹邏輯鏈條，有望成為基礎科學研究的重要基礎設施。
目前，LongCat?Flash?Prover的代碼、模型及相關技術報告已在GitHub與Hugging Face平臺全面開源。
特別聲明：以上內容(如有圖片或視頻亦包括在內)為自媒體平臺“網易號”用戶上傳并發布，本平臺僅提供信息存儲服務。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
