Axiom Math 運用 AI 代理程式驗證 Stacks Project 資料庫

新創公司 Axiom Math 推出了一套旨在自動驗證數學證明的 AI 代理程式系統。開發人員已成功完成對 Stacks Project 的形式化驗證，這是全球最大的代數幾何資料庫之一，包含數千頁的理論推導。

該公司的技術旨在解決現代語言模型所產生的「數學垃圾」問題。與標準的 LLM 不同，Axiom Math 的代理程式採用形式化驗證方法，能夠在數學上確認證明中每一步的正確性。這消除了機率模型常見的邏輯錯誤或幻覺問題。

在數學領域使用形式化方法傳統上需要科學家投入巨大的時間成本，因為編寫用於證明驗證系統（如 Lean 或 Coq）的程式碼是一個繁瑣的過程。該新創公司的代理程式將此階段自動化，將自然數學語言轉換為適合嚴格驗證的機器可讀格式。

對於數學界而言，這意味著能夠快速確認新假設，並檢查現有研究是否存在隱藏錯誤。導入此類工具使研究人員能夠利用 AI 的強大功能來加速發現，同時保持學術嚴謹性與結果的可靠性。