在數(shù)學(xué)和計(jì)算機(jī)科學(xué)的交叉領(lǐng)域，有一項(xiàng)挑戰(zhàn)極其艱巨的任務(wù)——自動(dòng)定理證明。想象一下，你需要教會(huì)計(jì)算機(jī)像數(shù)學(xué)家那樣，一步一步地推導(dǎo)出復(fù)雜數(shù)學(xué)定理的證明。這就像教一個(gè)從未見(jiàn)過(guò)廚房的人，僅憑食譜和原料清單，精確地烹飪出一道法式大餐。今天，我要為大家介紹一項(xiàng)由騰訊AI實(shí)驗(yàn)室和騰訊大語(yǔ)言模型部門(mén)的研究人員共同完成的最新突破——MPS-Prover（多視角搜索證明器）。這項(xiàng)研究由騰訊AI實(shí)驗(yàn)室的梁振文、宋麟峰、米海濤、俞棟和騰訊大語(yǔ)言模型部門(mén)的李楊、楊濤、張峰于2025年5月發(fā)布在arXiv預(yù)印本平臺(tái)上。

自動(dòng)定理證明是什么？簡(jiǎn)單來(lái)說(shuō)，它是讓計(jì)算機(jī)自動(dòng)生成數(shù)學(xué)定理的形式化證明。這些證明必須嚴(yán)格遵循邏輯推理規(guī)則，確保每一步都是正確的。想象一下，你在解一道復(fù)雜的數(shù)學(xué)題，每一步都必須嚴(yán)格按照數(shù)學(xué)規(guī)則，而且不能有任何錯(cuò)誤。計(jì)算機(jī)在做自動(dòng)定理證明時(shí)，面臨的挑戰(zhàn)更大——它需要在巨大的搜索空間中找到正確的證明路徑。

近年來(lái)，大型語(yǔ)言模型（LLMs）在這一領(lǐng)域展現(xiàn)出令人矚目的能力。但現(xiàn)有的逐步證明系統(tǒng)（一步一步生成證明的方法）仍然面臨幾個(gè)主要問(wèn)題：它們往往依賴有偏見(jiàn)的搜索引導(dǎo)，導(dǎo)致效率低下和次優(yōu)的證明策略。比如，它們可能會(huì)陷入重復(fù)使用相同的證明策略而無(wú)法取得進(jìn)展、選擇錯(cuò)誤的策略導(dǎo)致無(wú)法證明的狀態(tài)，或者使用看似強(qiáng)大但在特定情況下無(wú)效的策略。

MPS-Prover通過(guò)兩大創(chuàng)新解決了這些問(wèn)題：一個(gè)高效的訓(xùn)練后數(shù)據(jù)精選策略和一個(gè)多視角樹(shù)搜索機(jī)制。讓我們一起來(lái)看看這個(gè)系統(tǒng)是如何工作的，以及它如何在多個(gè)挑戰(zhàn)性基準(zhǔn)測(cè)試中實(shí)現(xiàn)了最先進(jìn)的性能。

一、理解自動(dòng)定理證明的挑戰(zhàn)

想象你正在教一個(gè)完全不懂?dāng)?shù)學(xué)的人如何解一道復(fù)雜的數(shù)學(xué)題。你不僅需要告訴他解題的每一步，還需要解釋為什么這樣做是正確的。而且，你不能跳過(guò)任何一個(gè)步驟，否則他就會(huì)迷失。

在自動(dòng)定理證明領(lǐng)域，研究人員主要采用兩種方法：一種是"整體證明生成"，即一次性生成完整的證明腳本；另一種是"逐步形式化證明生成"，即計(jì)算機(jī)在每一步都會(huì)提出下一個(gè)證明步驟（一個(gè)正式的策略），然后由形式化證明助手驗(yàn)證這一步是否正確，并提供更新后的證明狀態(tài)作為反饋。

逐步方法有幾個(gè)明顯的優(yōu)勢(shì)：它允許與證明引擎持續(xù)交互，能夠逐步簡(jiǎn)化搜索目標(biāo)，具有更高的容錯(cuò)性（錯(cuò)誤只需要回溯到前一步，而不是重新開(kāi)始整個(gè)證明），而且天然適合使用樹(shù)搜索方法探索不同的證明路徑。

然而，逐步方法也面臨一些關(guān)鍵挑戰(zhàn)，如圖1所示：

首先，引導(dǎo)節(jié)點(diǎn)選擇的評(píng)價(jià)模型可能會(huì)產(chǎn)生偏見(jiàn)。這種偏見(jiàn)往往源于訓(xùn)練數(shù)據(jù)中某些"安全"或廣泛適用的策略（如have或general-purpose simplifiers如aesop和simp_all）出現(xiàn)頻率較高。這些策略雖然通常是有效證明的一部分，但如果模型過(guò)度依賴它們，可能無(wú)法找到最高效的證明路徑，導(dǎo)致類似策略建議重復(fù)出現(xiàn)而使證明停滯不前。

其次，錯(cuò)誤的策略應(yīng)用可能導(dǎo)致"無(wú)法證明的狀態(tài)"，比如過(guò)度簡(jiǎn)化條件。

第三，一些強(qiáng)大但具有條件性有效的策略（如aesop、simp_all）可能被無(wú)效地應(yīng)用。語(yǔ)言模型可能由于這些策略在訓(xùn)練數(shù)據(jù)中頻繁出現(xiàn)或它們能夠產(chǎn)生看似有希望的局部簡(jiǎn)化而提出它們，但當(dāng)狀態(tài)不真正適合這種簡(jiǎn)化時(shí)，它們可能無(wú)法取得進(jìn)展，甚至可能模糊前進(jìn)的路徑。

雖然基于最佳優(yōu)先搜索（BFS）的方法在導(dǎo)航這個(gè)搜索空間方面顯示出希望，但它們通常依賴單一評(píng)價(jià)分?jǐn)?shù)來(lái)擴(kuò)展節(jié)點(diǎn)，這仍然使它們?nèi)菀资艿竭@些失敗模式的影響，特別是學(xué)習(xí)型評(píng)價(jià)模型中固有的偏見(jiàn)。

二、MPS-Prover的雙重創(chuàng)新

MPS-Prover的創(chuàng)新之處在于它巧妙地解決了上述挑戰(zhàn)，通過(guò)兩個(gè)核心創(chuàng)新：

### 1. 訓(xùn)練數(shù)據(jù)精選策略

傳統(tǒng)的專家迭代方法通常會(huì)統(tǒng)一添加所有新證明的問(wèn)題，但MPS-Prover引入了明確的規(guī)則，過(guò)濾掉約40%的冗余或低價(jià)值訓(xùn)練示例，使模型專注于學(xué)習(xí)更復(fù)雜的推理模式。

想象你在學(xué)習(xí)做菜。如果你的食譜書(shū)中90%的內(nèi)容都在教你如何煮白米飯，那么你在復(fù)雜烹飪技巧上的進(jìn)步會(huì)很有限。同樣，如果訓(xùn)練數(shù)據(jù)中充斥著太多簡(jiǎn)單的、重復(fù)的證明模式，模型就難以學(xué)習(xí)到更高級(jí)的推理策略。

具體來(lái)說(shuō)，他們采取了兩種過(guò)濾策略：

一是過(guò)濾短證明。研究團(tuán)隊(duì)排除了那些可以在3步或更少步驟內(nèi)證明的定理。這些非常短的證明主要依賴于一組有限的基本策略（如rfl、simp_all或nlinarith），對(duì)高級(jí)問(wèn)題解決技術(shù)的洞察很少。通過(guò)移除這些過(guò)于簡(jiǎn)單的例子，他們將初始訓(xùn)練數(shù)據(jù)集減少了約40%。

值得注意的是，過(guò)濾這些簡(jiǎn)單證明并不會(huì)降低模型解決簡(jiǎn)單問(wèn)題的能力。這是因?yàn)橹鸩阶C明器的訓(xùn)練數(shù)據(jù)固有地包含大量"后期階段"的證明步驟。這些步驟是在證明已經(jīng)取得良好進(jìn)展并接近完成時(shí)采取的，通常類似于在更簡(jiǎn)單問(wèn)題中遇到的狀態(tài)。因此，模型仍然通過(guò)復(fù)雜證明的中間步驟接觸到足夠的簡(jiǎn)單推理環(huán)境。

二是移除無(wú)效策略。他們還過(guò)濾掉了那些沒(méi)有對(duì)證明狀態(tài)產(chǎn)生有意義進(jìn)展的訓(xùn)練數(shù)據(jù)。某些旨在簡(jiǎn)化的策略有時(shí)不會(huì)給證明狀態(tài)帶來(lái)任何變化，例如aesop、all_goals和simp_all。評(píng)估數(shù)據(jù)集后，他們識(shí)別并移除了約5%的此類無(wú)效策略。這種有針對(duì)性的修剪鼓勵(lì)模型更好地辨別何時(shí)應(yīng)該應(yīng)用這些簡(jiǎn)化策略，減少過(guò)度依賴并提高證明效率。

### 2. 多視角樹(shù)搜索機(jī)制

MPS-Prover的第二個(gè)關(guān)鍵創(chuàng)新是它的多視角樹(shù)搜索機(jī)制。想象你在走迷宮時(shí)，不僅僅依靠一張地圖，而是同時(shí)使用衛(wèi)星視圖、指南針和當(dāng)?shù)厝说慕ㄗh。這種多重指導(dǎo)讓你更不容易走入死胡同。

傳統(tǒng)的最佳優(yōu)先搜索（BFS）方法僅基于最佳評(píng)價(jià)分?jǐn)?shù)選擇節(jié)點(diǎn)。如圖2所示，MPS-Prover不僅考慮評(píng)價(jià)模型的建議，還融入了策略性設(shè)計(jì)的啟發(fā)式規(guī)則，以多樣化策略選擇，防止陷入重復(fù)的、無(wú)效的或不可證明的狀態(tài)，從而提高搜索的穩(wěn)健性。

具體來(lái)說(shuō)，MPS-Prover引入了三種啟發(fā)式選擇規(guī)則：

1. 策略有效性評(píng)分：根據(jù)策略在推進(jìn)證明方面的感知效能為不同策略分配不同的分?jǐn)?shù)。一般來(lái)說(shuō)，那些引入新的、實(shí)質(zhì)性假設(shè)或顯著重構(gòu)證明目標(biāo)的策略，如rcases、intro、contrapose、induction或proof by contradiction（在適當(dāng)應(yīng)用時(shí)），會(huì)被分配更高的分?jǐn)?shù)。這些通常是能夠解鎖新推理路徑或通過(guò)分解問(wèn)題來(lái)簡(jiǎn)化問(wèn)題的策略。相反，輔助策略或那些專注于更局部化的簡(jiǎn)化，如norm_num和simp_all，會(huì)收到較低的分?jǐn)?shù)。

2. 最小化案例分割：選擇導(dǎo)致?tīng)顟B(tài)字符串中案例出現(xiàn)次數(shù)最少的策略。雖然像induction、constructor和split這樣的策略在特定情況下是有益的，但過(guò)度的案例分割會(huì)使證明狀態(tài)變得復(fù)雜。這種啟發(fā)式鼓勵(lì)更簡(jiǎn)單、更易管理的證明狀態(tài)。

3. 最短狀態(tài)偏好：優(yōu)先考慮導(dǎo)致更短的Lean 4狀態(tài)字符串的策略。與最小化案例類似，這種啟發(fā)式偏好更簡(jiǎn)單、更直接的狀態(tài)，有助于更高效地完成證明。

如圖2所示，MPS-Prover的樹(shù)搜索每次擴(kuò)展步驟最多維護(hù)四個(gè)節(jié)點(diǎn)。具體來(lái)說(shuō)，從前一次迭代中選擇的節(jié)點(diǎn)集合開(kāi)始，使用大語(yǔ)言模型為每個(gè)節(jié)點(diǎn)生成Nsamples候選策略。這會(huì)產(chǎn)生一個(gè)更大的潛在下一狀態(tài)池（例如，如果選擇了4個(gè)節(jié)點(diǎn)，并且Nsamples = 8，我們將有4 × 8 = 32個(gè)候選下一狀態(tài)）。從這個(gè)擴(kuò)展的池中：

1. 基于評(píng)價(jià)模型的預(yù)測(cè)（即與完成的距離最小的那個(gè)）選擇一個(gè)節(jié)點(diǎn)。 2. 基于啟發(fā)式規(guī)則選擇額外的三個(gè)節(jié)點(diǎn)。每個(gè)啟發(fā)式規(guī)則評(píng)估所有候選下一狀態(tài)，并選擇最符合其標(biāo)準(zhǔn)的那個(gè)。如果不同視角選擇了相同的節(jié)點(diǎn)，我們只保留它一次，這意味著在這種情況下，可能會(huì)有少于四個(gè)唯一節(jié)點(diǎn)被帶入下一個(gè)搜索迭代。

研究團(tuán)隊(duì)承認(rèn)，每個(gè)啟發(fā)式規(guī)則，包括評(píng)價(jià)模型，都有內(nèi)在的偏見(jiàn)和限制，偏向某些證明策略或狀態(tài)。然而，通過(guò)并發(fā)應(yīng)用這些標(biāo)準(zhǔn)，他們顯著增強(qiáng)了每個(gè)搜索層的多樣性，確保有希望的節(jié)點(diǎn)被保留，而不是因?yàn)閱我粯?biāo)準(zhǔn)的偏見(jiàn)而被忽視。

三、實(shí)驗(yàn)證明MPS-Prover的卓越性能

為了全面評(píng)估MPS-Prover的性能，研究團(tuán)隊(duì)使用了兩個(gè)廣受認(rèn)可的基準(zhǔn)測(cè)試：

1. miniF2F：這是ATP領(lǐng)域的標(biāo)準(zhǔn)基準(zhǔn)測(cè)試。問(wèn)題來(lái)源于數(shù)學(xué)競(jìng)賽（AMC、AIME、IMO）以及高中和本科課程。他們使用了來(lái)自Huggingface Numina倉(cāng)庫(kù)的最新版本，該版本糾正了原始數(shù)據(jù)集中發(fā)現(xiàn)的八個(gè)錯(cuò)誤。

2. ProofNet：這個(gè)基準(zhǔn)測(cè)試包含371個(gè)問(wèn)題，特點(diǎn)是本科水平的數(shù)學(xué)題。研究團(tuán)隊(duì)報(bào)告了其測(cè)試集上的性能。

在supervised fine-tuning（SFT）方面，他們對(duì)Qwen2.5-Math-7B-base進(jìn)行了微調(diào)。SFT數(shù)據(jù)集由以下幾部分組成：(1)在專家迭代過(guò)程中生成并由他們的過(guò)濾技術(shù)精選的逐步證明數(shù)據(jù)；(2)通過(guò)連接已接受的證明步驟形成的完整證明數(shù)據(jù)；(3)為搜索算法的距離評(píng)價(jià)模型訓(xùn)練的數(shù)據(jù)。這個(gè)聚合數(shù)據(jù)集在應(yīng)用訓(xùn)練數(shù)據(jù)過(guò)濾方法后約為350萬(wàn)個(gè)問(wèn)題-答案對(duì)。模型訓(xùn)練了3個(gè)周期，使用余弦學(xué)習(xí)率調(diào)度器，最大學(xué)習(xí)率為2 × 10^-5。累積批量大小為256。訓(xùn)練在8個(gè)H20 80G GPU上進(jìn)行，總訓(xùn)練時(shí)間約為3天。

實(shí)驗(yàn)結(jié)果令人印象深刻。在miniF2F測(cè)試集上，MPS-Prover成功證明了244個(gè)問(wèn)題中的185個(gè)，準(zhǔn)確率達(dá)到75.82%，顯著超過(guò)了之前的最先進(jìn)逐步證明器BFS-prover。在所有7B參數(shù)類模型中（包括整體證明和逐步生成方法），MPS-Prover的性能僅次于DeepSeek-Prover-V2（Distilled, CoT）?？紤]到他們的7B模型是從一個(gè)明顯更大的模型蒸餾而來(lái)，這一結(jié)果尤為令人印象深刻。相比之下，MPS-Prover是直接通過(guò)7B規(guī)模的迭代細(xì)化進(jìn)行訓(xùn)練的。

另一個(gè)值得注意的發(fā)現(xiàn)是MPS-Prover即使在受限的搜索預(yù)算下也表現(xiàn)出色。在評(píng)估的最小搜索預(yù)算下，MPS-Prover在miniF2F上達(dá)到了67.62%的通過(guò)率，顯著優(yōu)于InternLM（50.7%）和Hunyuan Prover（59.84%）在類似最小條件下的表現(xiàn)。令人印象深刻的是，這種基本性能已經(jīng)超過(guò)了幾個(gè)強(qiáng)大基線（如Goedel-prover和InternLM2.5-StepProver）報(bào)告的最大性能，這表明他們的方法表現(xiàn)出優(yōu)秀的穩(wěn)定性和高效性，無(wú)需窮盡搜索努力即可實(shí)現(xiàn)有競(jìng)爭(zhēng)力的結(jié)果。

在更具挑戰(zhàn)性的ProofNet基準(zhǔn)測(cè)試上，MPS-Prover取得了32.97%的成功率，超過(guò)了所有其他7B基線模型，包括使用思維鏈（CoT）推理的DeepSeek-Prover-V2。

研究團(tuán)隊(duì)還進(jìn)行了在固定預(yù)算下的比較?？紤]到MPS每次迭代天然會(huì)探索更多分支，為確保公平比較，他們將MPS的pass@k與BFS的pass@4k在類似算力下進(jìn)行了對(duì)比。如圖3所示，MPS在分配相似計(jì)算資源時(shí)始終優(yōu)于BFS。在最低預(yù)算下（MPS pass@1 vs. BFS pass@4），MPS達(dá)到67.62%（165/244）的成功率，略高于BFS的66.39%（162/244）。隨著預(yù)算增加，這種優(yōu)勢(shì)變得更加明顯，突顯了MPS多樣化探索策略的有效性。

四、深入分析：證明長(zhǎng)度與多樣性

為了進(jìn)一步研究不同搜索策略生成的證明特征，研究團(tuán)隊(duì)對(duì)MPS和標(biāo)準(zhǔn)BFS（使用基于樹(shù)的距離預(yù)測(cè)作為評(píng)價(jià)標(biāo)準(zhǔn)）進(jìn)行了量化比較。他們通過(guò)使用相同的大語(yǔ)言模型骨干并只分析MPS和BFS都成功證明的定理集來(lái)確保公平比較。

圖4a展示了證明長(zhǎng)度的分布，以策略步驟數(shù)量衡量（分組為1-9和10+類別）。很明顯，MPS生成的證明平均比BFS找到的證明顯著更短，如虛線所示的平均值。MPS生成更多步驟較少的證明，而B(niǎo)FS表現(xiàn)出更多較長(zhǎng)證明的長(zhǎng)尾分布。這表明MPS中的多樣化引導(dǎo)信號(hào)有助于避免無(wú)效策略序列或局部最優(yōu)，導(dǎo)致更簡(jiǎn)潔的解決方案。

圖4b說(shuō)明了證明策略多樣性的分布。多樣性定義為證明中使用的唯一策略數(shù)量除以其總長(zhǎng)度（步驟數(shù)）。分?jǐn)?shù)越接近1表示相對(duì)于長(zhǎng)度的策略多樣性越高。結(jié)果清楚地表明，MPS生成的證明具有比BFS證明明顯更高的平均多樣性分?jǐn)?shù)（見(jiàn)均值線）。雖然兩種方法都能生成具有最大多樣性的證明（分?jǐn)?shù)=1.0），但BFS產(chǎn)生了更多多樣性分?jǐn)?shù)非常低的證明。這凸顯了MPS在促進(jìn)探索和利用更廣泛策略范圍方面的有效性，而B(niǎo)FS則僅由評(píng)價(jià)模型引導(dǎo)，更容易出現(xiàn)重復(fù)使用策略的情況。

研究團(tuán)隊(duì)還分析了證明特征，通過(guò)比較MPS-Prover與兩個(gè)領(lǐng)先的整體證明生成器（Kimina-Prover-Preview和DeepSeek-Prover-V2）在170個(gè)共同解決的miniF2F問(wèn)題上生成的證明長(zhǎng)度。表4顯示，MPS-Prover生成的證明明顯更短（平均長(zhǎng)度3.44步），相比之下Kimina的平均長(zhǎng)度為15.91步，DeepSeek-Prover-V2為52.16步。

研究者將這種差異歸因于操作上的不同：像MPS-Prover這樣的逐步證明器受益于與Lean引擎的頻繁交互。每次策略執(zhí)行都會(huì)更新證明狀態(tài)，允許證明器通過(guò)將新?tīng)顟B(tài)視為子問(wèn)題來(lái)自適應(yīng)地優(yōu)化其策略。這種迭代過(guò)程，結(jié)合優(yōu)先考慮有影響力步驟的策略級(jí)搜索，有助于發(fā)現(xiàn)更直接的解決方案。相比之下，整體證明系統(tǒng)通常最初就計(jì)劃整個(gè)證明，動(dòng)態(tài)適應(yīng)有限，可能導(dǎo)致更長(zhǎng)，盡管正確的證明腳本。

五、案例研究：MPS-Prover的優(yōu)勢(shì)

為了提供對(duì)證明策略和生成解決方案差異的更細(xì)微理解，研究團(tuán)隊(duì)對(duì)特定定理進(jìn)行了案例研究，比較了MPS-Prover與Kimina-Prover和DeepSeek-Prover V2生成的證明，并展示了MPS-Prover獨(dú)特解決的問(wèn)題。

例如，在algebra_absapbon1pabsapbleqsumabsaon1pabsa定理（該定理涉及分式不等式證明）中，MPS-Prover生成了僅8行的極其簡(jiǎn)潔證明。關(guān)鍵步驟包括利用rw進(jìn)行基于非負(fù)性的目標(biāo)重寫(xiě)，使用by_cases進(jìn)行情況分析（例如a = 0），然后高效使用field_simp與相關(guān)假設(shè)如abs_nonneg和mul_nonneg。證明以refine'結(jié)合div_nonneg和強(qiáng)大的終結(jié)器如nlinarith和positivity結(jié)束。每一步似乎都取得了實(shí)質(zhì)性進(jìn)展，通常通過(guò)有效利用內(nèi)置的Mathlib引理和策略顯著簡(jiǎn)化目標(biāo)或完成部分證明。

相比之下，Kimina-Prover對(duì)同一問(wèn)題的解決方案長(zhǎng)達(dá)約40行，主要依賴一系列have語(yǔ)句引入中間引理。雖然邏輯合理，但這種明確陳述和證明多個(gè)中間步驟的方法導(dǎo)致了更冗長(zhǎng)的證明。

DeepSeek-Prover V2的證明最長(zhǎng)，約60行。它也廣泛使用have引入并證明一系列引理，但這些引理的證明及其后續(xù)應(yīng)用被分解為許多細(xì)粒度步驟。雖然展示了復(fù)雜的理解能力，但整體證明由于每個(gè)組件的詳細(xì)、一步一步的推導(dǎo)而變得相當(dāng)冗長(zhǎng)。

在另一個(gè)例子imo_1962_p2中（一個(gè)涉及不等式和平方根的問(wèn)題），MPS-Prover再次生成了非常短的證明。它有效使用refine'構(gòu)建連接，然后利用強(qiáng)大的重寫(xiě)和簡(jiǎn)化策略如rw、field_simp、norm_num和nlinarith，通常鏈接或與特定假設(shè)一起應(yīng)用。

這些案例研究強(qiáng)調(diào)了MPS-Prover通過(guò)其逐步搜索和選擇高進(jìn)展策略的趨勢(shì)，傾向于生成更簡(jiǎn)潔的證明，通過(guò)有效利用強(qiáng)大的內(nèi)置Mathlib功能。而整體證明系統(tǒng)，盡管能夠進(jìn)行復(fù)雜的推理和規(guī)劃，但由于其傾向于將問(wèn)題分解為許多更簡(jiǎn)單的、明確陳述的中間步驟，可能會(huì)生成更長(zhǎng)的證明，這些步驟可能受到初始、可能更冗長(zhǎng)的計(jì)劃的限制。

此外，研究團(tuán)隊(duì)還展示了一個(gè)MPS-Prover成功解決而其他兩個(gè)系統(tǒng)都失敗的問(wèn)題：amc12a_2020_p7。這個(gè)問(wèn)題涉及基于序列a(k)^3特定值的求和評(píng)估。MPS-Prover解決方案的關(guān)鍵在于使用induction'作為初始步驟，然后廣泛使用simp_all簡(jiǎn)化目標(biāo)，以及interval_cases處理特定范圍內(nèi)的自然數(shù)變量。MPS-Prover成功找到了這種特定組合的策略，特別是關(guān)鍵的induction'和有效使用interval_cases，這突顯了多視角方法在導(dǎo)航復(fù)雜搜索空間時(shí)的優(yōu)勢(shì)。

六、未來(lái)發(fā)展方向與局限性

盡管MPS-Prover在逐步自動(dòng)定理證明方面取得了顯著進(jìn)展，但研究團(tuán)隊(duì)也承認(rèn)逐步范式本身存在某些固有限制，特別是與整體證明生成方法相比。

當(dāng)前逐步證明器（包括MPS-Prover）的一個(gè)主要限制在于處理引入復(fù)雜、嵌套證明義務(wù)的策略，如需要自己的子證明的新引理。整體證明系統(tǒng)可以生成包含通過(guò)have語(yǔ)句引入并隨后證明輔助引理的完整證明腳本。然而，對(duì)于與Lean 4引擎交互的純逐步證明器，如果策略嘗試引入未經(jīng)證明的引理或需要立即滿足子證明的復(fù)雜結(jié)構(gòu)，Lean引擎通常會(huì)引發(fā)錯(cuò)誤并停止該證明路徑。證明器無(wú)法輕易"暫停"主證明，獨(dú)立證明引理，然后恢復(fù)，所有這些都在單個(gè)交互步驟中完成。

這意味著MPS-Prover，像其他當(dāng)前的逐步證明器一樣，在自主發(fā)現(xiàn)和利用不在上下文或標(biāo)準(zhǔn)庫(kù)中的復(fù)雜中間引理方面不太擅長(zhǎng)。雖然多視角搜索可以使用現(xiàn)有策略找到高效路徑，但它不固有支持自包含方式生成和證明新的、非平凡引理，就像整體證明生成器可能計(jì)劃的那樣。這限制了證明器將非常復(fù)雜的問(wèn)題分解為更可管理的、依賴引理的子問(wèn)題的能力。

研究團(tuán)隊(duì)將解決這一限制作為未來(lái)工作的關(guān)鍵方向。正如他們?cè)诮Y(jié)論中提到的，探索結(jié)合MPS-Prover的逐步搜索能力與整體證明生成方法的全局規(guī)劃和引理處理優(yōu)勢(shì)的混合方法，可能會(huì)提供一條有前途的道路來(lái)克服這一挑戰(zhàn)，進(jìn)一步擴(kuò)大自動(dòng)證明定理的范圍。

七、結(jié)論與影響

MPS-Prover的創(chuàng)新展示了如何通過(guò)訓(xùn)練數(shù)據(jù)的精心設(shè)計(jì)和先進(jìn)的搜索策略來(lái)提高自動(dòng)定理證明的性能。事實(shí)上，MPS-Prover不僅在性能上超越了其他逐步證明器，還在生成的證明簡(jiǎn)潔性和多樣性方面表現(xiàn)出色。

這項(xiàng)研究對(duì)人工智能和形式化數(shù)學(xué)領(lǐng)域有幾個(gè)重要影響：

首先，它展示了大型語(yǔ)言模型在逐步自動(dòng)定理證明中的強(qiáng)大能力，進(jìn)一步證明了人工智能在數(shù)學(xué)推理中的潛力。其次，MPS-Prover生成的證明更短、更多樣，這表明它不僅能找到正確的證明，還能找到更高效的路徑。這對(duì)于實(shí)際應(yīng)用中的形式驗(yàn)證特別有價(jià)值。第三，該研究為未來(lái)的混合證明器開(kāi)發(fā)提供了有價(jià)值的見(jiàn)解，結(jié)合了逐步和整體方法的優(yōu)勢(shì)。

隨著自動(dòng)定理證明系統(tǒng)的不斷發(fā)展，我們可以期待它們?cè)谛问交匾獢?shù)學(xué)定理、驗(yàn)證軟件和硬件系統(tǒng)，甚至可能幫助數(shù)學(xué)家驗(yàn)證新猜想方面發(fā)揮越來(lái)越重要的作用。MPS-Prover是這一激動(dòng)人心旅程中的重要一步，為探索更強(qiáng)大、更可靠的自動(dòng)定理證明系統(tǒng)提供了堅(jiān)實(shí)的框架和全面的分析。