陶哲軒上手Copilot：不可思議，它能從定理名字猜出我想要的方向

嚐鮮 GPT-4 之後，陶哲軒又用上了 Github Copilot。

這次，他的試用場景是學習 Lean 語言並利用其形式化數學定理。

對大模型來說，形式化的定理證明也算是一種挑戰。形式化證明本質上是一種電腦程序，但與 C 或 Python 中的傳統程序不同，證明的正確性可以用證明助手（例如 Lean 語言）來驗證。定理證明是代碼產生的一種特殊形式，在評估上非常嚴格，沒有讓模型產生幻覺的空間。

而陶哲軒提到的定理，來自10 月9 日的一篇論文：

論文中的這個證明只有不到一頁，但陶哲軒的形式化證明使用了200 行Lean 語言。

舉例來說，在論文中，陶哲軒只是斷言對於任意a>0 的情況，在實數上是凸的，因為這是一個常規的微積分練習，然後調用了Jensen 不等式，但寫出所有細節用了大約50 行程式碼。

陶哲軒表示，Github copilot 能夠正確預測各種例行驗證的多行程式碼，並從定理的名字等線索中推斷出他想要的方向，這種能力是「不可思議的」。

Lean 的「重寫」策略是不可或缺的，它可以透過有針對性的替換來修改冗長的假設或目標，無需完整地鍵入表達式就能對其進行操作。

「在用LaTeX 撰寫證明時，我經常粗略地模擬這種方法，將我要處理的冗長表達式從一行剪切粘貼到下一行，然後進行有針對性的編輯，但這有時會導致錯字在文件中多行傳播，因此能以自動和可驗證的方式進行重寫是件好事。」

論文中也提到一個不等式，即對於任意的k, l, n，滿足，則

陶哲軒表示下一個目標就是建立該不等式的簡單版本，即論文中的不等式(1.8)：

這部分的證明主要還是利用微積分的知識，但有一個困難是需要使用漸近符號。陶哲軒表示後續的論證雖然會很耗時，但並不是特別困難。

但目前的工具仍有一些局限性，例如，重寫涉及綁定變數（如數列中的求和變數）的表達式並不總是很容易完成。他期待著有一天，人們可以簡單地要求自然語言LLM 進行此類轉換……

^{參考連結：https://mathstodon. xyz/@tao/111271244206606941}

#

以上是陶哲軒上手Copilot：不可思議，它能從定理名字猜出我想要的方向的詳細內容。更多資訊請關注PHP中文網其他相關文章！