Filetype PDF | Posted on 25 Jan 2023 | 2 years ago
Authentication
digital resources
139x Filetype PDF File size 0.52 MB Source: www.csl.sri.com
Synthesizing Geometry Constructions
Sumit Gulwani Vijay Anand Korthikanti∗ Ashish Tiwari†
Microsoft Research UIUC SRIInternational
Redmond,WA,USA Urbana Champaign, IL, USA MenloPark, CA, USA
sumitg@microsoft.com vkortho2@uiuc.edu tiwari@csl.sri.com
Abstract Concurrent algorithms [34, 39], parameters of embedded sys-
In this paper, we study the problem of automatically solving tems [6, 37].
ruler/compass based geometry construction problems. We first in- • GeneralpurposeprogrammingassistanceforSoftwareDevelop-
troduce a logic and a programming language for describing such ers: Partial programming [4, 23, 33], Template based program-
constructionsandthenphrasetheautomationproblemasaprogram ming[35,36],Automateddebugging[40],Programunderstand-
synthesis problem. Wethendescribeanewprogramsynthesistech- ing [18].
niquebasedonthreekeyinsights:(i)reductionofsymbolicreason- • Automating repetitive tasks for End-users: Programming by
ingtoconcretereasoning(basedonadeeptheoreticalresultthatre- Demonstration systems [9, 26], Programming by Example sys-
duces verification to random testing), (ii) extending the instruction tems [13, 15], shell scripts [25].
set of the programming language with higher level primitives (rep- However,wefeelthatthemostrevolutionaryapplicationofpro-
resenting basic constructions found in textbook chapters, inspired gramsynthesis technology can be in K-12 education. The potential
by how humans use their experience and knowledge gained from impact size of target population is simply mind boggling: billion
chapters to perform complicated constructions), and (iii) pruning students and teachers (compared to say ten thousand algorithmic
the forward exhaustive search using a goal-directed heuristic (sim- designers, million software developers, and hundred million end-
ulating backward reasoning performed by humans). Our tool can users).
successfully synthesize constructions for various geometry prob- Program synthesis technology can be applied to automating
lems picked up from high-school textbooks and examination pa- constructions for various domains in high-school curriculum. Ex-
pers in a reasonable amount of time. This opens up an amazing amples of such constructions include (i) ruler/compass based geo-
set of possibilities in the context of making classroom teaching metric constructions in mathematics (ii) constructions of chemical
interactive. compoundsorbiologicalproteinsusing(bio)chemicalreactionsun-
Categories and Subject Descriptors D.1.2 [Programming Tech- der appropriate conditions governed by catalysts, temperature and
niques]: Automatic Programming; I.2.2 [Artificial Intelligence]: pressure in chemistry and biology, (iii) constructions of electrical
ProgramSynthesis; K.3.1 [Computers and Education]: Computer circuits using series and parallel composition of resistances and ca-
uses in Education pacitances in physics, and so on.
One might wonder what is the connection between program
General Terms Algorithms, Theory synthesis and automating constructions. Programming languages
Keywords Program synthesis, Ruler-Compass geometry con- allowustoformallydescribetheseconstructions.Taketheexample
structions, Abstraction, Forward and Backward Analysis of geometric constructions that involve constructing a set of objects
Owith desired properties φ from an initial set of objects I with
2
certain properties φ using a series of steps S, where each step
1. Introduction 1
involves using ruler or compass to create new objects. The objects
Program Synthesis is the task of automatically synthesizing a pro- I and O are like program variables and S is the program whose
1
instructionsetincludesruler/compassoperations. Theformulasφ
graminsomeunderlyinglanguagefromagivenspecificationusing 1
andφ playtheroleofpreconditionandpostconditionrespectively.
some search technique [12]. It has been used for a wide variety of 2
applications targeted towards various classes of users. Checking the correctness of a given geometric construction is like
checking the validity of the Hoare triple hφ ,S,φ i, which is a
• Discovery of new algorithms for Algorithm Designers: Bit- 1 2
vector algorithms [14], Mutual exclusion algorithms [3, 21], programverification problem. In fact, this verification problem has
been studied intensively in the context of geometric constructions.
Synthesizing the geometric construction S, given φ and φ , is the
∗Workdonewhilevisiting SRI International. 1 2
†Research supported in part by NSF grants CSR-EHCS-0834810, CSR- programsynthesis problem, which is what we address in this paper
0917398andSHF:CSR-1017483. in the context of geometric constructions.
We focus on automating geometry constructions because ge-
ometry is regarded to be one of the most difficult as well as im-
portant subjects in high-school curriculum. Geometry education is
supposed to help exercise logical abilities of the left-brain, visu-
Permission to make digital or hard copies of all or part of this work for personal or alization abilities of the right-brain, and hence enables students to
classroom use is granted without fee provided that copies are not made or distributed make the two connect and work together as one. Geometric con-
for profit or commercial advantage and that copies bear this notice and the full citation
on the first page. To copy otherwise, to republish, to post on servers or to redistribute
to lists, requires prior specific permission and/or a fee. 1In fact, a programming language for drawing such geometric objects is
PLDI’11, June 4–8, 2011, San Jose, California, USA. used to motivate freshman and non-major students to take up programming
c
Copyright
2011 ACM978-1-4503-0663-8/11/06...$10.00 lang. course at UCSD [29].
structions have a close connection to axiomatic logic. The skills doing such constructions. This can also be thought of as pruning
needed to figure out how to construct, say, a square without a pro- the forward search by integrating it with backward search.
tractor, are closely related to the thinking skills needed to prove Based on these ideas, we built a tool for automating geometry
theorems about squares [1]. The visual nature of geometry makes constructions. Our tool could solve most standard geometry con-
it initially more accessible than other parts of mathematics, such struction problems in less than a second. Surprisingly, it could also
as algebra or number theory. “Construction can reinforce proof and solve some nontrivial problems whose solution is not immediately
lend visual clarity to many geometric relationships.” [30] “They clear, such as, constructing a square whose (extended) sides pass
give the secondary school student, starved for a Piagetian concrete- through four given points. While our focus is on synthesizing ge-
operational experience, something tangible.” [28]. ometry constructions, the basic concepts used here could be appli-
One might also wonder why we insist on high-school curricu- 2
cable in other domains as well.
lum as opposed to undergraduate/graduate curriculum for our suc- Another interesting application of our algorithm is in the con-
cess metric. We want to build tools that are scalable, predictive in text of dynamic geometry, or creating animations. Suppose we can
their power and can have a real practical impact. Given scalabil- findamodelfordeclarativeconstraintsusingnumericalmethodsin
ity limitations of program synthesis techniques in terms of being 1 second, and it takes 5 seconds to synthesize an equivalent con-
able to automatically synthesize only relatively small snippets of struction for the declarative problem specification. The importance
code in a reasonable amount of time, high-school problem solving of having the construction (besides education purposes) is that run-
(wheresolutionsizeisrelativelysmallenoughandarelessinvolved ning that construction will take micro-seconds. So, if the goal is
compared to undergraduate/graduate problems) is an excellent fit. to quickly re-compute coordinates of various points after assigning
Wepresent a new program synthesis technique for automating a new value to the free variables, running the construction will be
geometry constructions. Our program synthesis technique is based faster by orders of magnitude compared to using numerical meth-
on exhaustive search, but exploits three key ideas, inspired by ods.
humanexperience and intelligence, to make it scalable. This paper makes the following key contributions.
Idea 1: Reducing symbolic reasoning to concrete First, we re- • Usingthespecificexampleofgeometryconstructions,thepaper
duce the problem of symbolic reasoning to concrete reasoning. We points out the role that programming languages, logic, and
reduce the problem of “obtaining a construction that can transform program synthesis can play in the area of building automated
input objects I with precondition φ to output objects O with post- tutoring systems, which is traditionally considered to be a sub-
1
condition φ ” to that of “obtaining a construction that can perform field of AI.
2
the transformation on a randomly chosen concrete model for I and • We present a novel search algorithm that combines three key
Othat satisfies constraints φ and φ ”. In our implementation, we
1 2 ideas picked up from different research areas: property testing
generate such a random model using a numerical (multivariate) (theoretical computer science), higher-level abstractions (pro-
function minimization procedure. The probabilistic soundness of gramming languages), and goal-directed reasoning (AI). We
this reduction relies on a deep theoretical result that is an exten- believe that the principles underlying our search algorithm are
sion of randomized polynomial identity testing theorem. (This re- general enough to be applicable to other automated problem
sult is analogous to reducing verification of a straight-line program solving domains, and other program synthesis applications.
to testing on a random input.) This reduction is critically important
because symbolic reasoning would not scale - it would make our • We report on a successful experimental prototype thereby es-
technique multiple orders of magnitude slower, and hence useless tablishing the feasibility of building automated tutoring sys-
in an interactive setting. This reduction is inspired by how humans temsaroundtheimportanthigh-schoolsubjectofruler-compass
also work out geometric constructions by visually working out the based geometry constructions.
construction on a randomly chosen configuration.
Idea 2: Using extended set of common constructions Whenhu- 2. OverviewofourApproach
mans typically solve a construction problem, they don’t attempt to Consider the problem: Construct a triangle, given its base, a base
construct everything from first principles. They think in terms of angle and sum of the other two sides. We wish to synthesize a
somekeyhigherlevelabstractions, where they exploit their knowl- program S that performs the above construction using ruler and
edge of how to perform some key multi-step constructions. Our compass instructions. Before we can discover S, we first need to
technique, which is based on exhaustive search, exploits this obser- ~ ~
formally state its inputs I, output O, its precondition φ and its
vation by working with an extended set of common constructions pre
postcondition φ .
found in textbook chapters (Table 2) as opposed to simply working post
~
with a basic minimal set of constructions (Table 1). This can also Theinputs I consist of a line segment (points p1, p2, and a line
be thought of as giving preference to certain combinations of basic L = Line(p1,p2)) that defines the base of the desired triangle, a
3 ~
construction steps, which is related to the notion of using priors in length r and an angle a. The desired output O consists of a single
the machine learning community. This allows for transforming the point p.
Theprecondition φ arises from the triangle inequality as
search process with small width and large depth to one with large pre
width and small depth. r > Length(p ,p ) (1)
1 2
Idea 3: Performing goal-directed search Weprune our forward 2Theideaofrepresentingknowledgeasalibraryandthenconstructingnew
exhaustivesearchbyapplyingaconstruction(fromtheextendedset structures by composing elements of the library can be viewed as one way
of constructions) only when the goodness measure function sug- of interpreting (Turing award winner) Ed Feigenbaum’s recent remarks in
gests that it may be useful to apply that construction. For example, an interview in ACM Communications, where he calls out for having a
the goodness measure function might suggest that if a construction way for computer to read books and learn to solve problems after that, as
results in a line L that passes through a given output point P, then
1 opposed to building domain specific tools [32].
it may be useful to apply that construction (since we might be able 3In our formalization of geometry constructions, we distinguish between
to construct another line L in the future that also passes through
2 the cases when we have just two points on a plane versus when we also
P,andhenceintersection of L and L can yield desired point P).
1 2 have the line segment connecting those two points explicitly drawn on the
This is inspired by backward reasoning performed by humans in plane.
Thepostcondition φ can be stated as, using goodness, the search for S fails to terminate in allocated
post time. Fig. 1(right) shows the points constructed during a truncated
Angle(p,p1,p2) = a ∧ Length(p,p1)+Length(p,p2) = r (2) search.
~ ~ The above program was synthesized in 3.5 seconds. When
After we have a formal description of the inputs I, outputs O, rewritten in terms of the basic library, the above program expands
precondition φ and postcondition φ , we next find a (ran-
pre post to a program with 17 instructions. We remark that our implementa-
dom)concrete input-output pair that is consistent with the pre/post tion distinguishes between lines and rays, but we do not show this
specification (Idea 1). In other words, we need to find coordinates distinction here for simplicity.
of the input points p ,p , the distance r, the angle a, and the coor-
1 2
dinates of the output point p such that the conditions in Equation 1
and Equation 2 are satisfied. These conditions are (multivariate) 3. GeometryProgrammingLanguage
nonlinear constraints over the reals. We translate these nonlinear Wedescribe a programming language for geometric constructions.
constraints into a multivariate nonlinear optimization problem (as We will later synthesize programs in this programming language
described in Section 6.2) and then use a (numerical) multivariate starting from a given specification.
nonlinear optimization routine to find a concrete input-output pair. Traditional (imperative) programming languages manipulate
Duringthisprocess,weensurethattheconcreteinput-outputpairis values of variables. These values are typically integers, floats,
picked sufficiently randomly. Let us say that we find the following Booleans, or addresses (pointers). The entities that our program-
concrete input-output pair: ming language for geometry manipulates are objects, such as
L = Line(h81.62,99.62i,h99.62,83.62i) points, lines and circles. Specifically, our programming language
r = 88.07 a = 0.81radians for geometry has the following set of object types:
p = h131.72,103.59i Point. A point is a primitive object in our language. It is repre-
~ ~ sented using Cartesian coordinates. In this paper, we restrict
Let (I ,O ) denote these concrete input-output objects. (Here all
c c ourselves to 2-dimensional geometry and a point is represented
numerals are truncated to 2 digits after decimal, but the implemen- using its x- and y-coordinates that remain hidden.
tation uses a much higher precision). Line. A line is represented by a pair of two distinct points that lie
~ ~
Now we have a concrete input-output pair, (I ,O ), for the
c c on it. The constructor Line(p ,p ) returns a line object that is
problem. The geometry synthesis problem is also given an exe- 1 2
defined by the points p and p .
cutable library of functions that should be used to synthesize S. 1 2
For example, assume we have a library that implements the “ruler- Angle. An angle is a number in the range [0,2 ∗ π). An angle
is represented using three points. The function ExplodeAngle
compass” functions in Table 1 (the functions take concrete inputs returns these three points.
and output concrete objects). Length. Alengthis a number in the range [0,∞). The constructor
Our tool now searches for a program S that works correctly on Length(p ,p ) returns a length object denoting the distance
~ ~ 1 2
this one input-output pair (I ,O ). It searches for S by enumerat- between points p and p .
c c 1 2
ing programs up to a certain length. However, to reduce the size of Circle. A circle is represented as a pair of a point and a length. For
the search space, rather than using the basic library in Table 1, we a point p and length l, the constructor Circle(p,l) returns the
use an extended library that additionally implements functions in circle with center p and radius l. The radius of a circle is always
Table 2 (Idea 2). Furthermore, we use a heuristic goodness metric a nonzero positive number.
to make the search for S goal-directed (Idea 3). Program variables are typed and are given one of the five types
When searching for S, we generate several partial programs. defined above. A program takes some objects as inputs, and using
~
These partial programs will, when given the input I , generate dif-
c a predefined library Lib of functions F ,...,F , it constructs new
ferent geometric objects like points, lines and circles - all of which 1 k
are represented using points. Figure 1 shows all these intermediate objects and outputs one or more of these objects. Thus, a program
~ ~
takes as input I and uses (tuples of) temporary variables t to
points in two different settings. On the left, we show the points gen- i
~
erated when we use the goodness metric to prune the search space, compute the output O as follows:
andontheright, we show the points generated when we do not use ~
the goodness metric. It is clearly evident that when we do not use a geoProgram(I):
~ ~
t :=F (V );
1 π 1
goodness metric to prune the search space, then the approach does 1
not scale. .
.
~ .
Once we find a program S that works on input I , we return it
c ~ ~
t :=F (V );
n π n
if it also works correctly on a second randomly sampled concrete n
~ ~
input. The program synthesized by our tool for the above problem O:=Vn+1;
~
(using the extended library in Table 2) is: return O;
Test10(p1,p2,L,r,a): where
L1 := ConstructLineGivenAngleLinePoint(L,a,p1); ~ ~
• each variable in V is either an input variable from I, or a
i
C1 := ConstructCircleGivenPointLength(p1,r); ~
temporary variable from t such that j < i, and
j
(p3,p4) := LineCircleIntersection(L1,C1); • 1 ≤ π ≤ k.
i
L2 := PerpendicularBisector2Points(p2,p3);
p5 := LineLineIntersection(L1,L2); 3.1 TheExpressionLanguage
return p5; Thereisonlyonekindofexpressioninourgeometryprogramming
~
The line L1 is good because the output point p lies on it. The language, namely a function call F (V ), where F is a function
i i
circle C1 is good because it intersects an existing object (namely, fromagivenlibrary. The library for “ruler-and-compass” construc-
line L1) at a good point p3: p3 is good because it is equidistant tions is shown in Table 1. It consists of functions for constructing
from the output point p and the input point p . Similarly, we can lines, circles, and lengths from points, and functions for construct-
2
establish goodness of all the other intermediate objects. Without ing points from line-line intersection, line-circle intersection, and
Points generated by goal-directed search Points generated by brute-force search
depth 0 (Input) depth 0 (Input)
250 depth 1 depth 1
depth 2 depth 2
depth 3 100 depth 3
depth 4 depth 4
depth 5 (Output) depth 5
200 depth 6 (Output)
150 50
y 100 y
50 0
0
-50
-50
-50 0 50 100 150 200 250 -50 0 50 100
x x
Figure 1. Points visited in a goal-directed search (left) and a brute-force search (right). The concrete inputs and output were picked
independently in the two runs. The output point was not reached in the brute-force search and the search had to be truncated.
Function Description
L = Line(p1,p2) Listheline joining p1 and p2 (provided p1 6= p2).
C = Circle(p,r) Cisthecircle with center p and radius r.
r = Length(p1,p2) r is the length of the segment from p1 to p2 (provided p1 6= p2).
p = LineLineXn(L1,L2) pis the point that lies at the intersection of L1 and L2 (provided L1, L2 are not parallel).
p~ = LineCircleXn(L1,C1) p~ is the vector containing (1 or 2) points that lie on both L1, C1 (provided they intersect).
p~ = CircleCircleXn(C1,C2) p~ is the vector containing (1 or 2) points that lie on both C1, C2 (provided they intersect).
p~ = ExplodeAngle(a) p~ is the vector of (three) points that define angle a.
Table 1. Library functions in the geometry programming language: the type of p1,p2,... is Point, p~ is a vector of points, L is a line, C a
circle, a an angle, and r a length.
circle-circle intersection. It also consists of a function to expose andwecanspecifythatLine(p ,p )andLine(p ,p )areperpen-
1 2 3 4
points that define a given angle. It is not difficult to observe that dicular as an equality between arithmetic expressions:
programs in our geometry programming language correspond di- slope(p ,p )∗slope(p ,p ) = −1
rectly to “ruler-and-compass” constructions on paper. 1 2 3 4
However, the library shown in Table 1 contains only the primi-
tive “ruler-and-compass” operations. It can be extended by includ- 4. ProblemDefinition
ing new (derived) functions such as those in Table 2. We later show Our goal is to synthesize programs in our geometry programming
that suchanextensionenablessynthesisofnontrivialgeometrypro- language given their specification in the form of precondition and
grams. postcondition. Here we will formally define the synthesis problem
for the geometry domain.
The synthesis problem is given the specification of the desired
3.2 TheSpecification Language programandalsotheexecutablecodeimplementingagivenlibrary.
Thespecificationlanguageisusedtowritethepreconditionandthe The goal of the geometry synthesis problem is to discover a pro-
postcondition of a geometry program. gram in the geometry programming language that correctly imple-
A specification is given as a conjunction of atomic facts. An ments the specification.
atomic fact is an equality or inequality between two arithmetic Formally, the geometry synthesis problem requires the user to
expressions. An arithmetic expression is built using the standard provide the following:
~ ~ ~ ~ ~
• A specification hI,O,φ (I),φ (I,O)i of the desired
arithmetic operations, +,−,∗, applied on numeral objects, the pre post
LengthandAnglefunctions, and the functions: program, which includes
~ ~
• distL(p,L)returns distance between point p and line L. • a tuple of typed input variables I and output variables O.
~
• slope(L)returns the slope of line L. • a formula φ (I) that specifies the precondition and a
pre
~ ~
We found that these functions were sufficient to describe almost formula φ (I,O)that specifies the postcondition.
post
all high-school geometry problems. For example, note that we can • Alibrary of executable specifications
specify that “point p lies on line joining points p and p ” as an
1 2 ~ ~ ~
equality between two slopes, Lib := {hI ,O ,F (I )i | i = 1,...,k},
i i i i
where F is an executable implementation of the i-th library
i
slope(p,p ) = slope(p ,p ), function.
1 1 2
no reviews yet
Please Login to review.
