Program Synthesis in AI

Can AI-Driven Programming help us create more intelligent machines?

Program synthesis is the idea of automatically generating programs from specifications. It is different than program verification. Program verification relies on formal proofs to demonstrate that programs behave according to formal specifications.

In 1957, Alonzo Church , during the Summer Institute of Symbolic Logic at Cornell University tried to synthesize circuits from mathematical requirements. Eventually, researchers of AI in the 1960s elaborated on the concept of program synthesis to apply it to symbolic AI research.

In recent years, deep learning has changed the way AI accomplishes tasks. The advancement has propelled researchers to try to teach AI tasks that humans are good at. One of the big areas is creating meta-learning systems that teach AI to learn various tasks. Research in Neural Program Synthesis and robotics allow the early glimpses of the power of using program synthesis to teach robotics to perform tasks with precision.

The biggest applications where programming synthesis is used is still making computer programming more accessible. Applications such as AutoProf, FlashFill, Storyboard Programming Tool that allow students to write programs in more intuitive ways by manipulating certain concepts directly.

In AI researcher Francois Chollet’s paper On the Measure of Intelligence , he referenced program synthesis as the technique to use to solve ARC tasks.

In his interview with Verge about his paper, Chollet said, “The key insight is that there is no task where achieving high skill is a sign of intelligence. Unless the task is a meta-task, that involves acquiring new skills over a broad [range] of previously unknown problems. And that’s exactly what I propose as a benchmark of intelligence.”

In essence, the intelligence of the system should be measured by the following, Chollet said, “This means only using new tasks that are not known to the system beforehand, measuring the prior knowledge about the task that the system starts with, and measuring the sample-efficiency of the system (which is how much data is needed to learn to do the task). The less information (prior knowledge and experience) you require to reach a given level of skill, the more intelligent you are. And today’s AI systems are not very intelligent at all.”

In essence, the problem for the Abstraction and Reasoning Challenge on Kaggle involves harnessing the power of programming synthesis to learn ARC tasks that are previously unknown.

Breaking Down the Programming Synthesis Problem

For every impossible problem, it involves breaking down the challenges into little bite-sized pieces. If you’ve never studied programming synthesis, then understanding what the challenges are and what you can do solve them will allow you to start the work.

1. The Program Space Problem

Each programming synthesis problem will eventually search over the entire program space. The search methods must be efficient. Imagine if you use a tree-based algorithm. You must have a way to cut down the limbs of the tree, otherwise, as it searches, it has the potential to grow infinitely.

2. The User Intent Problem

There’s often ambiguity in between logic that tests the user’s intent. There’s an aspect of discovery when users interact with the environment. Upon engagement, new data may transform the problem into an entirely new one in the user’s eyes.

Practical Tools to Use for Program Synthesis

In Python, Z3 is the python package to use to program synthesis. Here’s a great tutorial for Z3 from Adrian Sampson.

Examples from his article can be seen here:

You construct a generate generic solver such as the below.

Then, you define your formula that you want to run.

You run: print(solve(formula)) to solve any problem. You can read his tutorials for many more details and examples.

Want to Learn More About Program Synthesis?

Here are a few learning resources for program synthesis.