Pixels, Patterns, but No Poetry: To See The World like Humans

2025-07-21｜UCAS, NJU, NUS, BUPT, NKU, PSU, PKU, BJTU|??46

???http://arxiv.org/abs/2507.16863v1????
????https://huggingface.co/papers/2507.16863????
????https://TuringEyeTest.github.io???

研究背景與意義

• 多模態(tài)大語(yǔ)言模型（MLLMs）近年來(lái)在視覺(jué)理解與語(yǔ)言處理的結(jié)合上取得了顯著進(jìn)展，成為人工智能領(lǐng)域的重要研究方向。
• 盡管已有研究多聚焦于提升MLLMs的推理能力，但“MLLMs是否能像人類一樣感知世界”的根本問(wèn)題尚未解決。
• 本文提出了“圖靈之眼測(cè)試”（Turing Eye Test, TET），一個(gè)專注于感知能力的基準(zhǔn)測(cè)試，設(shè)計(jì)了四個(gè)診斷任務(wù)，考察模型對(duì)合成人類直觀處理的圖像的感知表現(xiàn)。
• 研究發(fā)現(xiàn)，當(dāng)前最先進(jìn)的MLLMs在這些感知任務(wù)上表現(xiàn)極差，顯示出視覺(jué)感知與理解方面的顯著瓶頸，尤其是視覺(jué)編碼器（vision tower）的泛化能力不足，而非語(yǔ)言推理或知識(shí)能力的缺陷。

研究方法與創(chuàng)新

• 基準(zhǔn)設(shè)計(jì)創(chuàng)新：TET基于四個(gè)視覺(jué)感知任務(wù)構(gòu)建，涵蓋隱藏文本識(shí)別、3D驗(yàn)證碼識(shí)別、色盲測(cè)試圖案識(shí)別以及復(fù)雜漢字結(jié)構(gòu)識(shí)別，任務(wù)設(shè)計(jì)貼近人類直觀視覺(jué)感知，區(qū)別于傳統(tǒng)以推理為核心的多模態(tài)評(píng)測(cè)。
• 多模型廣泛評(píng)測(cè)：選取15個(gè)不同架構(gòu)和規(guī)模的MLLMs，涵蓋統(tǒng)一多模態(tài)模型、閉源API模型及開(kāi)源模型，全面評(píng)估其在TET任務(wù)上的表現(xiàn)，體現(xiàn)了研究的廣泛適用性和代表性。
• 深入機(jī)制分析：利用Grad-CAM技術(shù)揭示模型視覺(jué)編碼器及語(yǔ)言解碼器的注意力分布，發(fā)現(xiàn)模型難以準(zhǔn)確聚焦關(guān)鍵視覺(jué)區(qū)域，視覺(jué)編碼器常偏重整體物體特征而忽視文本或細(xì)節(jié)特征，語(yǔ)言解碼器則缺乏對(duì)視覺(jué)信息的有效利用。
• 細(xì)粒度微調(diào)實(shí)驗(yàn)：通過(guò)監(jiān)督微調(diào)對(duì)模型不同組件（視覺(jué)編碼器、語(yǔ)言骨干、視覺(jué)語(yǔ)言適配器等）進(jìn)行參數(shù)更新，發(fā)現(xiàn)僅視覺(jué)編碼器微調(diào)能顯著提升任務(wù)表現(xiàn)，驗(yàn)證了視覺(jué)編碼器泛化能力的核心瓶頸。
• 學(xué)習(xí)范式探索：嘗試上下文學(xué)習(xí)（in-context learning）以提升模型感知能力，結(jié)果顯示上下文示例對(duì)感知任務(wù)無(wú)明顯提升，進(jìn)一步凸顯架構(gòu)及視覺(jué)表征的根本限制。
• 圖像處理實(shí)驗(yàn)：通過(guò)對(duì)輸入圖像進(jìn)行下采樣和模糊處理，發(fā)現(xiàn)下采樣能提升模型在隱藏文本任務(wù)上的表現(xiàn)，說(shuō)明視覺(jué)編碼器對(duì)圖像分塊處理機(jī)制的敏感性及當(dāng)前視覺(jué)特征提取方法的局限。
• 理論基礎(chǔ)：研究基于視覺(jué)編碼器（如ViT）與語(yǔ)言模型的聯(lián)合架構(gòu)，強(qiáng)調(diào)視覺(jué)編碼器對(duì)感知任務(wù)的核心作用，提出感知與推理能力需分開(kāi)考察，呼吁未來(lái)結(jié)合感知階段的推理能力以提升視覺(jué)泛化。

實(shí)驗(yàn)設(shè)計(jì)與結(jié)果分析

• 數(shù)據(jù)集構(gòu)建：TET包含四個(gè)子任務(wù)，分別為150張隱藏文本圖像、150個(gè)3D驗(yàn)證碼、150張色盲測(cè)試圖以及40個(gè)復(fù)雜漢字組合，任務(wù)難度設(shè)計(jì)貼近人類直覺(jué)，確保評(píng)測(cè)的真實(shí)性和挑戰(zhàn)性。
• 模型評(píng)測(cè)結(jié)果：15個(gè)MLLMs在四個(gè)任務(wù)上的Pass@1和Pass@32指標(biāo)均極低，多數(shù)任務(wù)表現(xiàn)為零，最高也未超過(guò)約5%，顯示模型在感知任務(wù)上的“災(zāi)難性失敗”。
• 性能曲線：隨著Pass@K增大，模型表現(xiàn)提升極其有限，說(shuō)明增加生成嘗試次數(shù)無(wú)法彌補(bǔ)視覺(jué)感知的根本不足。
• Grad-CAM可視化：模型視覺(jué)編碼器注意力多偏離關(guān)鍵字符區(qū)域，語(yǔ)言解碼器注意力散亂，表明模型未能有效聚焦任務(wù)相關(guān)視覺(jué)信息。
• 微調(diào)效果：僅視覺(jué)編碼器微調(diào)顯著提升準(zhǔn)確率（最高達(dá)90%以上），而語(yǔ)言骨干微調(diào)或視覺(jué)語(yǔ)言適配器微調(diào)效果甚微，驗(yàn)證視覺(jué)編碼器是當(dāng)前性能瓶頸。
• 上下文學(xué)習(xí)無(wú)效：多模型上下文學(xué)習(xí)示例加入后，感知任務(wù)表現(xiàn)無(wú)明顯提升，反映出知識(shí)補(bǔ)充無(wú)法解決感知架構(gòu)缺陷。
• 圖像處理影響：下采樣處理提升隱藏文本任務(wù)表現(xiàn)，模糊處理效果不佳，揭示視覺(jué)編碼器對(duì)圖像分塊的依賴性及潛在的視覺(jué)特征提取不足。

結(jié)論與展望

• 本文通過(guò)TET基準(zhǔn)揭示了當(dāng)前最先進(jìn)的多模態(tài)大語(yǔ)言模型在視覺(jué)感知方面存在的根本性缺陷，尤其是視覺(jué)編碼器泛化能力不足，導(dǎo)致模型無(wú)法像人類一樣直觀地理解圖像內(nèi)容。
• 研究明確區(qū)分了視覺(jué)感知與語(yǔ)言推理能力，指出提升模型推理能力不足以解決感知瓶頸，強(qiáng)調(diào)未來(lái)工作應(yīng)聚焦視覺(jué)編碼器的結(jié)構(gòu)改進(jìn)和視覺(jué)泛化能力提升。
• 微調(diào)實(shí)驗(yàn)表明，針對(duì)視覺(jué)編碼器的專門訓(xùn)練是提升感知能力的關(guān)鍵路徑。
• 建議未來(lái)探索將推理能力注入感知階段，融合像GRPO等先進(jìn)訓(xùn)練方法，以促進(jìn)視覺(jué)編碼器對(duì)復(fù)雜視覺(jué)模式的理解和泛化。
• 計(jì)劃發(fā)布更豐富多樣的TET任務(wù)集，推動(dòng)多模態(tài)模型在感知能力評(píng)測(cè)和提升上的持續(xù)進(jìn)步，促進(jìn)構(gòu)建更接近人類視覺(jué)認(rèn)知的智能系統(tǒng)。

Can One Domain Help Others? A Data-Centric Study on Multi-Domain Reasoning via Reinforcement Learning

2025-07-23｜OpenDataLab, Shanghai AI Lab|??23

???http://arxiv.org/abs/2507.17512v1????
????https://huggingface.co/papers/2507.17512????
????https://github.com/Leey21/A-Data-Centric-Study???

研究背景與意義

• 研究背景：隨著大型語(yǔ)言模型（LLMs）推理能力的快速發(fā)展，強(qiáng)化學(xué)習(xí)與可驗(yàn)證獎(jiǎng)勵(lì)（RLVR）成為提升模型推理水平的重要范式?，F(xiàn)有研究多聚焦于單一領(lǐng)域（如數(shù)學(xué)、編程、邏輯推理）的強(qiáng)化學(xué)習(xí)應(yīng)用，然而現(xiàn)實(shí)應(yīng)用往往涉及多領(lǐng)域綜合推理，領(lǐng)域間的交互機(jī)制尚未充分理解。
• 研究意義：本研究系統(tǒng)性探討了數(shù)學(xué)、代碼生成和邏輯謎題三大推理領(lǐng)域在RLVR框架下的協(xié)同訓(xùn)練效果，揭示了跨領(lǐng)域訓(xùn)練的互補(bǔ)性與沖突，深入分析了監(jiān)督微調(diào)（SFT）、課程學(xué)習(xí)、獎(jiǎng)勵(lì)設(shè)計(jì)及語(yǔ)言差異對(duì)多領(lǐng)域推理性能的影響，旨在為構(gòu)建具備綜合推理能力的多領(lǐng)域強(qiáng)化學(xué)習(xí)模型提供理論和實(shí)踐指導(dǎo)。

研究方法與創(chuàng)新

• 技術(shù)框架：采用Group Relative Policy Optimization（GRPO）算法，結(jié)合Qwen-2.5-7B模型家族，針對(duì)數(shù)學(xué)、代碼、邏輯謎題三領(lǐng)域構(gòu)建了多維度訓(xùn)練與評(píng)估體系，涵蓋單域訓(xùn)練、跨域聯(lián)合訓(xùn)練、監(jiān)督微調(diào)前后的對(duì)比分析，以及課程學(xué)習(xí)和獎(jiǎng)勵(lì)設(shè)計(jì)的系統(tǒng)探究。
• 創(chuàng)新點(diǎn)：

多領(lǐng)域系統(tǒng)性分析：首次系統(tǒng)揭示數(shù)學(xué)、代碼與邏輯推理三領(lǐng)域在強(qiáng)化學(xué)習(xí)中的相互作用，包括相互促進(jìn)與潛在沖突。

監(jiān)督微調(diào)與強(qiáng)化學(xué)習(xí)結(jié)合：深入比較基礎(chǔ)模型與經(jīng)過(guò)指令微調(diào)模型在強(qiáng)化學(xué)習(xí)中的表現(xiàn)差異，明確SFT對(duì)RL效果的關(guān)鍵促進(jìn)作用。

課程學(xué)習(xí)策略創(chuàng)新：提出策略刷新機(jī)制，通過(guò)階段性更新參考模型和優(yōu)化器狀態(tài)，顯著提升課程學(xué)習(xí)的收斂速度和最終性能。

獎(jiǎng)勵(lì)設(shè)計(jì)多樣化：針對(duì)不同任務(wù)特性設(shè)計(jì)并比較二元獎(jiǎng)勵(lì)、部分獎(jiǎng)勵(lì)、格式獎(jiǎng)勵(lì)和重新縮放獎(jiǎng)勵(lì)，優(yōu)化訓(xùn)練信號(hào)以提升學(xué)習(xí)效率。

語(yǔ)言敏感性研究：首次系統(tǒng)評(píng)估中文與英文訓(xùn)練數(shù)據(jù)對(duì)模型推理能力的影響，發(fā)現(xiàn)語(yǔ)言差異顯著影響RLVR的泛化能力。

• 理論基礎(chǔ)：基于強(qiáng)化學(xué)習(xí)理論，結(jié)合多任務(wù)學(xué)習(xí)與遷移學(xué)習(xí)原理，構(gòu)建了適應(yīng)多領(lǐng)域推理的訓(xùn)練框架，突破了傳統(tǒng)單域強(qiáng)化學(xué)習(xí)的局限。

實(shí)驗(yàn)設(shè)計(jì)與結(jié)果分析

• 實(shí)驗(yàn)設(shè)計(jì)：

使用數(shù)學(xué)（DeepScaleR、CountDown）、代碼（CodeR1-12k）、邏輯謎題（Knights-and-Knaves、LogicPuzzleBaron）數(shù)據(jù)集，統(tǒng)一規(guī)模采樣，確保多領(lǐng)域訓(xùn)練數(shù)據(jù)平衡。

評(píng)估采用多任務(wù)基準(zhǔn)，包括MATH500、AIME24、HumanEval、MBPP及ZebraLogicBench，覆蓋不同推理難度與類型。

訓(xùn)練配置細(xì)致調(diào)整，數(shù)學(xué)任務(wù)設(shè)置更長(zhǎng)的推理鏈條，代碼任務(wù)采用安全沙箱執(zhí)行環(huán)境，邏輯謎題任務(wù)設(shè)計(jì)多階段課程學(xué)習(xí)。

• 關(guān)鍵結(jié)果：

單域訓(xùn)練中，數(shù)學(xué)與邏輯推理任務(wù)互相促進(jìn)，提升模型推理深度；代碼訓(xùn)練提升代碼生成能力，但對(duì)基礎(chǔ)模型存在一定抑制效應(yīng)。

多域聯(lián)合訓(xùn)練表現(xiàn)出復(fù)雜的協(xié)同效應(yīng)，雙域和三域組合均提升整體性能，但不同任務(wù)間的沖突需通過(guò)精細(xì)設(shè)計(jì)緩解。

模板一致性對(duì)模型性能至關(guān)重要，訓(xùn)練與測(cè)試模板不匹配會(huì)顯著降低推理準(zhǔn)確率，暴露當(dāng)前RLVR方法在模板魯棒性上的不足。

課程學(xué)習(xí)顯著提升模型在復(fù)雜邏輯謎題上的表現(xiàn)，策略刷新機(jī)制加快收斂并提高最終精度，驗(yàn)證了分階段訓(xùn)練的有效性。

獎(jiǎng)勵(lì)設(shè)計(jì)對(duì)模型訓(xùn)練影響顯著，部分獎(jiǎng)勵(lì)在復(fù)雜任務(wù)中優(yōu)于簡(jiǎn)單二元獎(jiǎng)勵(lì)，合理調(diào)整獎(jiǎng)勵(lì)函數(shù)有助于提升訓(xùn)練穩(wěn)定性和泛化能力。

語(yǔ)言差異導(dǎo)致性能差距，英文訓(xùn)練數(shù)據(jù)普遍優(yōu)于中文，提示未來(lái)需針對(duì)多語(yǔ)言環(huán)境優(yōu)RLVR策略。

統(tǒng)計(jì)顯著性：所有提升均在多次實(shí)驗(yàn)中重復(fù)驗(yàn)證，顯著優(yōu)于基線，展示了方法的穩(wěn)健性和廣泛適用性。

結(jié)論與展望

• 總結(jié)貢獻(xiàn)：

本文首次系統(tǒng)性揭示多領(lǐng)域強(qiáng)化學(xué)習(xí)推理的內(nèi)在機(jī)制和交互效應(yīng)，明確了數(shù)學(xué)、代碼和邏輯推理三領(lǐng)域的協(xié)同與沖突關(guān)系。

創(chuàng)新性地結(jié)合監(jiān)督微調(diào)、課程學(xué)習(xí)和多樣化獎(jiǎng)勵(lì)設(shè)計(jì)，顯著提升了多領(lǐng)域推理模型的性能與泛化能力。

通過(guò)詳細(xì)的模板一致性和語(yǔ)言敏感性分析，指出了當(dāng)前強(qiáng)化學(xué)習(xí)推理方法的關(guān)鍵瓶頸和改進(jìn)方向。

• 局限性分析：

當(dāng)前研究主要基于7B參數(shù)規(guī)模模型，尚未驗(yàn)證更大規(guī)模模型的適用性和擴(kuò)展性。

語(yǔ)言敏感性分析集中于中英文，缺少更多語(yǔ)言的廣泛驗(yàn)證。

多領(lǐng)域訓(xùn)練中任務(wù)權(quán)重和數(shù)據(jù)比例的自動(dòng)調(diào)節(jié)機(jī)制仍待深入研究，以進(jìn)一步緩解領(lǐng)域間沖突。

• 未來(lái)展望：

探索更大規(guī)模模型和更復(fù)雜任務(wù)的多領(lǐng)域強(qiáng)化學(xué)習(xí)訓(xùn)練，推動(dòng)模型推理能力向更高層次發(fā)展。

開(kāi)發(fā)更魯棒的模板設(shè)計(jì)和自適應(yīng)訓(xùn)練策略，提升模型在不同應(yīng)用場(chǎng)景下的泛化穩(wěn)定性。

深入研究多語(yǔ)言、多文化背景下的強(qiáng)化學(xué)習(xí)推理，構(gòu)建真正通用的跨領(lǐng)域推理模型。

引入自動(dòng)化數(shù)據(jù)選擇和任務(wù)調(diào)度機(jī)制，優(yōu)化多領(lǐng)域訓(xùn)練過(guò)程，最大化協(xié)同效應(yīng)，減少負(fù)遷移。

Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny

2025-07-22｜Shanghai AI Lab|??15

???http://arxiv.org/abs/2507.16331v1????
????https://huggingface.co/papers/2507.16331????
????https://github.com/Veri-Code/ReForm???

研究背景與意義

1. 研究背景隨著大型語(yǔ)言模型（LLMs）在自動(dòng)代碼生成領(lǐng)域的迅猛發(fā)展，確保生成代碼的正確性成為關(guān)鍵挑戰(zhàn)，尤其是在安全關(guān)鍵領(lǐng)域如醫(yī)療、金融和自動(dòng)駕駛中。傳統(tǒng)的單元測(cè)試和人工代碼審查存在覆蓋不足和依賴專家經(jīng)驗(yàn)的局限，形式化驗(yàn)證作為一種數(shù)學(xué)上嚴(yán)謹(jǐn)?shù)奶娲桨福芴峁┏绦蛐袨榈膰?yán)格證明。然而，現(xiàn)有LLMs在形式化驗(yàn)證任務(wù)中表現(xiàn)不佳，主要因數(shù)據(jù)稀缺和對(duì)人類先驗(yàn)知識(shí)的高度依賴。
2. 研究意義本文首次系統(tǒng)探討了如何減少對(duì)人類先驗(yàn)的依賴，通過(guò)將LLMs置于形式語(yǔ)言Dafny的環(huán)境中，實(shí)現(xiàn)自動(dòng)且可擴(kuò)展的形式軟件驗(yàn)證。該研究不僅突破了傳統(tǒng)依賴大量人工注釋的瓶頸，還為未來(lái)實(shí)現(xiàn)大規(guī)模、可靠的形式化軟件驗(yàn)證奠定了基礎(chǔ)。通過(guò)自動(dòng)生成和驗(yàn)證形式規(guī)范，本文推動(dòng)了代碼生成向真正語(yǔ)義理解和行為保證的轉(zhuǎn)變。

研究方法與創(chuàng)新

1. 技術(shù)方法描述研究設(shè)計(jì)了一套端到端自動(dòng)化的數(shù)據(jù)構(gòu)建和訓(xùn)練管線，核心包括：

• 數(shù)據(jù)構(gòu)建：利用LLMs自動(dòng)生成Dafny代碼及其形式規(guī)范，結(jié)合Python代碼轉(zhuǎn)換和自動(dòng)迭代驗(yàn)證修正，完全去除人工單樣本注釋。
• 基準(zhǔn)設(shè)計(jì)：構(gòu)建了DafnyComp基準(zhǔn)，涵蓋合成的復(fù)雜多函數(shù)程序，支持評(píng)估模型的組合推理和跨域泛化能力。
• 訓(xùn)練策略：采用兩階段訓(xùn)練，先通過(guò)有限監(jiān)督微調(diào)（SFT）掌握基礎(chǔ)語(yǔ)法和語(yǔ)義，再利用強(qiáng)化學(xué)習(xí)（RL）結(jié)合Dafny自動(dòng)驗(yàn)證信號(hào)進(jìn)行開(kāi)放式探索和策略優(yōu)化。
• 獎(jiǎng)勵(lì)設(shè)計(jì)：創(chuàng)新引入三類獎(jiǎng)勵(lì)機(jī)制——語(yǔ)法正確性獎(jiǎng)勵(lì)、驗(yàn)證獎(jiǎng)勵(lì)和邏輯子集獎(jiǎng)勵(lì)，后者通過(guò)邏輯蘊(yùn)含關(guān)系衡量生成規(guī)范優(yōu)于或等同于真實(shí)規(guī)范，極大促進(jìn)了模型生成更強(qiáng)、更準(zhǔn)確的規(guī)范。

2. 創(chuàng)新點(diǎn)突出

• 極大降低人類先驗(yàn)依賴：完全摒棄自然語(yǔ)言鏈?zhǔn)剿季S（CoT）和人工注釋，依賴自動(dòng)化數(shù)據(jù)和系統(tǒng)反饋，實(shí)現(xiàn)訓(xùn)練過(guò)程的可擴(kuò)展性。
• 形式語(yǔ)言空間內(nèi)的強(qiáng)化學(xué)習(xí)應(yīng)用：首次將RL反饋完全基于形式驗(yàn)證器的自動(dòng)信號(hào)，保證了獎(jiǎng)勵(lì)的準(zhǔn)確性和嚴(yán)謹(jǐn)性。
• 邏輯子集獎(jiǎng)勵(lì)機(jī)制：創(chuàng)新性地利用形式邏輯關(guān)系指導(dǎo)規(guī)范生成，推動(dòng)模型超越訓(xùn)練數(shù)據(jù)，發(fā)掘更優(yōu)規(guī)范。
• 小模型有效性驗(yàn)證：證明了0.5B至14B參數(shù)規(guī)模模型在該任務(wù)中的有效性，挑戰(zhàn)了大型模型獨(dú)占優(yōu)勢(shì)的常規(guī)認(rèn)知。

3. 理論基礎(chǔ)討論研究基于強(qiáng)化學(xué)習(xí)理論和形式驗(yàn)證的數(shù)學(xué)邏輯基礎(chǔ)，結(jié)合最新的策略優(yōu)化算法（如GRPO），確保訓(xùn)練過(guò)程既能探索新策略，又能穩(wěn)定收斂。形式邏輯中預(yù)條件松弛和后條件強(qiáng)化的驗(yàn)證機(jī)制為獎(jiǎng)勵(lì)設(shè)計(jì)提供了堅(jiān)實(shí)的理論支撐。

實(shí)驗(yàn)設(shè)計(jì)與結(jié)果分析

1. 實(shí)驗(yàn)設(shè)計(jì)

• 模型與數(shù)據(jù)：使用Qwen-2.5架構(gòu)，涵蓋0.5B至14B參數(shù)規(guī)模，訓(xùn)練數(shù)據(jù)包含2萬(wàn)條自動(dòng)注釋的Dafny程序。
• 訓(xùn)練流程：先進(jìn)行有限監(jiān)督微調(diào)，再以Dafny驗(yàn)證器為反饋信號(hào)進(jìn)行強(qiáng)化學(xué)習(xí)，訓(xùn)練細(xì)節(jié)包括采樣溫度、批量大小和學(xué)習(xí)率等均經(jīng)過(guò)精細(xì)調(diào)優(yōu)。
• 評(píng)估指標(biāo)：采用語(yǔ)法正確率、驗(yàn)證通過(guò)率及規(guī)范優(yōu)越率（SSR）三維度衡量模型性能，特別強(qiáng)調(diào)SSR以體現(xiàn)規(guī)范質(zhì)量提升。

2. 結(jié)果分析

• 監(jiān)督微調(diào)效果顯著：即使是0.5B模型，SFT階段也能達(dá)到80%以上的語(yǔ)法正確率，優(yōu)于GPT-4o等大型商業(yè)模型。
• 強(qiáng)化學(xué)習(xí)帶來(lái)實(shí)質(zhì)提升：RL階段不僅提升了語(yǔ)法和驗(yàn)證通過(guò)率，更顯著提高了規(guī)范優(yōu)越率，表現(xiàn)出模型在探索更優(yōu)規(guī)范方面的能力。
• 模型規(guī)模效應(yīng)明顯：隨著模型參數(shù)增長(zhǎng)，性能持續(xù)提升，尤其是在驗(yàn)證通過(guò)率和規(guī)范優(yōu)越率上展現(xiàn)出良好的擴(kuò)展性。
• 探索能力驗(yàn)證：RL訓(xùn)練產(chǎn)生了超出訓(xùn)練語(yǔ)料的新穎且語(yǔ)義豐富的規(guī)范，證明了RL驅(qū)動(dòng)的探索有效突破了監(jiān)督學(xué)習(xí)的局限。
• 消除CoT影響：實(shí)驗(yàn)中完全去除自然語(yǔ)言鏈?zhǔn)剿季S，確保性能提升源于模型在形式語(yǔ)言空間內(nèi)的真實(shí)推理能力而非人工提示。

結(jié)論與展望

1. 研究貢獻(xiàn)總結(jié)本文提出了一種極大減少人類先驗(yàn)、依賴自動(dòng)化形式驗(yàn)證反饋的訓(xùn)練管線，實(shí)現(xiàn)了小規(guī)模LLMs在形式軟件驗(yàn)證任務(wù)中的突破。通過(guò)創(chuàng)新的獎(jiǎng)勵(lì)設(shè)計(jì)和數(shù)據(jù)構(gòu)建方法，模型展現(xiàn)出強(qiáng)大的組合推理和泛化能力，超越了現(xiàn)有商業(yè)模型。該工作為實(shí)現(xiàn)大規(guī)模、可靠的自動(dòng)形式化驗(yàn)證奠定了堅(jiān)實(shí)基礎(chǔ)。
2. 局限性分析

• 數(shù)據(jù)仍主要依賴自動(dòng)生成和合成，真實(shí)世界代碼的多樣性和復(fù)雜度可能導(dǎo)致泛化挑戰(zhàn)。
• Dafny驗(yàn)證器雖強(qiáng)大，但完備性有限，可能影響?yīng)剟?lì)信號(hào)的絕對(duì)準(zhǔn)確性。
• 訓(xùn)練資源消耗較大，尤其是中大型模型的RL訓(xùn)練，限制了更大規(guī)模模型的探索。

3. 未來(lái)方法展望

• 探索更豐富的形式語(yǔ)言和驗(yàn)證工具，提升獎(jiǎng)勵(lì)信號(hào)的全面性和準(zhǔn)確性。
• 結(jié)合符號(hào)執(zhí)行和靜態(tài)分析等多模態(tài)驗(yàn)證手段，增強(qiáng)模型對(duì)復(fù)雜程序行為的理解。
• 研究更高效的RL算法和模型蒸餾技術(shù)，降低訓(xùn)練成本，推動(dòng)更大規(guī)模模型的應(yīng)用。
• 拓展到多語(yǔ)言、多范式的形式化驗(yàn)證，提升跨領(lǐng)域適應(yīng)性和實(shí)用價(jià)值。

本文轉(zhuǎn)載自?????AI研究前瞻?????，作者：胡耀淇