Relational program synthesis with numerical reasoning Celine Hocquette Andrew Cropper University of Oxford

2025-04-29 0 0 1.21MB 15 页 10玖币

侵权投诉

Relational program synthesis with numerical reasoning

C´

eline Hocquette, Andrew Cropper

University of Oxford

celine.hocquette@cs.ox.ac.uk, andrew.cropper@cs.ox.ac.uk

Abstract

Program synthesis approaches struggle to learn programs with

numerical values. An especially difﬁcult problem is learn-

ing continuous values over multiple examples, such as inter-

vals. To overcome this limitation, we introduce an inductive

logic programming approach which combines relational learn-

ing with numerical reasoning. Our approach, which we call

NUMSYNTH, uses satisﬁability modulo theories solvers to ef-

ﬁciently learn programs with numerical values. Our approach

can identify numerical values in linear arithmetic fragments,

such as real difference logic, and from inﬁnite domains, such

as real numbers or integers. Our experiments on four diverse

domains, including game playing and program synthesis, show

that our approach can (i) learn programs with numerical values

from linear arithmetical reasoning, and (ii) outperform exist-

ing approaches in terms of predictive accuracies and learning

times.

1 Introduction

Zendo is a game in which one player, the Master, creates a

rule for structures that the rest of the players, as Students,

try to discover by building and studying structures which

follow or break the rule. The ﬁrst student to correctly guess

the rule wins. For instance, suppose the structure on the left

of Figure 1a follows the secret rule while the one on the right

does not. Figure 1b shows a possible secret rule. It states

that structures must have two pieces in contact, one with

size at least 7. Discovering this rule involves identifying the

numerical value 7.

Suppose we want to use machine learning to play Zendo,

i.e. to learn secret rules from examples of structures. Then

we need an approach that can (i) learn explainable rules, and

(ii) generalise from small numbers of examples. However,

these requirements are difﬁcult for standard machine learning

techniques, yet are crucial for many real-world problems

(Cropper et al. 2022).

Inductive logic programming (ILP) (Muggleton 1991) is

a form of machine learning that can learn explainable rules

from small numbers of examples. Existing ILP techniques

could, for instance, learn rules for simple Zendo problems.

However, existing approaches struggle to learn rules that

require identifying numerical values from inﬁnite domains

(Corapi, Russo, and Lupu 2011; Evans and Grefenstette 2018;

Cropper and Morel 2021). Moreover, although some ILP ap-

Positive example Negative example

(a) Examples

zendo(A) ←piece(A,B), contact(B,C),

size(C,D), geq(D,7).

(b) A rule which states that two pieces are in contact,

one with size greater or equal than 7.

zendo(A) ←piece(A,B), contact(B,C), size(C,D),

geq(D,N), @numerical(N).

Figure 1: Learning a hypothesis for Zendo. Learning this

hypothesis involves reasoning with the numerical predicate

geq represented in bold to identify the numerical value 7.

proaches can learn programs with numerical values (Muggle-

ton 1995; Hocquette and Cropper 2022), they cannot perform

complex numerical reasoning, such as identifying numerical

values by reasoning over multiple examples jointly. For in-

stance, they struggle to learn that the size of one piece must

be greater than some particular numerical value, or that the

sum of the coordinates describing the position of a piece must

be lower than some particular numerical value. These limita-

tions are not speciﬁc to ILP and, as far as we are aware, apply

to all current program synthesis approaches (Raghothaman

et al. 2019; Ellis et al. 2018; Shi et al. 2022).

To overcome these limitations, we introduce an approach

that can identify numerical values from inﬁnite domains and

reason from multiple examples. The key idea of our approach

is to decompose the learning task into two stages (i) program

search, and (ii) numerical search.

In the program search stage, the learner searches for partial

hypotheses (sets of rules) with variables in place of numer-

ical symbols. This step follows ALEPH’s lazy evaluation

procedure (Srinivasan and Camacho 1999). For example, to

arXiv:2210.00764v2 [cs.LG] 4 Oct 2022

learn a rule for Zendo, the learner may generate the partial

hypothesis shown in Figure 1c. In this hypothesis, the ﬁrst-

order variable

is marked as a numerical variable with the

predicate symbol @numerical but is not yet bound to any

particular value.

In the numerical search stage, the learner searches for val-

ues for the numerical variables using the training examples.

We encode the search for numerical values as a satisﬁability

modulo theories (SMT) formula. For instance, to ﬁnd values

for

in the hypothesis in Figure 1c, the learner executes

the partial hypothesis without its numerical literal geq(D,N)

against the examples to ﬁnd possible substitutions for the vari-

able

, from which it builds a system of linear inequations.

These inequations constrain the search for the numerical vari-

able

with the values obtained for

from the examples.

Finally, the learner substitutes

in the partial program with

any solution found for the inequations.

To implement our idea, we build on the state-of-the-art

learning from failures (LFF) (Cropper and Morel 2021) ILP

approach. LFF is a constraint-driven ILP approach where the

goal is to accumulate constraints on the hypothesis space. A

LFF learner continually generates and tests hypotheses, from

which it infers constraints. We implement our numerical rea-

soning approach in NUMSYNTH, which, as it builds on the

LFF learner POPPER, supports predicate invention and learn-

ing recursive and optimal (in textual complexity) programs.

NUMSYNTH uses built-in numerical literals to additionally

support linear arithmetical reasoning over real numbers and

integers.

Novelty and Contributions

Compared to existing ap-

proaches, the main novelty of our approach is expressiv-

ity: NUMSYNTH can learn programs with numerical values

which require reasoning over multiple examples in linear

arithmetic fragments. In other words, our approach can learn

programs that existing approaches cannot. For instance, our

experiments show that our approach can learn programs of

the form shown in Figure 1b. In addition, our approach can

(i) efﬁciently search for numerical values in inﬁnite domains

such as real numbers or integers, (ii) identify numerical val-

ues which may not appear in the background knowledge, and

(iii) learn programs with several chained numerical literals.

For instance, it can learn that the sum of two variables is

lower than some particular numerical value. As far as we

are aware, no existing approach can efﬁciently solve such

problems. Overall, we make the following contributions:

We introduce an approach for numerical reasoning in inﬁ-

nite domains. Our approach supports numerical reasoning

in linear arithmetic fragments.

We implement our approach in NUMSYNTH, which can

learn programs with numerical values, perform predicate

invention, and learn recursive and optimal programs.

We experimentally show on four domains (geometry, bi-

ology, game playing, and program synthesis) that our

approach can (i) learn programs requiring numerical rea-

soning, and (ii) outperform existing ILP systems in terms

of learning time and predictive accuracy.

2 Related Work

Program Synthesis.

Program synthesis approaches that

enumerate the search space (Raghothaman et al. 2019; Ellis

et al. 2018; Evans et al. 2021) can only learn from small

and ﬁnite domains and cannot learn from inﬁnite domains.

Several program synthesis systems delegate the search for

programs to an SMT solver (Jha et al. 2010; Gulwani et al.

2011; Reynolds et al. 2015; Albarghouthi et al. 2017). By

contrast, we delegate the numerical search to an SMT solver.

Moreover, NUMSYNTH can learn programs with numerical

values from inﬁnite domains. Sketch (Solar-Lezama 2009)

uses a SAT solver to search for suitable constants given a

partial program, where the constants can be numerical val-

ues. This approach is similar to our numerical search stage.

However, Sketch does not learn the structure of programs but

expects as input a skeleton of a solution: it requires a partial

program and its task is to ﬁll in missing values with constants

symbols. By contrast, NUMSYNTH learns both the program

and numerical values.

ILP.

Many ILP approaches (Muggleton 1995; Srinivasan

2001) use bottom clause construction to search for programs.

However, these approaches can only identify numerical val-

ues that appear in the bottom clause of a single example.

They cannot reason about multiple examples jointly, which

is, for instance, necessary to learn inequations.

Constraint inductive logic programming (Sebag and Rou-

veirol 1996) uses constraint logic programming to learn pro-

grams with numerical values. This approach generalises a

single positive example given some negative examples and is

restricted to numerical reasoning in difference logic.

Anthony and Frisch (1997) propose an algorithm to learn

hypotheses with numerical literals. FORS (Karali

c and

Bratko 1997) ﬁts regression lines to subsets of the positive ex-

amples in a positive example only setting. In contrast to NUM-

SYNTH, these two approaches allow some error in numerical

values predicted by numerical literals. However, these two ap-

proaches follow top-down reﬁnement with one specialisation

step at a time, which prevents them from learning hypotheses

with multiple chained numerical literals.

TILDE (Blockeel and De Raedt 1998) uses a discretiza-

tion procedure to ﬁnd candidate numerical constants while

making the induction process more efﬁcient (Blockeel and

De Raedt 1997). However, TILDE cannot learn recursive

programs and struggles to learn from small numbers of ex-

amples.

Many recent ILP systems enumerate every possible rule in

the search space (Corapi, Russo, and Lupu 2011; Kaminski,

Eiter, and Inoue 2018; Evans and Grefenstette 2018; Sch

uller

and Benz 2018) or all constant symbols as unary predicate

symbols (Evans and Grefenstette 2018; Cropper and Morel

2021; Purgał, Cerna, and Kaliszyk 2022) and therefore cannot

handle inﬁnite domains.

LFF.

Recent LFF systems represent constant symbols with

unary predicate symbols (Cropper and Morel 2021; Purgał,

Cerna, and Kaliszyk 2022), which prevents them from learn-

ing in inﬁnite domains. MAGICPOPPER (Hocquette and Crop-

per 2022) can identify constant symbols from inﬁnite do-

mains. Similar to ALEPH’s lazy evaluation approach and

our program search approach, MAGICPOPPER builds partial

hypotheses with variables in place of constant symbols. It

then executes the partial hypotheses independently over each

example to identify particular candidate constant symbols.

However, it may ﬁnd an intractable number of candidate

constants when testing hypotheses with non-deterministic

predicates with a large or inﬁnite number of answer substi-

tutions, such as greater than. Moreover, it cannot perform

numerical reasoning from multiple examples jointly. By con-

trast, NUMSYNTH uses all of the examples simultaneously

when reasoning about numerical values so it can learn inter-

vals whereas MAGICPOPPER cannot.

Lazy Evaluation.

The most related work is an extension

of ALEPH that supports lazy evaluation (Srinivasan and Ca-

macho 1999). During the construction of the bottom clause,

ALEPH replaces numerical values with existentially quanti-

ﬁed variables. During the reﬁnement search of the bottom

clause, ALEPH ﬁnds substitutions for these variables by exe-

cuting the partial hypothesis on the examples. This procedure

can predict output numerical variables using custom loss func-

tions measuring error (Srinivasan et al. 2006), while NUM-

SYNTH cannot. However, ALEPH needs the user to write

background deﬁnitions to ﬁnd numerical values, such as a

deﬁnition for computing a threshold or linear regression co-

efﬁcients from data. By contrast, NUMSYNTH has numerical

literals built-in. Moreover, ALEPH executes each deﬁnition

used during lazy evaluation independently which prevents it

from learning hypotheses with multiple literals requiring lazy

evaluation sharing variables, such as an upper and a lower

bound for the same variable. By contrast, NUMSYNTH can

learn hypotheses with multiple chained numerical literals.

Finally, ALEPH does not support predicate invention, is not

guaranteed to learn optimal (textually minimal) programs,

and struggles to learn recursive programs.

3 Problem Setting

We now describe our problem setting. We assume familiarity

with logic programming (Lloyd 2012). Our problem setting

is the learning from failures (LFF) (Cropper and Morel 2021)

setting, which is based on the learning from entailment setting

(Muggleton and De Raedt 1994) of ILP. LFF assumes a

meta-language

, which is a language about hypotheses. LFF

uses hypothesis constraints to restrict the hypothesis space.

Hypothesis constraints are expressed in

. A LFF input is

deﬁned as:

Deﬁnition 1

A LFF input is a tuple

(E+, E−, B, H, C)

where

E+

and

E−

are sets of ground atoms representing

positive and negative examples respectively,

is a deﬁnite

program representing background knowledge,

is a hypoth-

esis space, and

is a set of hypothesis constraints expressed

in the meta-language L.

Given a set of hypotheses constraints

, we say that a hypoth-

esis

is consistent with

if, when written in

does

not violate any constraint in

. We call

the subset of

consistent with C. We deﬁne a LFF solution:

Deﬁnition 2

Given a LFF input

(E+, E−, B, H, C)

, a LFF

solution is a hypothesis

H∈ HC

such that

is complete

with respect to

E+

(

∀e∈E+, B ∪H|=e

) and consistent

with respect to E−(∀e∈E−, B ∪H6|=e).

Conversely, given a LFF input, a hypothesis

is incomplete

when

∃e∈E+, H ∪B6|=e

, and is inconsistent when

∃e∈

E−, H ∪B|=e.

In general, there might be multiple solutions given a LFF

input. We associate a cost to each hypothesis and prefer

optimal solutions, which are solutions with minimal cost. In

the following, we use as cost function the size of hypotheses,

measured as the number of literals in it.

A hypothesis which is not a solution is called a failure. A

LFF learner identiﬁes constraints from failures to restrict the

hypothesis space. For instance, if a hypothesis is inconsistent,

ageneralisation constraint prunes its generalisations, as they

are provably also inconsistent.

4 Numerical Reasoning

We extend the framework in the previous section to allow

numerical reasoning in possibly inﬁnite domains. We assume

familiarity with SMT theory (De Moura and Bjørner 2011).

The idea is to separate the search into two stages (i) program

search, and (ii) numerical search. First, the learner generates

partial programs with ﬁrst-order numerical variables in place

of numerical values. Then, the learner searches for numerical

values to ﬁll in the numerical variables.

4.1 Program Search

The learner ﬁrst searches for partial programs with variables,

called numerical variables, in place of numerical values.

Numerical Variables.

We extend the meta-language

LFF to contain numerical variables. A numerical variable is

a ﬁrst-order variable that can be substituted by a numerical

value, i.e. a numerical variable acts as a placeholder for a

numerical symbol. In the following, we represent numerical

variables with the unary predicate symbol @numerical. For

example, in the program in Figure 1c, the variable

marked

with the syntax @numerical is a numerical variable.

Numerical Literals.

A numerical literal is a literal which

requires numerical reasoning and whose arguments all are nu-

merical. A numerical literal may contain numerical variables

as arguments. During the program search stage, the learner

builds partial hypotheses with variables in place of numerical

variables in numerical literals. For example, the learner may

generate the following program, where the literal leq(B,N) is

a numerical literal which contains the numerical variable

H: f(A) ←length(A,B), leq(B,N), @numerical(N)

Related Variables.

A related variable is a variable that ap-

pears both in a numerical literal and a regular literal. Related

variables act as bridges between relational learning and nu-

merical reasoning. For instance, the variable

is a variable

related to the numerical variable

in the program

above.

Possible substitutions for the related variables are identiﬁed

by executing the hypothesis without its numerical literals over

the positive and negative examples. For instance, given the

positive examples

{f([a, b]), f([])}

and the negative exam-

ples

{f([b, c, a, d, e, f]), f([c, e, d, a, b])}

, the hypothesis

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

RelationalprogramsynthesiswithnumericalreasoningC´elineHocquette,AndrewCropperUniversityofOxfordceline.hocquette@cs.ox.ac.uk,andrew.cropper@cs.ox.ac.ukAbstractProgramsynthesisapproachesstruggletolearnprogramswithnumericalvalues.Anespeciallydifcultproblemislearn-ingcontinuousvaluesovermultipleexampl...

展开>> 收起<<

Relational program synthesis with numerical reasoning Celine Hocquette Andrew Cropper University of Oxford.pdf

共15页,预览3页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

Relational program synthesis with numerical reasoning Celine Hocquette Andrew Cropper University of Oxford

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: