當(dāng)我們在解數(shù)學(xué)題時，通常是先讀懂題目，然后一步步推理證明。但對于人工智能來說，這個看似簡單的過程卻充滿挑戰(zhàn)。想象一下，如果你只會看懂正式的數(shù)學(xué)符號，卻完全不理解人類的自然語言，那么當(dāng)老師用中文或英文出一道幾何題時，你就完全束手無策了。這正是目前大多數(shù)AI數(shù)學(xué)證明系統(tǒng)面臨的困境——它們雖然能在嚴(yán)格的數(shù)學(xué)符號世界里游刃有余，卻無法直接處理我們?nèi)粘Ｊ褂玫淖匀徽Z言數(shù)學(xué)問題。

這個問題困擾了研究人員很久，直到華為諾亞方舟實驗室、華為Celia團(tuán)隊和香港中文大學(xué)的聯(lián)合研究團(tuán)隊帶來了突破性進(jìn)展。他們在2025年6月8日發(fā)表的這項研究名為"Mathesis: Towards Formal Theorem Proving from Natural Languages"（Mathesis：走向從自然語言出發(fā)的形式化定理證明），完整論文可通過arXiv:2506.07047v1獲取。研究團(tuán)隊包括華為Celia團(tuán)隊的俞學(xué)軍、翟鵬義等人，華為諾亞方舟實驗室的鐘建元、馮子錦、劉浩雄等研究者，以及香港中文大學(xué)的徐強教授，由李振國和沈鑫擔(dān)任通訊作者。

這項研究首次實現(xiàn)了從自然語言數(shù)學(xué)問題到嚴(yán)格數(shù)學(xué)證明的端到端自動化處理。就像為AI配備了一位既精通人類語言又擅長數(shù)學(xué)推理的翻譯兼數(shù)學(xué)家。研究團(tuán)隊不僅開發(fā)了名為Mathesis的完整解決方案，還創(chuàng)建了一個包含488道中國高考數(shù)學(xué)題的標(biāo)準(zhǔn)測試集，為這個領(lǐng)域建立了重要的評估基準(zhǔn)。

更令人興奮的是，這套系統(tǒng)已經(jīng)被實際應(yīng)用到華為Celia智能助手中，幫助解決真實的高考數(shù)學(xué)問題。當(dāng)面對復(fù)雜的數(shù)學(xué)推理時，系統(tǒng)能夠?qū)⒎钦降耐评砼c嚴(yán)格的形式化證明相結(jié)合，準(zhǔn)確率從原來的65.3%提升到了84.2%。這意味著AI不僅能理解我們的數(shù)學(xué)問題，還能給出既嚴(yán)謹(jǐn)又可驗證的證明過程。

一、從語言理解到數(shù)學(xué)翻譯：Mathesis-Autoformalizer的突破

想象你是一位精通中英文的數(shù)學(xué)老師，學(xué)生用中文向你提出一個幾何問題，你需要將這個問題精確地翻譯成嚴(yán)格的數(shù)學(xué)符號語言，不能丟失任何條件，也不能添加多余的假設(shè)。這正是Mathesis-Autoformalizer所要完成的任務(wù)——將自然語言表達(dá)的數(shù)學(xué)問題準(zhǔn)確轉(zhuǎn)換為計算機能夠處理的形式化數(shù)學(xué)語言。

傳統(tǒng)的自動形式化方法就像一個只會按照固定模板工作的翻譯軟件，遇到復(fù)雜或新穎的表達(dá)方式就容易出錯。而Mathesis-Autoformalizer采用了一種全新的強化學(xué)習(xí)方法，就像培養(yǎng)一個真正的數(shù)學(xué)翻譯專家，讓它在實踐中不斷學(xué)習(xí)和改進(jìn)。

這個系統(tǒng)的核心創(chuàng)新在于建立了一套雙重檢驗機制。首先是語法檢驗，確保翻譯出的數(shù)學(xué)表達(dá)式在形式上是正確的，就像檢查一個句子是否符合語法規(guī)則。然后是語義檢驗，確保翻譯后的內(nèi)容與原問題的數(shù)學(xué)含義完全一致，就像確認(rèn)翻譯是否準(zhǔn)確傳達(dá)了原文的意思。

研究團(tuán)隊設(shè)計了一個巧妙的獎勵系統(tǒng)來訓(xùn)練這個翻譯專家。當(dāng)系統(tǒng)成功將一個自然語言問題轉(zhuǎn)換為語法正確且語義準(zhǔn)確的形式化表達(dá)時，就會獲得正面反饋。反之，如果翻譯出現(xiàn)錯誤或偏差，系統(tǒng)就會收到負(fù)面信號并調(diào)整策略。這種方法讓AI能夠從每次翻譯嘗試中學(xué)習(xí)，逐漸提高準(zhǔn)確性。

為了進(jìn)一步優(yōu)化性能，研究團(tuán)隊還引入了層次化偏好優(yōu)化技術(shù)。這就像為翻譯專家配備了一位資深導(dǎo)師，不僅關(guān)注單次翻譯的質(zhì)量，還考慮翻譯結(jié)果是否有利于后續(xù)的數(shù)學(xué)證明過程。通過這種方式，系統(tǒng)學(xué)會了生成既準(zhǔn)確又實用的形式化表達(dá)。

在數(shù)據(jù)準(zhǔn)備方面，研究團(tuán)隊采用了智能的主題建模技術(shù)來篩選訓(xùn)練材料。他們使用BERTopic算法將大量數(shù)學(xué)問題按照主題進(jìn)行分類，然后有針對性地選擇那些能夠提供豐富學(xué)習(xí)信號的問題進(jìn)行訓(xùn)練。這種方法大大提高了訓(xùn)練效率，讓系統(tǒng)能夠更快地掌握各種數(shù)學(xué)領(lǐng)域的表達(dá)特點。

實驗結(jié)果顯示，Mathesis-Autoformalizer在處理復(fù)雜數(shù)學(xué)問題時表現(xiàn)出色。在新構(gòu)建的高考數(shù)學(xué)測試集上，它的成功率比之前最好的系統(tǒng)提高了22%。在廣泛使用的MiniF2F測試集上，也取得了5%的提升。這些數(shù)字背后代表的是AI在理解和轉(zhuǎn)換自然語言數(shù)學(xué)表達(dá)方面的顯著進(jìn)步。

二、精準(zhǔn)評估翻譯質(zhì)量：LeanScorer的創(chuàng)新評估框架

在數(shù)學(xué)翻譯的世界里，如何判斷一個翻譯是否真正準(zhǔn)確是一個極其復(fù)雜的問題。想象你是一位嚴(yán)格的數(shù)學(xué)老師，需要評判學(xué)生是否正確理解了題目。簡單的對錯判斷往往不夠，你需要仔細(xì)分析學(xué)生理解的每個細(xì)節(jié)，發(fā)現(xiàn)那些看似正確但實際存在微妙偏差的地方。

傳統(tǒng)的評估方法就像只看最終答案是否正確的粗糙檢查，無法發(fā)現(xiàn)翻譯過程中的細(xì)微問題。研究團(tuán)隊開發(fā)的LeanScorer系統(tǒng)則像一位經(jīng)驗豐富的數(shù)學(xué)老師，能夠進(jìn)行多層次、多角度的精細(xì)評估。

LeanScorer的工作過程就像一個細(xì)致的分析專家。首先，它會將復(fù)雜的數(shù)學(xué)問題分解成若干個子任務(wù)，比如將一個幾何證明題分解為"給定條件"、"求證結(jié)論"、"輔助定義"等不同部分。然后對每個部分進(jìn)行獨立評估，判斷形式化翻譯是否準(zhǔn)確反映了原問題的意圖。

在評估每個子任務(wù)時，LeanScorer采用了三級評價體系。"完全匹配"表示翻譯完美地反映了原問題的數(shù)學(xué)含義，就像一個完美的翻譯作品。"輕微不一致"表示翻譯在數(shù)學(xué)本質(zhì)上是正確的，但在表達(dá)方式或細(xì)節(jié)上存在微小差異，就像同一個意思的不同表達(dá)方式。"嚴(yán)重不一致"則表示翻譯在數(shù)學(xué)含義上存在根本性錯誤，可能導(dǎo)致完全不同的數(shù)學(xué)問題。

這種細(xì)致的評估結(jié)果需要通過一個巧妙的聚合機制來形成最終判斷。研究團(tuán)隊采用了Sugeno模糊積分這一數(shù)學(xué)工具，就像一位經(jīng)驗豐富的評委能夠綜合考慮各個方面的表現(xiàn)來給出公正的總分。這個聚合過程有一個重要特點：如果翻譯中存在任何"嚴(yán)重不一致"的問題，整個翻譯就會被判定為不合格，體現(xiàn)了數(shù)學(xué)嚴(yán)謹(jǐn)性的要求。同時，多個"輕微不一致"會導(dǎo)致分?jǐn)?shù)的逐步扣減，鼓勵系統(tǒng)追求更高的準(zhǔn)確性。

LeanScorer的有效性通過與其他評估方法的對比得到了驗證。與簡單的LLM評判方法相比，LeanScorer在精確度上達(dá)到94%，召回率達(dá)到89%，F(xiàn)1分?jǐn)?shù)達(dá)到0.92，顯著超越了傳統(tǒng)方法。這意味著它不僅能夠準(zhǔn)確識別好的翻譯，還能有效發(fā)現(xiàn)存在問題的翻譯，為數(shù)學(xué)AI系統(tǒng)的改進(jìn)提供了可靠的指導(dǎo)。

更重要的是，LeanScorer提供了一個連續(xù)的評分機制，而不是簡單的通過或不通過判斷。這種細(xì)致的評估能夠幫助研究人員更好地理解系統(tǒng)的優(yōu)缺點，為進(jìn)一步改進(jìn)提供方向。在實際應(yīng)用中，用戶還可以根據(jù)具體需求調(diào)整評估的嚴(yán)格程度，在準(zhǔn)確性和實用性之間找到平衡。

三、嚴(yán)格數(shù)學(xué)推理：Mathesis-Prover的證明能力

當(dāng)自然語言數(shù)學(xué)問題被成功轉(zhuǎn)換為形式化表達(dá)后，下一步就是生成嚴(yán)格的數(shù)學(xué)證明。這就像一位數(shù)學(xué)家接過了一個精確表述的數(shù)學(xué)問題，需要運用邏輯推理和數(shù)學(xué)知識來構(gòu)建完整的證明過程。Mathesis-Prover就是這樣一位AI數(shù)學(xué)家，專門負(fù)責(zé)將形式化的數(shù)學(xué)陳述轉(zhuǎn)化為可驗證的嚴(yán)格證明。

Mathesis-Prover的設(shè)計理念基于專家迭代的思想，就像一位數(shù)學(xué)家通過不斷練習(xí)和學(xué)習(xí)來提高證明技巧。系統(tǒng)首先從現(xiàn)有的優(yōu)秀數(shù)學(xué)證明中學(xué)習(xí)基礎(chǔ)技能，然后通過嘗試解決新問題來不斷改進(jìn)自己的能力。這個過程形成了一個自我改進(jìn)的循環(huán)：系統(tǒng)解決問題的能力越強，就能處理更復(fù)雜的問題，從而學(xué)到更高級的證明技巧。

在訓(xùn)練過程中，Mathesis-Prover采用了精心設(shè)計的難度篩選機制。系統(tǒng)不會盲目地嘗試所有問題，而是專注于那些具有適當(dāng)挑戰(zhàn)性的題目。具體來說，它會選擇那些現(xiàn)有系統(tǒng)無法在四次嘗試內(nèi)解決，但經(jīng)過訓(xùn)練后的新系統(tǒng)能夠成功證明的問題。這種策略確保了訓(xùn)練的效率和效果，讓系統(tǒng)能夠在合適的難度區(qū)間內(nèi)穩(wěn)步提升。

Mathesis-Prover的另一個重要特點是它對證明質(zhì)量的嚴(yán)格要求。在數(shù)學(xué)證明的世界里，形式正確但缺乏實質(zhì)內(nèi)容的"證明"是不被接受的。研究團(tuán)隊發(fā)現(xiàn)，有些AI系統(tǒng)會生成形式上通過編譯器檢查但實際上沒有進(jìn)行真正推理的證明，比如使用"apply?"這樣的萬能策略或者將證明目標(biāo)簡化為顯而易見的真命題。Mathesis-Prover通過嚴(yán)格的質(zhì)量控制機制排除了這些不合格的證明，確保每個生成的證明都具有真正的數(shù)學(xué)價值。

在實際性能測試中，Mathesis-Prover展現(xiàn)出了優(yōu)秀的證明能力。當(dāng)與不同的自動形式化系統(tǒng)配合使用時，它都能夠提供穩(wěn)定且優(yōu)秀的證明性能。特別是當(dāng)與Mathesis-Autoformalizer組合使用時，整個端到端系統(tǒng)在MiniF2F測試集上達(dá)到了64.3%的成功率，在更具挑戰(zhàn)性的高考數(shù)學(xué)測試集上也實現(xiàn)了18.0%的成功率。

這些數(shù)字的意義不僅在于絕對性能的提升，更重要的是證明了AI系統(tǒng)確實能夠處理從自然語言到嚴(yán)格證明的完整流程。研究團(tuán)隊的分析顯示，在這個端到端流程中，自動形式化的質(zhì)量提升對整體性能的影響甚至超過了證明器本身的改進(jìn)，這再次說明了準(zhǔn)確理解和轉(zhuǎn)換自然語言數(shù)學(xué)問題的重要性。

四、構(gòu)建評估基準(zhǔn)：Gaokao-Formal數(shù)據(jù)集的重要意義

為了真正評估AI系統(tǒng)處理自然語言數(shù)學(xué)問題的能力，研究團(tuán)隊面臨一個關(guān)鍵挑戰(zhàn)：現(xiàn)有的評估基準(zhǔn)主要關(guān)注已經(jīng)形式化的數(shù)學(xué)問題，而缺乏針對自然語言到形式化轉(zhuǎn)換過程的全面測試。這就像要評估一位翻譯的能力，卻只給他已經(jīng)翻譯好的文本進(jìn)行校對，而不讓他直接進(jìn)行翻譯工作。

為了填補這個空白，研究團(tuán)隊精心構(gòu)建了Gaokao-Formal數(shù)據(jù)集，這是一個包含488道中國高考數(shù)學(xué)題的綜合性評估基準(zhǔn)。選擇高考數(shù)學(xué)題有著深層的考慮：這些題目不僅具有標(biāo)準(zhǔn)化的難度和質(zhì)量保證，更重要的是它們涵蓋了數(shù)學(xué)的各個分支，包括許多現(xiàn)有評估集合有意避開的復(fù)雜領(lǐng)域。

與現(xiàn)有的測試集相比，Gaokao-Formal的一個重要特點是它的全面性和真實性。許多現(xiàn)有的數(shù)學(xué)AI評估集合為了降低自動形式化的難度，往往會簡化問題表述或者排除某些類型的題目，比如幾何問題、組合數(shù)學(xué)問題或者包含復(fù)雜文字描述的應(yīng)用題。這種做法雖然便于評估，但無法反映真實世界中數(shù)學(xué)問題的復(fù)雜性。

Gaokao-Formal則采取了完全不同的策略，它保留了高考數(shù)學(xué)題的原始復(fù)雜性。數(shù)據(jù)集包含了函數(shù)、數(shù)列、不等式、三角函數(shù)、解析幾何、概率組合以及綜合問題等七個主要類別。其中，綜合問題類別特別值得關(guān)注，這些問題往往涉及多個數(shù)學(xué)領(lǐng)域的概念，包含新穎的定義或復(fù)雜的語言結(jié)構(gòu)，對自動形式化系統(tǒng)提出了極高的挑戰(zhàn)。

在數(shù)據(jù)集構(gòu)建過程中，研究團(tuán)隊付出了巨大的努力來確保質(zhì)量。每個問題都包含原始的中文版本、專業(yè)的英文翻譯，以及經(jīng)過數(shù)學(xué)專家驗證的Lean 4形式化表述。這種三重保障確保了數(shù)據(jù)集的準(zhǔn)確性和可靠性。特別值得一提的是，專家驗證的形式化表述嚴(yán)格遵循數(shù)學(xué)的完整性要求，明確聲明所有前提條件，定義所有使用的變量和函數(shù)域，不允許任何含糊或不嚴(yán)謹(jǐn)?shù)谋磉_(dá)。

Gaokao-Formal的另一個重要特征是它對自動形式化復(fù)雜性的真實反映。研究團(tuán)隊故意保留了那些形式化過程特別困難的問題，這些問題往往是現(xiàn)有評估集合刻意避開的。比如，一些問題需要AI系統(tǒng)理解新定義的數(shù)學(xué)概念，另一些問題則需要處理復(fù)雜的幾何關(guān)系或組合計數(shù)問題。這種設(shè)計使得Gaokao-Formal成為測試AI系統(tǒng)真實能力的嚴(yán)格基準(zhǔn)。

數(shù)據(jù)集的統(tǒng)計分布也體現(xiàn)了其全面性。在488個問題中，函數(shù)類問題167個，數(shù)列問題150個，體現(xiàn)了這兩個領(lǐng)域在高等數(shù)學(xué)中的重要地位。同時，幾何、三角函數(shù)、不等式等傳統(tǒng)困難領(lǐng)域也都有充分的代表。這種分布確保了評估結(jié)果的全面性和代表性。

更重要的是，Gaokao-Formal為整個研究社區(qū)提供了一個標(biāo)準(zhǔn)化的評估平臺。研究人員可以使用這個數(shù)據(jù)集來比較不同方法的性能，識別各種方法的優(yōu)勢和局限性，從而推動整個領(lǐng)域的進(jìn)步。數(shù)據(jù)集的公開發(fā)布也為后續(xù)研究提供了重要資源，有助于建立更加完善的數(shù)學(xué)AI系統(tǒng)。

五、端到端系統(tǒng)的完整流程

將自然語言數(shù)學(xué)問題轉(zhuǎn)換為嚴(yán)格的數(shù)學(xué)證明，就像完成一個復(fù)雜的接力賽，需要多個專門的系統(tǒng)精密配合。Mathesis的端到端流程就是這樣一個精心設(shè)計的協(xié)作系統(tǒng)，每個環(huán)節(jié)都有其特定的作用和價值。

整個流程的起點是一個用自然語言表述的數(shù)學(xué)問題，比如"證明對于任意正整數(shù)n，1+2+...+n = n(n+1)/2"。這樣的問題對人類來說很容易理解，但對計算機而言卻需要經(jīng)過復(fù)雜的轉(zhuǎn)換才能處理。

第一個環(huán)節(jié)是自動形式化階段，由Mathesis-Autoformalizer負(fù)責(zé)。這個系統(tǒng)就像一位精通數(shù)學(xué)的翻譯專家，需要將自然語言表述轉(zhuǎn)換為計算機能夠理解的形式化數(shù)學(xué)語言。為了提高成功率，系統(tǒng)會生成多個候選翻譯，就像一位謹(jǐn)慎的翻譯者會提供幾種不同的翻譯方案供選擇。

緊接著是驗證篩選階段，這是整個流程中的質(zhì)量控制環(huán)節(jié)。首先，所有候選翻譯都要通過Lean編譯器的語法檢查，確保它們在形式上是正確的數(shù)學(xué)表達(dá)式。然后，通過語法檢查的翻譯會被送到LeanScorer進(jìn)行語義評估，判斷它們是否準(zhǔn)確反映了原問題的數(shù)學(xué)含義。這個雙重驗證過程就像一位嚴(yán)格的編輯既要檢查文章的語法正確性，又要確認(rèn)內(nèi)容的準(zhǔn)確性。

在驗證篩選之后，系統(tǒng)會選擇那個既通過語法檢查又獲得最高語義評分的翻譯作為最終的形式化表述。這個選擇過程體現(xiàn)了系統(tǒng)對質(zhì)量的嚴(yán)格要求：不僅要求形式正確，更要求意義準(zhǔn)確。

最后一個環(huán)節(jié)是證明生成階段，由Mathesis-Prover接手工作。這個系統(tǒng)就像一位專業(yè)的數(shù)學(xué)家，接收形式化的數(shù)學(xué)陳述并生成完整的證明過程。為了應(yīng)對證明的復(fù)雜性和不確定性，系統(tǒng)會嘗試生成多個證明方案，然后通過Lean驗證器確認(rèn)哪些證明是正確和完整的。

整個端到端流程的設(shè)計考慮了數(shù)學(xué)推理的特殊要求。與其他AI任務(wù)不同，數(shù)學(xué)證明不允許任何模糊或近似，每一步都必須嚴(yán)格正確。因此，系統(tǒng)在每個環(huán)節(jié)都設(shè)置了嚴(yán)格的質(zhì)量檢查機制，確保錯誤不會在流程中累積和傳播。

這種端到端的設(shè)計還具有重要的實用價值。在傳統(tǒng)的數(shù)學(xué)AI系統(tǒng)中，用戶往往需要自己進(jìn)行形式化轉(zhuǎn)換，這要求用戶具備專業(yè)的數(shù)學(xué)知識和形式化技能。而Mathesis的端到端流程使得普通用戶也能直接使用自然語言提出數(shù)學(xué)問題，大大降低了使用門檻。

實驗結(jié)果證明了這種端到端設(shè)計的有效性。當(dāng)所有組件協(xié)同工作時，系統(tǒng)在MiniF2F測試集上達(dá)到了64.3%的成功率，在Gaokao-Formal測試集上達(dá)到了18.0%的成功率。這些數(shù)字不僅代表了技術(shù)性能，更重要的是證明了AI系統(tǒng)確實能夠處理完整的數(shù)學(xué)問題解決流程。

六、實驗驗證與性能分析

要驗證一個復(fù)雜AI系統(tǒng)的真實能力，就像評估一位新手廚師的烹飪水平，不僅要看他做出的菜品質(zhì)量，還要考察他在不同條件下的穩(wěn)定表現(xiàn)以及與其他廚師的比較。研究團(tuán)隊為Mathesis系統(tǒng)設(shè)計了全面而嚴(yán)格的實驗評估方案。

在自動形式化能力的測試中，Mathesis-Autoformalizer與眾多強大的競爭對手進(jìn)行了對比。這些對手包括像Claude-3.5、GPT-4o這樣的商業(yè)API模型，以及Herald-7B、Kimina-7B等開源專業(yè)模型。測試就像一場多項比賽，每個系統(tǒng)都需要處理相同的自然語言數(shù)學(xué)問題，然后比較它們生成的形式化表述的質(zhì)量。

評估采用了兩個層次的指標(biāo)。首先是語法正確性檢查，確保生成的形式化表述能夠通過Lean編譯器的驗證，這就像檢查一篇文章是否符合基本的語法規(guī)則。然后是語法加語義雙重檢查，不僅要求形式正確，還要求意義準(zhǔn)確，這就像要求翻譯不僅要通順，還要忠實原文。

在這場比拼中，Mathesis-Autoformalizer表現(xiàn)優(yōu)異。在具有挑戰(zhàn)性的Gaokao-Formal數(shù)據(jù)集上，當(dāng)系統(tǒng)有6次嘗試機會時，它的綜合成功率達(dá)到了71%，比之前最好的Kimina基線系統(tǒng)的49%有了顯著提升，相對改進(jìn)幅度達(dá)到約45%。這意味著每10個復(fù)雜的數(shù)學(xué)問題中，Mathesis能夠成功處理7個，而之前的最好系統(tǒng)只能處理不到5個。

在廣泛使用的MiniF2F測試集上，Mathesis同樣表現(xiàn)出色，綜合成功率達(dá)到了96%，比Kimina的91%有進(jìn)一步提升。這些數(shù)字的背后反映了強化學(xué)習(xí)和層次化偏好優(yōu)化策略的有效性，證明了讓AI系統(tǒng)從實踐中學(xué)習(xí)比單純的監(jiān)督學(xué)習(xí)更加有效。

LeanScorer評估框架的有效性也得到了充分驗證。與傳統(tǒng)的LLM-as-a-Judge方法相比，LeanScorer在精確度上提升了21個百分點，在F1分?jǐn)?shù)上提升了7個百分點。與重新信息化基線方法相比，改進(jìn)更加顯著，F(xiàn)1分?jǐn)?shù)提升了27個百分點。這些數(shù)字說明了細(xì)致的多層次評估比簡單的二元判斷更加可靠和有用。

端到端系統(tǒng)的測試結(jié)果最令人振奮。研究團(tuán)隊將不同的自動形式化器與不同的證明器進(jìn)行組合測試，就像測試不同演員組合的舞臺效果。結(jié)果顯示，Mathesis-Autoformalizer與Mathesis-Prover的組合達(dá)到了最佳性能，在MiniF2F上取得64.3%的成功率，在Gaokao-Formal上取得18.0%的成功率。

更有趣的是，研究團(tuán)隊還分析了系統(tǒng)各個組件對整體性能的貢獻(xiàn)。他們發(fā)現(xiàn)，在端到端流程中，自動形式化器的改進(jìn)對整體性能的影響甚至超過了證明器的改進(jìn)。在MiniF2F上，使用更好的證明器帶來11.5%的性能提升，而使用更好的自動形式化器則帶來29.5%的提升。在Gaokao-Formal上，這種趨勢更加明顯，自動形式化器的改進(jìn)帶來11.2%的提升，而證明器改進(jìn)只帶來6.4%的提升。

這個發(fā)現(xiàn)具有重要的指導(dǎo)意義，它說明了準(zhǔn)確理解和轉(zhuǎn)換自然語言數(shù)學(xué)問題是整個流程中的關(guān)鍵瓶頸。這也解釋了為什么研究團(tuán)隊在自動形式化方面投入了大量精力，開發(fā)了復(fù)雜的強化學(xué)習(xí)和偏好優(yōu)化機制。

實驗還揭示了一些有趣的現(xiàn)象。在某些情況下，AI生成的形式化表述甚至比人工編寫的版本更容易被證明器處理。這主要是因為人工版本往往會嚴(yán)格聲明所有數(shù)學(xué)條件和定義域，而AI版本可能會采用更簡潔的表述方式，恰好符合證明器的訓(xùn)練分布。當(dāng)然，這種現(xiàn)象也部分歸因于LeanScorer在檢測微妙語義差異方面還有改進(jìn)空間。

七、華為Celia中的實際應(yīng)用

將先進(jìn)的AI研究成果從實驗室?guī)У秸鎸嵤澜绲膽?yīng)用中，就像將一道精心研制的菜品從廚房端上餐桌，需要考慮更多實際因素和用戶需求。華為Celia智能助手中Mathesis系統(tǒng)的部署，為我們展示了學(xué)術(shù)研究如何轉(zhuǎn)化為實用技術(shù)。

華為團(tuán)隊面臨的第一個挑戰(zhàn)是高考數(shù)學(xué)問題的復(fù)雜性。真實的高考題往往包含多個相互關(guān)聯(lián)的子問題，單個端到端證明系統(tǒng)難以處理如此復(fù)雜的結(jié)構(gòu)。研究團(tuán)隊設(shè)計了一個智能的問題分解策略，就像一位經(jīng)驗豐富的數(shù)學(xué)老師會將復(fù)雜的大題分解成若干個相對獨立的小問題。

這個分解過程并非簡單的機械切割，而是需要深度理解問題的邏輯結(jié)構(gòu)。系統(tǒng)首先使用大語言模型分析整個問題的內(nèi)容和結(jié)構(gòu)，識別出不同的數(shù)學(xué)概念、條件和目標(biāo)。然后將原問題拆分成若干個原子級的子問題，每個子問題都可以獨立地通過端到端定理證明流程來處理。

為了進(jìn)一步提升性能，華為團(tuán)隊還開發(fā)了一個創(chuàng)新的交互式形式化-非形式化框架。這個框架就像在嚴(yán)格的數(shù)學(xué)推理和直觀的數(shù)學(xué)理解之間建立了一座橋梁，讓兩種不同的推理方式能夠相互補充和驗證。

在實際應(yīng)用中，系統(tǒng)采用三種不同的方法來處理同一個數(shù)學(xué)問題。第一種是傳統(tǒng)的非正式推理方法，使用最先進(jìn)的大語言模型（如DeepSeek-R1）直接進(jìn)行數(shù)學(xué)推理。第二種是純粹的端到端定理證明方法，完全依賴Mathesis系統(tǒng)的形式化推理能力。第三種是結(jié)合兩者優(yōu)勢的交互式方法，在形式化推理和非正式推理之間建立動態(tài)的協(xié)作機制。

華為團(tuán)隊從近年來的高考數(shù)學(xué)題中篩選出了95個需要證明的子問題，涵蓋了解析幾何、函數(shù)、不等式、數(shù)列、三角函數(shù)和綜合問題等六個主要類別。這些問題具有很強的代表性，能夠全面反映系統(tǒng)在不同數(shù)學(xué)領(lǐng)域的表現(xiàn)。

實驗結(jié)果令人印象深刻?；A(chǔ)的非正式推理方法取得了65.3%的準(zhǔn)確率，這已經(jīng)是一個相當(dāng)不錯的成績。當(dāng)加入端到端定理證明系統(tǒng)后，準(zhǔn)確率提升到69.4%，顯示了形式化推理的價值。而完整的Celia系統(tǒng)，結(jié)合了形式化和非形式化推理的優(yōu)勢，準(zhǔn)確率達(dá)到了84.2%，相比基礎(chǔ)方法提升了18.9個百分點。

這種性能提升在不同數(shù)學(xué)領(lǐng)域都有體現(xiàn)，但程度有所不同。在函數(shù)和不等式問題上，形式化推理的優(yōu)勢特別明顯，這主要是因為這些領(lǐng)域的推理過程往往需要嚴(yán)格的邏輯鏈條，而形式化系統(tǒng)在這方面具有天然優(yōu)勢。在幾何和綜合問題上，交互式框架的效果最為顯著，說明了結(jié)合不同推理方式的重要性。

通過具體的案例分析，華為團(tuán)隊發(fā)現(xiàn)非正式推理在面對復(fù)雜邏輯推理或精細(xì)數(shù)學(xué)計算時容易出錯，有時甚至?xí)捎貌粔驀?yán)謹(jǐn)?shù)耐评矸椒ǎ热缤ㄟ^枚舉特殊情況而非一般性證明來得出結(jié)論。相比之下，形式化推理系統(tǒng)能夠利用Lean 4內(nèi)置的數(shù)學(xué)策略（如nlinarith）來處理復(fù)雜的代數(shù)運算，確保推理過程的嚴(yán)謹(jǐn)性。

這種實際應(yīng)用的成功不僅驗證了Mathesis系統(tǒng)的技術(shù)價值，更重要的是為AI在教育領(lǐng)域的應(yīng)用開辟了新的可能性。學(xué)生和教師可以使用這樣的系統(tǒng)來驗證數(shù)學(xué)推理的正確性，探索不同的證明思路，甚至學(xué)習(xí)更嚴(yán)謹(jǐn)?shù)臄?shù)學(xué)表達(dá)方式。

八、技術(shù)創(chuàng)新的深層意義

Mathesis系統(tǒng)的技術(shù)創(chuàng)新超越了單純的性能提升，它在人工智能和數(shù)學(xué)推理的交叉領(lǐng)域開辟了全新的研究方向。這些創(chuàng)新就像在傳統(tǒng)的數(shù)學(xué)研究和計算機科學(xué)之間架起了一座新的橋梁，讓兩個領(lǐng)域的優(yōu)勢能夠充分結(jié)合。

強化學(xué)習(xí)在自動形式化中的應(yīng)用代表了一個重要的方法論突破。傳統(tǒng)的自動形式化方法主要依賴監(jiān)督學(xué)習(xí)，就像讓學(xué)生通過背誦標(biāo)準(zhǔn)答案來學(xué)習(xí)翻譯技巧。而Mathesis采用的強化學(xué)習(xí)方法更像是讓學(xué)生通過實際練習(xí)和反饋來提高能力，這種方法能夠更好地適應(yīng)復(fù)雜多變的實際問題。

層次化偏好優(yōu)化的引入更是體現(xiàn)了系統(tǒng)性思維的重要性。這種方法認(rèn)識到，在復(fù)雜的AI系統(tǒng)中，局部最優(yōu)不一定導(dǎo)致全局最優(yōu)。一個在單獨評估時表現(xiàn)優(yōu)秀的自動形式化結(jié)果，未必有利于后續(xù)的證明生成過程。通過考慮整個端到端流程的最終目標(biāo)，系統(tǒng)能夠做出更加明智的選擇。

LeanScorer評估框架的創(chuàng)新在于它對數(shù)學(xué)嚴(yán)謹(jǐn)性的深刻理解。傳統(tǒng)的評估方法往往忽略了數(shù)學(xué)推理中細(xì)微但關(guān)鍵的差異，而LeanScorer通過細(xì)致的多層次分析和模糊積分聚合，能夠捕捉到這些微妙的區(qū)別。這種評估方法不僅對當(dāng)前研究有價值，也為未來的數(shù)學(xué)AI系統(tǒng)評估建立了新的標(biāo)準(zhǔn)。

從更廣闊的視角來看，Mathesis系統(tǒng)代表了AI能力的一個重要擴(kuò)展。它證明了AI系統(tǒng)不僅能夠處理感知任務(wù)（如圖像識別、語音識別），也不僅能夠處理生成任務(wù)（如文本生成、圖像生成），更能夠處理需要嚴(yán)格邏輯推理的抽象數(shù)學(xué)任務(wù)。這種能力的擴(kuò)展為AI在科學(xué)研究、工程設(shè)計、教育培訓(xùn)等領(lǐng)域的應(yīng)用開辟了新的可能性。

Gaokao-Formal數(shù)據(jù)集的構(gòu)建也具有重要的方法論意義。它展示了如何從真實世界的需求出發(fā)，構(gòu)建既具有挑戰(zhàn)性又具有實用價值的AI評估基準(zhǔn)。與那些為了便于處理而簡化問題的數(shù)據(jù)集不同，Gaokao-Formal保留了真實數(shù)學(xué)問題的完整復(fù)雜性，為AI系統(tǒng)提出了更高的要求。

交互式形式化-非形式化框架的設(shè)計反映了對人類數(shù)學(xué)思維的深刻洞察。人類數(shù)學(xué)家在解決問題時往往會在直覺思考和嚴(yán)格推理之間自由切換，利用兩種思維模式的不同優(yōu)勢。Mathesis系統(tǒng)成功地將這種思維模式轉(zhuǎn)化為可實現(xiàn)的技術(shù)架構(gòu)，為AI系統(tǒng)的設(shè)計提供了新的范式。

這些技術(shù)創(chuàng)新還揭示了一個重要趨勢：未來的AI系統(tǒng)將越來越多地采用多模塊協(xié)作的架構(gòu)，而不是單一的端到端模型。每個模塊專注于特定的任務(wù)，但通過精心設(shè)計的接口和協(xié)調(diào)機制來實現(xiàn)整體目標(biāo)。這種架構(gòu)不僅能夠提高系統(tǒng)的性能，還能增強系統(tǒng)的可解釋性和可維護(hù)性。

九、面臨的挑戰(zhàn)與未來展望

盡管Mathesis系統(tǒng)取得了顯著的成果，但研究團(tuán)隊也清醒地認(rèn)識到當(dāng)前技術(shù)仍面臨的挑戰(zhàn)和限制。這些挑戰(zhàn)就像攀登高峰過程中遇到的各種障礙，需要研究者們持續(xù)努力才能逐一克服。

當(dāng)前系統(tǒng)最主要的局限性在于各個組件之間仍然存在性能瓶頸。雖然端到端流程已經(jīng)實現(xiàn)，但在復(fù)雜問題上的成功率仍有很大提升空間。在Gaokao-Formal這樣具有挑戰(zhàn)性的數(shù)據(jù)集上，18%的成功率雖然創(chuàng)造了新紀(jì)錄，但距離實用化的要求還有不小差距。這就像一位新手攀巖者雖然成功征服了幾面巖壁，但還需要更多練習(xí)才能應(yīng)對最具挑戰(zhàn)性的攀登路線。

自動形式化過程中的語義理解仍然是一個核心挑戰(zhàn)。雖然LeanScorer提供了更精細(xì)的評估機制，但在處理一些微妙的數(shù)學(xué)概念和復(fù)雜的語言表述時，系統(tǒng)仍可能出現(xiàn)誤判。這種情況就像翻譯復(fù)雜的詩歌作品，不僅要理解字面意思，還要把握深層的意境和內(nèi)涵。

證明生成過程的效率和可解釋性也有待改進(jìn)。目前的系統(tǒng)雖然能夠生成正確的證明，但這些證明往往難以被人類理解和學(xué)習(xí)。在教育應(yīng)用中，學(xué)生不僅需要看到正確答案，更需要理解解題的思路和方法。如何讓AI生成的證明既嚴(yán)格又易懂，是一個需要深入研究的問題。

從技術(shù)架構(gòu)的角度來看，當(dāng)前的多模塊設(shè)計雖然有效，但也帶來了復(fù)雜性和維護(hù)成本。研究團(tuán)隊提出了一個有趣的未來方向：開發(fā)統(tǒng)一的端到端模型，能夠直接從自然語言輸入生成完整的形式化證明。這種模型就像一位全能的數(shù)學(xué)家，不需要經(jīng)過復(fù)雜的內(nèi)部轉(zhuǎn)換就能理解問題并給出證明。

數(shù)據(jù)質(zhì)量和多樣性也是需要持續(xù)關(guān)注的問題。雖然Gaokao-Formal數(shù)據(jù)集已經(jīng)相當(dāng)全面，但數(shù)學(xué)的世界無比廣闊，涵蓋了從基礎(chǔ)算術(shù)到前沿研究的各個層次。要讓AI系統(tǒng)真正掌握數(shù)學(xué)推理能力，需要更大規(guī)模、更多樣化的訓(xùn)練數(shù)據(jù)和評估基準(zhǔn)。

在應(yīng)用層面，如何平衡系統(tǒng)的準(zhǔn)確性和實用性是一個重要考慮。在某些應(yīng)用場景中，用戶可能更愿意接受偶爾的錯誤來換取更快的響應(yīng)速度，而在其他場景中，絕對的準(zhǔn)確性可能是不可妥協(xié)的要求。設(shè)計靈活的系統(tǒng)架構(gòu)來適應(yīng)不同的需求場景，是未來發(fā)展的重要方向。

跨語言和跨文化的數(shù)學(xué)表達(dá)也提出了新的挑戰(zhàn)。雖然數(shù)學(xué)被認(rèn)為是universal language（通用語言），但不同文化背景下的數(shù)學(xué)教育和表達(dá)習(xí)慣確實存在差異。如何讓AI系統(tǒng)適應(yīng)這些差異，為全球用戶提供高質(zhì)量的服務(wù)，需要更深入的研究和更廣泛的國際合作。

展望未來，研究團(tuán)隊設(shè)想了幾個重要的發(fā)展方向。首先是技術(shù)的進(jìn)一步融合，將形式化推理能力整合到通用的大語言模型中，讓這些模型在保持廣泛知識覆蓋的同時具備嚴(yán)格的數(shù)學(xué)推理能力。其次是應(yīng)用領(lǐng)域的擴(kuò)展，從數(shù)學(xué)證明擴(kuò)展到科學(xué)推理、工程設(shè)計、法律分析等需要嚴(yán)格邏輯的領(lǐng)域。

另一個令人興奮的方向是交互式AI數(shù)學(xué)助手的發(fā)展。未來的系統(tǒng)不僅能夠自主解決數(shù)學(xué)問題，還能夠與人類用戶進(jìn)行深度對話，解釋推理過程，回答疑問，甚至提供個性化的學(xué)習(xí)建議。這種助手就像一位永遠(yuǎn)在線的數(shù)學(xué)老師，能夠為學(xué)習(xí)者提供及時、準(zhǔn)確、個性化的幫助。

在教育應(yīng)用方面，研究團(tuán)隊看到了巨大的潛力。AI數(shù)學(xué)推理系統(tǒng)不僅可以幫助學(xué)生檢查作業(yè)、理解概念，還可以為教師提供豐富的教學(xué)資源和個性化的教學(xué)策略。通過分析學(xué)生的錯誤模式和學(xué)習(xí)進(jìn)度，系統(tǒng)可以提供針對性的練習(xí)題和解釋，真正實現(xiàn)因材施教。

最終，研究團(tuán)隊希望這項技術(shù)能夠降低數(shù)學(xué)學(xué)習(xí)和研究的門檻，讓更多人能夠享受到數(shù)學(xué)的美妙和力量。正如數(shù)學(xué)史上的每一次重大突破都會推動人類文明的進(jìn)步一樣，AI在數(shù)學(xué)推理方面的突破也可能為科學(xué)研究、技術(shù)創(chuàng)新和教育發(fā)展帶來深遠(yuǎn)的影響。

說到底，Mathesis系統(tǒng)代表的不僅僅是一個技術(shù)成果，更是人類在理解智能本質(zhì)道路上的重要里程碑。它證明了機器不僅能夠模仿人類的感知和行為，還能夠掌握人類最引以為傲的抽象思維和邏輯推理能力。雖然這條路還很長，但每一步前進(jìn)都讓我們更接近真正理解智能的本質(zhì)，也更接近創(chuàng)造出能夠與人類協(xié)作解決復(fù)雜問題的智能伙伴。

這項由華為團(tuán)隊主導(dǎo)、涉及多個知名研究機構(gòu)的工作，不僅在技術(shù)上取得了突破，更重要的是為整個AI研究社區(qū)提供了新的思路和工具。通過開源數(shù)據(jù)集、評估框架和部分代碼，他們?yōu)楹罄m(xù)研究奠定了堅實基礎(chǔ)。正如科學(xué)發(fā)展的歷史告訴我們的那樣，真正的突破往往來自于研究者之間的開放合作和知識共享。有興趣深入了解這項工作細(xì)節(jié)的讀者，可以通過arXiv:2506.07047v1獲取完整的研究論文，相信這項工作將激發(fā)更多創(chuàng)新思路和實際應(yīng)用。