技術日新月異的當下，人工智能編程日益成熟，它的發展能有助于人類制造更多智能機器嗎？

程序合成是指基于規范自動生成程序的概念。它不同于程序驗證。程序驗證依賴于正式的證明來證實程序按照正式的規范運行。

1957年，在康奈爾大學符號邏輯協會舉行夏季會議期間，阿隆佐·邱奇試圖基于數學要求合成程序。20世紀60年代，人工智能相關研究人員詳細闡述了程序合成的概念，并將其應用于典型的人工智能研究。

近年來，深度學習已經改變了人工智能完成任務的方式。這種進步促使研究人員嘗試教授人工智能人類擅長的工作。其中一個重要領域就是創建元學習系統，讓人工智能學習人類擅長的各種工作。神經程序合成和機器人技術的相關研究初步展現了利用程序合成來教授機器人精準執行任務的能力。

程序合成最常用于使計算機編程更容易實現。諸如AutoProf、FlashFill、Storyboard編程工具等應用程序允許學生通過直接操作某些概念以更直觀的方式編寫程序，而無需編寫代碼。

在人工智能研究人員弗朗索瓦·喬萊的論文《智力測試》中，他將程序合成作為一種用于解決智力測試問題后建模的ARC任務的技術。

在接受Verge網站關于其論文的采訪時，喬萊說：“關鍵點是，在任何任務中，獲得高技能都不是智力的表現。除非這個任務是一個元任務，涉及到從大量此前未知的問題上獲得新的技能。這正是我所認為的智力基準。”

從本質上講，系統智力應通過以下方式測試， 正如喬萊所說“這意味著只使用系統之前不知道的新任務，測量系統開始時對該任務之前的知識，以及測量系統的采樣效率（即學習完成該任務需要多少數據）。達到某一技能水平所需的信息（先前的知識和經驗）越少，就說明越智能。如今的人工智能系統一點也不智能。”

他后來將ARC任務作為問題發布，來解決Kaggle的抽象和推理問題挑戰。解決這一問題將涉及到利用編程綜合的力量來學習以前未知的ARC任務。

分解編程合成問題

對于每一個看似不可能解決的問題，可以先把問題分解成小問題。如果您從未學習過編程合成，那么就在開始工作前了解一下存在什么問題以及怎么解決。

1.程序空間問題

每個編程合成問題最終都要在整個程序空間中進行搜索。搜索方法必須是有效的。想象一下，若使用樹算法，就必須有辦法砍下這棵樹的枝干，否則，在它生長的過程中，它有無限生長的潛力。

2. 用戶意向問題

在測試用戶意圖的邏輯之間常常存在模糊領域。當用戶與環境交互時人們有了一方面的發現，在用戶參與時，新的數據可能會將問題轉化為用戶眼中的全新問題。

若要成功解決Kaggle挑戰必然涉及解決這兩個問題。

用于程序合成的實用工具

在Python中，Z3是用于程序合成的Python包。這里是阿德里安·桑普森為Z3提供的優秀教程。

其文章中的例子如下：

構建泛型求解器，如下所示：

代碼源于阿德里安·桑普森博客

然后，定義要運行的公式。

代碼源于阿德里安·桑普森博客

運行：print（solve（formula）） 來解決任何問題。您可以閱讀他的教程了解更多細節和例子。

責任編輯：ct