babble: Learning Better Abstractions with E-Graphs andAnti-Unification

babble：利用 E-Graph 和反統一學習更好的抽象

https://arxiv.org/pdf/2212.04596#page=26.74

庫學習通過從程序語料庫中提取公共結構到可重用的庫函數來壓縮給定的程序語料庫。先前關于庫學習的工作受到兩個限制，這兩個限制阻礙了它擴展到更大、更復雜的輸入。首先，它探索了太多對壓縮無用的候選庫函數。其次，它對輸入的句法變化不健壯。

我們提出了庫學習模理論（LLMT），這是一種新的庫學習算法，它還接受給定問題領域的等式理論作為輸入。LLMT使用e-graphs和等式飽和來緊湊地表示等價于模理論的程序空間，并使用一種新的e-graph反統一技術來更直接和高效地在語料庫中找到共同模式。

我們在名為babble的工具中實現了LLMT。我們的評估表明，babble實現的壓縮速度比現有技術快幾個數量級。我們還會提供一個定性評估，顯示babble在以前庫學習無法觸及的輸入上學習可重用函數。

CCS概念：?軟件及其工程→函數式語言；自動編程。

其他關鍵詞和短語：庫學習，e-graphs，反統一

1 引言

抽象是管理軟件復雜性的關鍵。有經驗的程序員通常會將共同的功能提取到庫中，以更清晰、更簡潔的方式表達他們的意圖。如果這個過程可以從代碼中自動提取有用的抽象，那會怎樣？庫學習試圖用技術來回答這個問題，通過提取公共結構到可重用的庫函數來壓縮給定的程序語料庫。庫學習有許多潛在的應用，從重構和反編譯[Jones等人2021；Nandi等人2020]，到模擬人類認知[Wang等人2021；Wong等人2022]，以及通過專門針對選定問題領域的目標語言來加速程序合成[Ellis等人2021]。

考慮圖1中的簡單庫學習任務。左側，圖1a顯示了Wong等人[2022]中的一個2d cad DSL的三個程序語料庫。每個程序對應于由多個旋轉線段組成的規則多邊形組成的圖片。右側，圖1b顯示了一個學習到的庫，其中有一個名為f0的函數，它抽象了縮放規則多邊形的構造。然后可以使用學到的f0將三個輸入程序重構為更簡潔的形式。f0是否是這個語料庫的“最佳”抽象通常很難量化。在本文中，我們遵循[Ellis等人2021]，并使用壓縮作為庫學習的度量，即目標是減少語料庫在AST節點中的總大小（從208減少到72圖1）。重要的是，語料庫的總大小包括庫的大小：這防止了庫學習生成太多過于特定的函數，而是偏向于更通用和可重用的抽象。

**庫學習可以表述為一個程序合成問題，分為兩個階段：生成候選抽象，接著選擇那些能產生最佳（最小）重構語料庫的抽象**。最先進的技術實現于 DreamCoder [Ellis 等人，2021]，但在擴展庫學習到更大和更現實的輸入時，存在兩個主要限制：

- 候選生成不夠精準：DreamCoder 會生成許多無用的候選抽象，減慢了選擇階段和整個算法的速度。

- 該技術純粹是句法性的，因此無法對表面上的變化具備魯棒性。例如，人類程序員會立即知道表達式 `2 + 1` 和 `1 + 3` 可以使用抽象 `λx. x + 1` 進行重構，因為加法是可交換的；而純粹的句法庫學習方法無法生成這種抽象。

在本文中，我們提出了**基于理論（等式）庫學習（LLMT）**的新算法，解決了上述兩大限制。

**通過反統一實現精準候選生成**。為了使候選生成更精準，LLMT 利用了兩個關鍵觀察：

- 有用的抽象必須在語料庫中至少使用兩次。例如，在包含兩個程序 `2 + 1` 和 `3 + 1` 的語料庫中，不需要考慮抽象 `λx. 3 + x`，因為它只能在一個地方使用，因此只會增加語料庫的大小。

- 抽象應該“盡可能具體”以適應給定的語料庫。例如，在同樣的語料庫中，抽象 `λx. x + 1` 優于更通用的 `λx y. x + y`，因為它們都適用于同樣的兩個表達式，但后者應用的代價更高（它需要兩個參數）。

換句話說，有用的抽象對應于與原始語料庫中某些子項匹配的最不通用模式；這種模式可以通過反統一（AU）[Plotkin 1970] 計算出來。例如，反統一 `2 + 1` 和 `3 + 1` 生成了模式 `X + 1`，并通過對模式變量 `X` 進行抽象，可以推導出所需的候選庫函數 `λx. x + 1`。類似地，在圖 1 中，可以通過反統一語料庫中的藍色和棕色子項推導出抽象 `f0`。

**通過 E-Graphs 實現魯棒性**。為了使候選生成更具魯棒性，LLMT 還接收特定領域的等式理論作為輸入，并使用該理論找到與原始語料庫語義等價但具有更多語法結構相似性的程序。例如，在算術領域中，我們期望理論中包含方程 `X + Y ≡ Y + X`，表明加法是交換的。給定包含 `2 + 1` 和 `1 + 3` 的語料庫，該規則可用于將第二個表達式重寫為 `3 + 1`，從而發現共同的抽象 `λx. x + 1`。

這種方法的主要挑戰是在與原始語料庫語義等價的程序的大空間中進行搜索。為此，LLMT 依賴于 e-graph 數據結構和等式飽和技術 [Tate 等人 2009；Willsey 等人 2021] 來計算和表示語義等價程序的空間。為了在此空間上實現高效的庫學習，我們提出了一種新的候選生成算法，該算法使用動態規劃高效地計算由 e-graph 表示的子項對之間的所有反統一集。

最后，在此設置中選擇最優庫歸結為從 e-graph 中提取出包含公共子表達式的最小項的問題。該問題在其一般形式中極具計算復雜性，現有的方法在可擴展性方面有限 [Yang 等人 2021]。因此，我們提出了一種新的 e-graph 提取算法，稱為**目標子表達式消除**，該算法利用特定領域的知識來減少搜索空間，并通過束搜索支持近似，以權衡準確性和效率。

**babble**。我們在工具 babble 中實現了 LLMT，它基于 egg e-graph 庫構建 [Willsey 等人 2021]。babble 的工作流程概述如圖2所示，灰色框代表現有技術，黑色框代表我們的貢獻。我們在兩個來源的基準上評估了 babble：從 DreamCoder 運行中提取的壓縮任務 [Bowers 2022] 和用于評估人類概念學習的二維 CAD 程序 [Wong 等人 2022]。我們的評估表明，babble 在其自己的基準上超越了 DreamCoder，在更短的時間內實現了更好的壓縮。添加特定領域的重寫規則進一步提高了壓縮效果。我們還展示了 babble 在更大的二維 CAD 語料庫中的可擴展性，這超出了 DreamCoder 的能力范圍。最后，我們展示并討論了 babble 學習到的抽象，證明了 LLMT 方法可以學習符合人類直覺的函數。

貢獻。總結來說，本文做出了以下貢獻：

? 基于等式理論的庫學習：一個可以結合任意領域特定的等式理論來使學習對句法變化更加健壯的庫學習算法；

? e-graph反統一：一個使用從術語擴展到e-graphs的反統一機制高效生成候選抽象集的算法；

? 有針對性的公共子表達式消除：一種新的近似算法，用于在存在公共子表達式的情況下從e-graph中提取最佳術語。

2 概述

我們通過一個運行示例來說明LLMT，該示例建立在圖1的基礎上。圖1中的輸入語料庫是用Wong等人[2022]的2d cad DSL編寫的，它具有以下原語：

也就是說，一個六邊形邊變形xform(line, [1, 0, ?0.5, 0.5/tan(/6)])重復六次，每次旋轉2/6弧度，得到的單位六邊形再被縮放2倍。

然而，仔細觀察圖1中的兩個藍色六邊形，我們會注意到一些奇特之處。圖1中xform(repeat . . . , [1, 0, 0, 0])的兩個出現是無操作：它們僅將一個圖形按1的因子縮放，既不旋轉也不平移。如果代碼是手工編寫的或從低級表示（像Szalinski這樣的工具[Nandi等人2020]）反編譯的，這些冗余的變換可能不會出現；但它們對于我們希望使用純句法技術學習最優抽象0至關重要。

圖3顯示了圖1中語料庫的簡化和“更自然”的版本，它消除了這些無操作變換。正如圖中所示，這導致純句法技術學習了一個不同的函數1，它抽象了一個未縮放的單位多邊形。因為縮放變換現在在抽象之外，所以它必須重復五次。結果，盡管簡化的輸入語料庫C比原始語料庫A更小（196個AST節點而不是208個），但它的壓縮版本D更大（81個AST節點而不是72個）！換句話說，句法庫學習對于保持語義的代碼變化是不健壯的。

相比之下，我們的工具babble可以接受簡化的語料庫C作為輸入，并且在不到一秒的時間內發現縮放的多邊形抽象0，得到大小為72的壓縮語料庫B。

在本節的剩余部分，我們將說明babble如何使用我們的新算法——基于等式理論的庫學習（LLMT）——實現這一點。

簡化的DSL。在本節的剩余部分，我們使用一個定制版本的2d cad DSL，增加了以下額外構造：

這些可以在原始DSL中表達，并且如果給定適當的語料庫，甚至可以通過庫學習發現；為了簡化表述，我們在這里將它們視為原語。

2.1 使用E-Graphs表示等價項

為了在庫學習中利用等價關系，babble接受領域特定的等式理論作為輸入。對于我們的運行示例，讓我們假設該理論包含一個單一的等式：

**該等式規定任何圖形 等價于自身縮放為 1 的情況**。有了這個等式后，就可以將語料庫 C “重寫”成語料庫 A，并通過純句法技術從中學習到最優的壓縮語料庫 B。挑戰在于，語料庫 C 可以被重寫成無限多的其他語料庫；如何選擇能夠最大化句法對齊、從而增加發現最優抽象機會的語料庫？

與其嘗試猜測最佳的等價語料庫，或逐個枚舉它們，babble 使用**等式飽和技術** [Tate 等人 2009；Willsey 等人 2021]。等式飽和技術以一個術語 和一組重寫規則為輸入，找到在給定規則下與 等價的所有術語空間；這得益于 e-graph 數據結構提供的高度共享特性，可以緊湊地表示生成的空間。

圖 4（左）展示了通過等式飽和技術為圖 3 中的藍色術語構建的 e-graph——在簡化的 DSL 中表示為 `repRot(side(6), 6, 2/6)`——使用重寫規則（1）。圖中的藍色部分代表原始術語，灰色部分則是通過等式飽和技術添加的。e-graph 中的實線矩形表示 e-nodes（類似于常規的 AST 節點），而虛線矩形表示 e-classes（表示術語的等價類）。重要的是，e-graph 中的邊從 e-nodes 指向 e-classes，這使得可以緊湊地表示子項中存在變化的程序：例如，將 e-class 1 作為 repRot 節點的第一個子節點，可以同時表示術語 `repRot(side(6), 6, 2/6)` 和 `repRot(scale(side(6), 1), 6, 2/6)`，而不重復它們的共同部分。此外，由于 e-graphs 可以有循環，因此它們也可以表示無限多的術語集：例如，e-class 1 表示的術語形式包括：`side(6)`，`scale(side(6), 1)`，`scale(scale(side(6), 1), 1)`，等等。由于這個 e-graph 表示了在重寫規則（1）下所有等價術語的空間，因此我們庫學習中尋找的術語，即 `scale(repRot(side(6), 6, 2/6), 1)`，也被包含在 e-class 0 中。

2.2 通過E-Graph反統一生成候選

在使用給定的等式理論通過等式飽和運行從給定語料庫構建e-graph之后，庫學習的下一步是生成候選模式，這些模式捕捉語料庫之間的句法相似性。挑戰在于生成足夠少的候選以使庫學習可行，但足夠多以實現良好的壓縮。我們使用圖4（右）中的e-graph來說明候選生成，它代表了我們語料庫的一部分，包括（飽和的）藍色和棕色術語。回想一下，最佳模式——對應于縮放多邊形抽象0——是：

先前在DreamCoder上的工作通過從語料庫中隨機選擇一個片段，然后隨意替換選擇的子術語與模式變量來生成模式。例如，為了生成模式0，DreamCoder需要選擇整個棕色子術語作為一個片段，然后決定對其子術語8和2進行抽象。這種方法成功地將候選集從所有句法上有效的模式限制為至少在語料庫中有一個匹配的模式；然而，由于選擇要抽象的子術語的方式太多，這個空間仍然太大，無法在短程序的小語料庫之外全面探索。在babble中，由于等式飽和，這個問題更加嚴重，因為e-graph通常包含比原始語料庫多出指數級或無限多的程序。

通用性過濾器。為了在babble中進一步修剪可行候選集，我們確定了兩類可以安全丟棄的模式，要么是因為它們太具體，要么是因為它們太抽象。首先，像repRot(side(8), , 2/8)這樣的模式可以丟棄，因為它對于這個語料庫來說太具體了：相應的抽象只能應用一次，本質上是將唯一匹配的術語repRot(side(8), 8, 2/8)替換為( repeat(side(8), , 2/8)) 8，這只會向語料庫中添加更多的AST節點。其次，像repRot(side(), , )這樣的模式可以丟棄，因為它對于這個語料庫來說太抽象了：它匹配的所有地方，更具體的模式repRot(side(), , 2/)也會匹配；使用更具體的模式可以更好地壓縮，因為在它的應用中實際參數既更少也更小：f 6 2/6和f 8 2/8與f 6和f 8相比。

因此，我們的第一個關鍵見解是將候選集限制在與（飽和的）語料庫中的某些子術語對匹配的最具體的模式。例如，模式0是最具體的模式，它匹配這兩個術語

術語反統一。計算與兩個給定術語匹配的最具體模式稱為反統一（AU）[Plotkin 1970; Reynolds 1969]。AU通過簡單的自頂向下遍歷兩個術語來工作，用模式變量替換任何不匹配的構造器。例如，要反統一術語（3）和（4），我們從兩個術語的根開始；由于兩個AST節點共享相同的構造器scale，它成為模式的一部分，我們遞歸進入子節點。我們最終遇到一個不匹配，左側的術語是6，右側的術語是8；所以我們創建一個新的模式變量，并記住反替代 = {(6, 8) ?→ }。當我們在角度的分母中遇到不匹配時，我們在中查找不匹配的術語對(6, 8)；因為我們已經為這對創建了一個變量，我們簡單地返回現有的變量。最后的不匹配是scale的第二個子節點中的(1, 2)；由于這對尚未在中，我們創建第二個模式變量，。此時，得到的反統一結果是模式0（2）。

反統一單個術語對是簡單且高效的。然而，在LLMT中，我們希望反統一所有可能在任何與原始語料庫等價（模給定的等式理論）的語料庫中出現的子術語對。

明確枚舉由e-graph表示的所有等價語料庫，然后對每對子術語進行AU是不可行的。相反，babble直接在e-graph上執行反統一。

從術語到E-類。我們首先解釋如何反統一兩個e-類。這個操作以一對e-類作為輸入，并返回一組主導反統一器，即一組模式，這些模式（1）匹配兩個e-類，并且（2）保證包括兩個e-類表示的術語對的最具體模式中的最佳抽象。

考慮計算圖4（右）中的e-graph的e-類1和4的AU(1, 4)。AU仍然作為自頂向下的遍歷進行，但在這種情況下我們必須檢查兩個e-類是否有任何共同的構造器。在這種情況下，它們確實有：一個side構造器和一個scale構造器。讓我們首先選擇兩個side構造器并遞歸進入它們唯一的子節點，計算AU({6}, {8})。這兩個e-類沒有匹配的構造器，所以AU簡單地返回一個模式變量，類似于術語反統一；這產生了1和4的第一個模式：side 。

然而，記住1和4也有匹配的scale構造器。這就有趣了：這些構造器涉及一個循環（它們的第一個子節點是父e-類本身）。如果我們讓AU跟隨這個循環，反統一器的集合就變得無限：

幸運的是，我們可以展示side 主導了這個集合中的所有其他模式，因為它們的模式變量——在這種情況下，只是——匹配相同的e-類，但它們也更大（在第4節中我們將展示這種支配關系如何讓我們修剪其他模式，不僅僅是由循環引起的模式）。因此，AU(1, 4)簡單地返回{side }。

對于兩個多邊形的根e-類，0和2，按照相同的邏輯，AU(0, 2)產生了模式0（2），這是學習最優抽象所必需的。

從E-類到E-圖。為了獲得所有候選抽象的集合，我們需要對e-graph中所有e-類的對進行反統一。顯然，這些計算有重疊的子問題（例如，我們必須計算AU(1, 4)作為AU(0, 2)和AU(0, 3)的一部分）。

為了避免重復工作，babble使用了一個高效的動態規劃算法，以自底向上的方式處理所有e-類的對。

2.3 通過有針對性的公共子表達式消除進行候選選擇

現在我們來說明babble中庫學習的最后步驟：給定由e-graph反統一生成的候選抽象集，目標是選擇一個子集，以便為整個語料庫提供最佳壓縮。例如，為圖3中的語料庫生成的候選包括：

目前尚不清楚哪種抽象更好：0匹配的術語比2多，但2需要的參數更少（所以如果我們在語料庫中有足夠多的縮放六邊形和只有一個八邊形，可能最好讓八邊形保持不抽象）。另一方面，1可能更好，因為它沒有在藍色六邊形上引入冗余的變換。最后，如果我們同時選擇0和2，我們還可以將2的定義抽象為0 6，從而獲得額外的重用！正如你所見，候選選擇非常復雜，因為它需要考慮到e-graph中不同等價程序的選擇，以及一些抽象可以使用其他抽象來定義的事實。

簡化為E-Graph提取。為了克服這個困難，我們再次利用e-graph和等式飽和。我們的第二個關鍵見解是，選擇最優的抽象子集可以簡化為在存在公共子表達式的情況下從e-graph中提取最小術語的問題。

為了說明這種簡化，讓我們將注意力限制在僅有的兩個候選抽象0和1上，如上所述。babble將每個候選模式及其相應的抽象轉換為一個重寫規則，該規則在語料庫中引入一個局部-抽象，然后應用；對于我們的兩個抽象，這些規則是：

將這些規則應用于圖4（右）中的e-graph的結果如圖5所示。例如，你可以看到e-class 2（代表縮放-2的八邊形）現在存儲了另一種表示形式：0 8 2。e-class 0（單位六邊形）使用0或1都有表示，因為這個類匹配了上述重寫規則（5）和（6）。還要注意，因為-抽象的定義也存儲在e-graph中，等式飽和可以使用這些規則在其主體內部進行應用，使得一個函數使用另一個函數：例如，存儲在0定義中的一個術語是

一旦我們為所有候選抽象構建了帶有局部lambda的e-graph版本，剩下的就是從這個e-graph中提取最小的術語。棘手的部分是我們希望只計算重復lambda的大小一次。例如，在圖5中，0被應用了兩次（在0和2中）；如果術語提取選擇這兩個e-節點，我們希望將它們的第一個子節點（0的定義）視為公共子表達式，其大小只對最終表達式貢獻一次。直觀地說，這是因為我們可以將這些lambda“提升”到頂層的let綁定中，從而只定義一次0，并用名稱替換每個局部lambda。

帶有公共子表達式的提取是一個已知但極其困難的問題，傳統上被簡化為整數線性規劃（ILP）[Wang等人2020；Yang等人2021]。由于ILP方法的可擴展性非常有限，我們開發了一個定制的提取算法，通過使用領域特定知識和近似來更好地擴展。

提取算法。使提取更高效的主要思想是，對于庫學習，我們只對共享某種類型的子術語感興趣：即，-抽象。因此，對于每個e-類，我們只需要跟蹤每個可能的庫（即每個-抽象的子集）的最佳術語。更準確地說，對于每個e-類和庫，我們跟蹤（1）庫的最小大小（2）使用這個庫重構的程序的最小大小（將-抽象計為單個節點）。我們通過e-graph自底向上計算和傳播這些信息。一旦這個信息被計算出來并傳播到根e-類（代表整個語料庫），我們就可以簡單地選擇總大小最小的庫。

例如，對于圖5中的e-類2，對于空庫?，庫的大小是0，最小程序的大小（scale(repRot(side(8), 8, 2/8), 2)）是9；對于庫{0}，庫的大小是9，最小程序的大小（0 2 8）是3；而對于庫{1}，庫的大小是7，最小程序的大小（scale(1 8, 2)）是4。顯然，對于這個e-類，引入庫函數還沒有回報（0 + 9 < 7 + 4 < 9 + 3），因為每個只能使用一次。然而，當我們向根移動時，情況就變了。對于0和2的父e-類，引入{0}和{1}的成本已經被攤銷了：使用空庫的最小程序大小是17，而使用{0}或{1}的最小程序大小是7，所以{1}已經值得引入了（9 + 7 < 0 + 17）。包括更多帶有縮放多邊形的程序最終使得庫{0}成為四個子集中最有利可圖的。

由于在更大的語料庫中，跟蹤所有候選抽象的子集是不可行的，babble提供了一種通過使用束搜索方法在可擴展性和精度之間進行權衡的方式。

3 在術語上進行庫學習

在本節中，我們對術語語料庫上的庫學習問題進行了形式化，并闡述了我們的第一個核心貢獻：通過反統一生成候選抽象。第4節將這種形式化推廣到e-graph上的庫學習。為了便于解釋，我們首先對庫學習的形式化是一階的，即初始語料庫本身不包含任何-抽象，所有學習到的抽象都是一階函數（babble實現沒有這個限制）。

3.1 預備知識

術語。一個簽名Σ是一組構造器的集合，每個構造器都與一個元數相關聯。T (Σ)表示在Σ上的術語集合，定義為包含所有(1, ... , )的最小集合，其中 ∈ Σ, = arity()，且1, ... , ∈ T (Σ)。我們將形式為()的零元術語縮寫為。術語的大小size()定義為通常的方式（術語中的構造器數量）。我們使用subterms()表示的所有子術語集合（包括本身）。我們假設Σ包含一個專用的多變量元組構造器，寫為?1, ... , ?，我們用它來表示將程序語料庫作為單個術語（??不貢獻術語的大小）。

模式。如果X是一個可枚舉的變量集，T (Σ, X)是模式的集合，即可以包含來自X的變量的術語。如果一個模式的每個變量只出現一次，則稱該模式是線性的：? ∈ vars().occurs(, ) = 1。一個替換 = [1 ?→ 1, ... , ?→ ]是從變量到模式的映射。我們寫()表示將應用于模式，其定義為標準方式。我們定義替換的大小size()為其右側的總大小。

如果存在使得′ = ()，則模式比（或匹配）′更一般，寫為′ ? ；我們將這樣的記為match(′, )。例如， + 1 ? + ，其中match( + 1, + ) = [ ?→ 1]。關系?是模式上的偏序，并且誘導了一個等價關系1 ～ 2 ? 1 ? 2 ∧ 2 ? 1（在變量重命名上等價）。在以下內容中，我們總是根據這個等價關系區分模式。

兩個模式1和2的連接——也稱為它們的反合一器——是匹配兩者的最一般模式；連接在～上是唯一的。注意?T (Σ, X), ?, ?, ? = ?是一個連接半格（Plotkin的子化格[Plotkin 1970]的一部分）。因此，連接可以推廣到任意一組模式。

一個上下文C是一個模式，其中包含一個區分變量?的單一出現。我們寫C []——在上下文C中的——作為[? ?→ ] (C)的語法糖。一個重寫規則是一個模式對，寫為1 ? 2。將重寫規則應用于術語或模式，寫為()，在標準方式中定義：如果 ? 1，則() = (match(, 1)) (2)，否則未定義。模式可以使用規則在一步中重寫為，寫為 →1，如果存在一個上下文C使得 = C [′]并且 = C [(′)]。這個關系的反射-傳遞閉包是重寫關系 →R，其中R是一組重寫規則。

壓縮術語。壓縮術語?T (Σ, X)的形式為：

換句話說，壓縮項可能包含一個帶有零個或多個綁定符號的 λ 抽象應用于相同數量的參數。需要注意的是，這是一種一階語言，因為所有抽象都被完全應用了。重要的是，我們定義了 size，使得 λ 抽象的多次出現只被計算一次。為簡化計算，應用項的大小被定義為，也就是說，抽象節點本身不增加大小。

壓縮項上的 Beta 歸約，記作，以通常的方式定義。

替換在壓縮項上的操作是標準的避免捕獲的 λ 演算替換。需要注意的是，由于我們的語言是一階的，并且沒有內置遞歸，它是強規范化的（該聲明的證明以及本節中省略的其他證明可以在補充材料中找到）。因此，-歸約的順序無關緊要，一般情況下我們可以定義壓縮項的求值按照應用序進行，即首先歸約最里面的-簡約式。結果是，在求值過程中被歸約的任何應用形式都是，也就是說，1 的主體和實際參數2都不包含任何簡約式（因此也不包含任何抽象）。這簡化了我們形式化的幾個方面；例如，由于1中沒有綁定符，因此不會發生變量捕獲，也就不需要重命名。

問題描述。現在我們可以將庫學習問題形式化如下：給定一個項 ∈ T (Σ)，目標是找到最小的壓縮項，它能歸約到（即? → ）。之所以?可能比更小，是因為它可能包含多次相同-抽象的出現（應用于不同的參數），但這些-抽象的大小只計算一次。圖6展示了一個例子。

盡管在一般情況下，解決方案可能包括具有自由變量的嵌套λ（定義在外部λ中），但在本文的其余部分中，我們將注意力限制在全局庫學習上，其中所有的λ都是閉合項。這樣做的動機在于庫學習的目的在于為給定問題域發現可重用的抽象。圖6中的解決方案已經具有這種形式。

3.2 模式驅動的庫學習

在高層次上，我們的庫學習方法是使用原始語料中出現的模式作為壓縮語料中-抽象的候選主體。查看圖6中的示例，乍看之下，單獨使用原始語料中的模式似乎不足夠，因為2的主體包含了1的一個應用。或許令人驚訝的是，這并不是問題：關鍵思想是我們可以通過反轉求值? → 將壓縮成?，并且由于求值順序是應用性的，在每一步中重寫的子項都不會包含任何-簡約式。

壓縮。更正式地說，給定一個模式，我們將其壓縮規則（簡稱為規則）定義為重寫規則。

換句話說，我們首先使用2重寫整個術語，然后使用1在引入的抽象體內進行重寫（注意這種壓縮順序與應用性評估順序相反）。語料庫中的第二個術語類似地進行壓縮；第三個術語使用1在單步中壓縮。盡管從上面的重寫序列中并不明顯，但由于共享了-抽象，如圖6右側所示，得到的壓縮語料庫確實比原始的更小。

3.3 修剪候選模式

在本節中，我們將討論在構建術語重寫問題的-規則集R時，哪些模式可以被丟棄不考慮。

我們可以展示，具有非負成本的模式可以安全地丟棄，即：存在另一種僅使用P \ {}的壓縮，其結果至少一樣小。

平凡模式。基于此分析，任何具有骨架大小skeleton() ≤ 1的線性模式都可以被丟棄，其中skeleton() = size() ? |vars()|是的“骨架”大小，即沒有變量的主體。直觀地說，的骨架太小，無法支付引入應用的費用。在這種情況下，cost(, _) > 0，不管它被使用多少次。我們稱這樣的模式為平凡模式。平凡模式的例子是和 + 。

單一匹配的模式。我們可以展示，在語料庫中只有一個匹配的模式也可以被丟棄。如果在中只有一個匹配，那么它在任何的壓縮中最多只能出現一次。如果是線性的，cost(, _) = 1 + |vars()|，這總是正的，所以可以被丟棄。但是，對于非線性模式，即使只有一個步驟也可以通過變量重用來減小大小，又該怎么辦呢？結果發現，任何只有一個匹配的非線性模式總是可以被一個更優的無變量的零元模式替換。

4圖書館學習模等式理論

4.1 頂層算法

我們可以將等式理論下的庫學習問題 (LLMT) 形式化為：給定一個項 和一組引發等價關系 ≡ 的等式，目標是找到一個壓縮后的項，使得（對于某個 ' ，并且的大小最小。

4.2經由E圖反統一的候選生成

圖 10 定義了這一操作，使用了兩個相互遞歸的函數來反統一 e-類和 e-節點。請注意，e-節點的反統一總是在非空上下文中調用。第一個方程對具有相同構造函數的兩個 e-節點進行反統一：在這種情況下，我們遞歸地反統一它們的子 e-類，并返回結果的笛卡爾積。第二個方程適用于具有不同構造函數的 e-節點：如同項反統一的情況，這將生成一個模式變量。處理 e-圖的一個很好的副作用是我們不需要跟蹤反替換來保證每對子項映射到相同的變量：因為任何重復的項都由相同的 e-類表示，我們可以簡單地使用 e-類 id 和 作為模式變量 , 的名稱。

第二組方程定義了 e-類的反統一（我們暫時忽略 dominant，它將在稍后解釋）。第一個方程適用于 和 已經被訪問的情況：在這種情況下，我們打破循環并返回空集。否則，最后一個方程將反統一兩個 e-類中的所有 e-節點對，并在更新的上下文中合并結果。需要注意的是，除非兩個 e-類中的所有 e-節點都有相同的構造函數，否則這將添加一個模式變量；我們在第 2 節中為了簡化省略了這一細節，但在 babble 中實現了這一功能，并且常常產生更優的模式。例如，考慮圖 4（右）中的 1 和 2 的反統一：雖然它們有相同的構造函數 scale，但 實際上是比 scale 更好的抽象這兩個 e-類的模式，因為與模式 scale 的實際參數（side(6), 1, repRot(side(8), 8, 2/8), 和 2）相比，模式 的實際參數（side(6) 和 scale(repRot(side(8), 8, 2/8), 2)）的總大小是相同的，而模式 本身卻更小。這種情況的發生是因為類 1 表示了多個不同的項，而與 兼容的項在這種情況下比與 scale 兼容的項更小。

5 候選模式選擇通過 E-圖提取

在生成候選抽象之后，LLMT 算法調用 `select_library` 來挑選出能夠最好地壓縮輸入語料庫的候選模式子集。本節描述了我們選擇最佳庫的方法，稱為目標化公共子表達式消除（targeted common subexpression elimination）。

庫選擇作為 E-圖提取

回顧一下，候選選擇從一個 e-圖 G′ 開始，該 e-圖表示使用候選模式 P 壓縮初始語料庫及其等效項的所有方式。我們將子集 L ? P 稱為庫。用 L 壓縮 e-類 的最佳大小可以計算為以下兩個部分的大小之和：(1) 僅使用庫 L 中的庫函數并且不計算 λ-抽象大小的最小項 ∈ J K，以及 (2) 庫 L 中每個 的最小版本。需要注意的是，定義 L 中的抽象的成本只計算一次，并且 L 中的抽象可以用于壓縮 L 中的其他抽象。我們的目標是找到一個 L，使得用 L 壓縮的根 e-類的大小最小。

給定一個特定的庫，我們可以通過相對簡單的自頂向下遍歷 e-圖來找到最小項的大小。因此，一個幼稚的庫選擇方法是枚舉 P 的所有子集，并選擇能夠在根節點處生成最小項的子集。不幸的是，隨著 P 的大小增加，這種方法變得不可行。

利用部分共享結構

相反，`babble` 使用自下而上的動態規劃算法來選擇最佳庫。為此，它將每個 e-節點和 e-類與一個成本集合相關聯，該集合是 (L, ) 的一組對，其中 L 是一個庫，而 是該庫的使用成本，即允許使用 L 時由 e-節點 / e-類 表示的最小項的大小（不包括 L 本身的大小）。成本集合通過圖 11 中所示的規則在 e-圖中向上傳播。基本情況是一個 nullary e-節點 ()，它不能使用任何庫函數，其大小始終為 1。對于具有子節點的 e-節點，`babble` 計算所有子 e-類的成本集合的交叉乘積。最后，對于應用 e-節點，成本集合必須包括庫函數 （除了來自 和 的成本集合的某些庫組合）；需要注意的是，抽象節點的使用成本僅包括 的使用成本，因為抽象體被排除在使用成本之外。

為了計算 e-類的成本集合，`babble` 取所有 e-節點成本集合的并集。然而，這樣做會導致成本集合的大小指數級增長。為了解決這個問題，我們定義了一個部分排序化簡（reduce），它只剪枝那些明顯次優的成本集合。給定 e-類成本集合中的兩個對 (L1, 1) 和 (L2, 2)，如果 L1 ? L2 并且 1 ≤ 2，那么 L2 就被 L1 包含，可以從成本集合中移除，因為 L1 即使在更少的庫函數下也可以更好地壓縮這個 e-類。實際上，這種優化剪枝了具有冗余抽象的庫，即兩種不同的抽象可以用來壓縮相同的子項。

Beam Approximation（光束近似）

即使有了部分排序化簡，為每個 e-節點和 e-類計算成本集合仍可能指數級增長。為此，`babble` 提供了限制每個成本集合中庫的大小和每個 e-類存儲的成本集合大小的選項。這會產生一種光束搜索風格的算法，其中每個 e-類的成本集合都會被剪枝，如圖 11 所示。這個剪枝操作首先過濾掉具有超過 個模式的庫，然后按總成本（即使用成本和庫的大小之和）對剩余的庫進行排名，最后返回這個集合中的前 個庫。

6 評估

我們通過兩個定量研究問題和一個定性問題來評估 `babble` 及其背后的 LLMT 算法：

**RQ 1.** `babble` 是否能比最先進的庫學習工具更好地壓縮程序？

**RQ 2.** LLMT 中的主要技術（反統一和等式理論）對算法的性能是否重要？

**RQ 3.** `babble` 學到的函數是否具有直觀意義？

基準選擇

我們使用了兩套基準來評估 `babble`，如表 1 所示。第一套基準源自 DreamCoder 研究 [Ellis et al. 2021]，并作為公共倉庫提供 [Bowers 2022]。DreamCoder 是當前最先進的庫學習工具，使用這些基準允許我們進行面對面的比較。DreamCoder 的基準被分為五個領域（每個領域有不同的 DSL）；我們選擇了其中兩個領域——List 和 Physics——因為我們對它們的理解最為深入，適合添加等式理論。

第二套基準，稱為 2d cad，來自 Wong et al. [2022]。這項工作收集了一個大型圖形 DSL 程序庫，目的是研究生成的對象與其自然語言描述之間的關系。這個數據集的“Drawings”部分包含 1,000 個程序，分為四個子領域（見表 1），每個子領域有 250 個程序。

我們在 AMD EPYC 7702P 處理器（2.0 GHz）上運行了所有基準。每個基準都在單核上運行。DreamCoder 的結果來自基準倉庫 [Bowers 2022]；DreamCoder 在 AMD EPYC 7302 處理器（3.0 GHz）的 8 核上運行。

6.1 與 DreamCoder 的比較

為了解答 RQ 1，我們將 `babble` 與最先進的 DreamCoder 工具 [Ellis et al. 2021] 進行比較，使用的是其自己的基準。DreamCoder 的基準適用于它的工作流程；雖然庫學習任務的輸入在概念上是一組程序（或僅一個大程序），每個輸入到 DreamCoder 的都是一組程序的集合。每組是從同一個程序合成任務（DreamCoder 管道的早期部分）輸出的程序集合。在通過庫學習壓縮程序時，DreamCoder 是通過連接每組中最壓縮的程序來最小化程序的成本，換句話說：

DreamCoder 采用這種方法來為其庫學習組件提供許多相同程序的變體，以便在不同合成問題的解決方案程序之間引入更多的共享結構。

為了在 `babble` 中實現 DreamCoder 的基準，我們使用 e-圖來捕捉一個組中的程序變體的概念。由于組中的每個程序都是相同合成任務的輸出，`babble` 將它們視為等效，并將它們放在同一個 e-類中。

**結果。** 我們在 DreamCoder 基準套件中的五個領域上運行了 `babble`。結果如圖 12 所示。總結來說，`babble` 在來自 DreamCoder 領域的基準測試中，始終能實現比 DreamCoder 更好的壓縮比，而且速度比 DreamCoder 快 1-2 個數量級。

**等式理論的作用。** 為了回答 RQ 2，我們再次使用 DreamCoder 基準，重點關注我們為 `babble` 提供等式理論的領域：List 和 Physics。在這些領域，我們用兩種額外的配置運行了 `babble`：

- “BabbleSyn” 忽略等式理論，僅進行語法庫學習。

- “EqSat” 僅使用等式飽和（Equality Saturation）和等式理論中的重寫來優化程序。該配置不進行任何庫學習。

圖 12a 和 12b 顯示了這些額外配置的結果，以及 DreamCoder 和正常的 `babble` 配置。所有 `babble` 配置都依賴于目標化子表達式消除來選擇最終學習的庫。顯然，“EqSat” 配置非常快速，但壓縮效果相對較少，因為它不學習任何庫抽象。“BabbleSyn” 配置確實能壓縮輸入，實際上在兩個領域中仍優于 DreamCoder。然而，加入等式理論（圖中的“babble”標記）顯著改善了壓縮效果，并且增加的運行時間相對較少，仍在一個數量級之內。

6.2 大規模 2d cad 基準測試

上一節展示了 `babble` 的性能遠超現有技術。在本節中，我們展示和討論了在 2d cad 領域基準測試中運行 `babble` 的結果。這些基準測試來自 Wong et al. [2022]，比 DreamCoder 數據集中的基準測試大得多（大約 10 倍到 100 倍），DreamCoder 無法處理這些數據集。

**定量結果。** 表 2 和圖 13 顯示了在 2d cad 領域基準測試上運行 `babble` 的結果。圖 13 中的圖表清楚地顯示了兩個觀察結果。首先，與 RQ 2 相關的是，添加等式理論改善了所有四個基準（實心標記總是位于空心標記的右側）。其次，或許令人驚訝的是，等式理論有時可以使 `babble` 更快！這與之前關于等式飽和 [Willsey et al. 2021] 的觀察一致：雖然等式飽和通常使 e-圖變大，但有時可以將兩個相關的 e-類合并為一個，從而減少對 e-圖執行某些操作時的工作量。

我們還觀察到 Nuts-and-bolts 數據集中包含多個冗余轉換，例如第 2 節運行示例中出現的“按 1 縮放”。這些冗余在缺少等式理論時可以幫助找到抽象。然而，它們不應該是 `babble` 所必需的，因為 LLMT 可以在需要時引入這些冗余。因此，我們從 Nuts-and-bolts 數據集中移除了所有現有的冗余轉換，并在轉換后的數據集上運行了 `babble`。結果見表 2 的最后一行。在修改后的數據集上，`babble` 使用等式理論時實現了相同的壓縮效果，但在沒有等式的情況下，表現比未修改的數據集差。

**定性評估。** 圖 14 突出了 `babble` 從 2d cad 基準測試中發現的一些抽象。我們在每個基準測試上運行了 `babble` 并應用了學到的抽象來可視化它們的使用。有關學習的庫的可用性和可讀性的問題難以回答，我們將這留待未來的工作。然而，圖 14 顯示 `babble` 確實識別出了在不同基準中相似的公共結構，這使得其輸出更易于重用和解釋。

首先，我們回顧第 1 節的 Nuts-and-bolts 示例：圖 14 顯示 `babble` 學到了縮放多邊形（ngon）抽象，這適用于數據集中的多個程序。我們還看到 `babble` 一貫地為 Nuts-and-bolts 和 Vehicles 發現了類似的“形狀環”抽象。最后，正如 Gadgets 示例所示，`babble` 為整個模型及其組件都找到了抽象。在這種情況下，它學習了抽象整個外形的函數 `gadget_body`，同時也學習了抽象外形把手的 `dial` 函數。

7 相關工作

`babble` 的靈感來源于庫學習的研究，特別是 DreamCoder 相關的工作，以及基于等式飽和的程序合成和反編譯。

**DreamCoder**。DreamCoder [Ellis et al. 2021] 是一個程序合成器，通過從一組相關合成任務的解決方案中學習一個抽象庫來進行工作。這個庫旨在用于解決其他類似的合成任務。DreamCoder 使用版本空間 [Lau et al. 2001; Mitchell 1977] 來緊湊地存儲大量程序，并利用 e-圖中的思想（如 e-匹配），但僅用于探索原始程序的重構空間，使用候選庫進行探索，而不是使庫學習對語法變化具有魯棒性。我們的評估顯示，`babble` 能夠比 DreamCoder 更快地找到更優的抽象。

DreamCoder 激發了若干跟進工作，試圖提高其庫學習過程的效率和所學抽象的質量。其中之一是 Wong et al. [2021] 的工作，他們使用自然語言注釋和神經網絡來引導庫學習。另一個是 Stitch [Bowers et al. 2023]，它與本工作同時開發，是與 `babble` 最相關的工作；我們在下面詳細討論 Stitch。

**Stitch**。兩種方法的核心區別在于，Stitch 側重于提高純語法庫學習的效率，而 `babble` 通過添加等式理論來提高其表達能力。雖然 `babble` 將庫學習分為兩個階段——通過反統一進行候選生成和通過 e-圖提取進行候選選擇——Stitch 算法則在分支限界的自頂向下搜索中交替進行生成和選擇階段。從“頂層”模式 \(X\) 開始，Stitch 逐步對其進行細化，直到進一步細化不再有收益。為了快速剪枝次優的候選模式，Stitch 通過將該模式在語料庫中每次匹配的壓縮量相加來計算其壓縮的上界（由于未考慮匹配可能重疊，因此該上界是不精確的）。對于沒有通過這種方式剪枝的候選模式，Stitch 通過搜索重寫的最佳匹配子集來計算其真實的壓縮量，這被稱為“重寫策略”。`babble` 的提取算法可以視為 Stitch 的重寫策略的一種泛化：前者在同時搜索模式的子集以及如何將其應用于語料庫時，后者則一次只考慮單個模式，并且只搜索最佳的應用方式。由于前者的搜索空間要大得多，`babble` 使用了束搜索近似，而 Stitch 的重寫策略是精確的。總結而言，兩種方法的主要優缺點如下：

- `babble` 能夠在考慮等式理論的情況下學習庫，而 Stitch 不能；

- Stitch 為一次學習一個最佳抽象提供了最優性保證，而 `babble` 可以同時學習多個抽象，但犧牲了理論上的最優性。

**其他庫學習技術**。Knorf [Dumancic et al. 2021] 是一個用于邏輯程序的庫學習工具，它與 `babble` 類似，也分為兩個階段。他們的候選生成階段類似于 Stitch 中的上界計算，而選擇階段則使用現成的約束求解器。探索他們的基于約束的技術是否可以推廣到邏輯程序之外將是很有趣的。

其他相關工作

一些研究發展了有限形式的庫學習，其中只能抽象出某些特定類型的子術語。例如，ShapeMod [Jones et al. 2021] 為 DSL 語言 ShapeAssembly 中表示的 3D 形狀學習宏，僅支持對數值參數（如形狀的尺寸）進行抽象。我們之前的工作 [Wang et al. 2021] 從圖形程序中提取共通結構，但僅支持對原始形狀進行抽象，并在程序的頂層應用這些抽象。這些限制使得庫學習問題在計算上更具可處理性，但也限制了所學抽象的表達能力。

有幾種神經程序合成工具 [Dechter et al. 2013; Iyer et al. 2019; Lázaro-Gredilla et al. 2018; Shin et al. 2019] 使用統計技術學習編程慣用法。其中一些工具使用了“探索-壓縮”算法 [Dechter et al. 2013]，通過迭代枚舉一組程序并找到一種解決方案，從而揭示使得這些程序集最大程度壓縮的抽象。這與 `babble` 用于指導提取的公共子表達式消除方法類似。

**循環重滾**。循環重滾與庫學習相關，因為它也旨在發現程序中的隱藏結構，不過這種結構以循環的形式存在。各種領域已經使用循環重滾從平坦輸入程序中推斷抽象。在硬件領域，循環重滾用于優化程序的代碼大小 [Rocha et al. 2022; Stiff and Vahid 2005; Su et al. 1984]。在許多這些工具中，編譯器首先展開循環，應用優化，然后重新滾動它——編譯器因此擁有有關循環的結構信息，可以用于重滾 [Rocha et al. 2022]。圖形領域則使用循環重滾從低級表示中發現潛在結構。CSGNet [Sharma et al. 2017] 和 Shape2Prog [Tian et al. 2019] 使用神經程序生成器從像素和體素基礎的輸入表示中發現 for 循環。[Ellis et al. 2017] 使用程序合成和機器學習從手繪圖像中推斷循環。Szalinski [Nandi et al. 2020] 使用等式飽和技術從通過網格解構工具合成的平坦 3D CAD 程序中自動學習循環，形式為映射和折疊 [Nandi et al. 2018]。WebRobot [Dong et al. 2022] 使用猜測重寫技術從 web 交互的跟蹤中推斷循環。與 `babble` 類似（且不同于 Szalinski），WebRobot 可以在多個輸入跟蹤上發現抽象。

**反統一的應用**。反統一是發現程序中共同結構的一個成熟技術。它是自底向上的歸納邏輯編程 [Cropper and Dumancic 2022] 的核心思想，也被用于軟件克隆檢測 [Bulychev et al. 2010]、示例編程 [Raza et al. 2014] 和學習重復代碼編輯 [Meng et al. 2013; Rolim et al. 2017]。這些應用可能也會受益于 `babble` 的反統一概念，特別是在處理語義保持變換時更具魯棒性。

**使用 e-圖進行合成和優化**。雖然傳統上 e-圖在 SMT 求解器中用于促進不同理論之間的通信，但一些工具已展示其在優化和合成中的應用。Tate et al. [2009] 首次使用 e-圖進行等式飽和：一種通過重寫優化具有循環的 Java 程序的技術。此后，多個工具使用等式飽和來尋找與輸入程序等效但更優的程序 [Nandi et al. 2020; Panchekha et al. 2015; VanHattum et al. 2021; Wang et al. 2020; Willsey et al. 2021; Wu et al. 2019; Yang et al. 2021]。`babble` 使用了針對 e-圖的反統一算法（結合領域特定的重寫），這是之前工作中沒有展示的。此外，之前的工作要么使用貪婪的提取策略，要么使用 ILP 基礎的提取策略，而 `babble` 使用了一種新的目標公共子表達式消除方法，我們認為它可以用于許多其他等式飽和的應用，特別是考慮到它可以通過束搜索進行近似。

8 結論與未來工作

我們介紹了基于理論的庫學習（LLMT）技術，該技術用于從一組程序中學習抽象，同時結合用戶提供的等式理論。我們在 babble 中實現了 LLMT。我們的評估顯示，babble 在壓縮效果上比現有技術快幾個數量級。在較大的 2d cad 程序基準套件上，babble 學習到了合理的函數，這些函數能壓縮一個以前過大而無法使用庫學習技術的數據集。

LLMT 和 babble 提出了許多未來工作的方向。首先，我們的評估表明，等式理論對于實現高壓縮率至關重要，但這些理論必須由領域專家提供。近期的自動化理論合成工作，如 Ruler [Nandi et al. 2021] 或 TheSy [Singher and Itzhaky 2021]，可能會幫助用戶完成這一任務。其次，LLMT 使用 e-圖反統一來生成有前景的抽象候選，但這種方法并不完整，可能遺漏了一些能夠實現更好壓縮的模式。未來一個令人興奮的方向是將 LLMT 與更高效的自頂向下搜索方法結合起來，如 Stitch [Bowers et al. 2023]。這具有挑戰性，因為 Stitch 依賴于快速計算給定模式壓縮的上界，通過求和每個匹配中的局部壓縮來實現。這種上界并不容易直接擴展到 e-圖，因為在 e-圖中，同一模式的不同匹配可能來自于語法變體的不同，且需要在抽象帶來的壓縮和不同語法變體之間的大小差異之間進行權衡。