Machine Learning Meets The Herbrand Universe Jelle Piepenbrock1 2Josef Urban2Konstantin Korovin3Miroslav Ol ˇsak4Tom Heskes1and Mikola ˇs Janota2

2025-05-02 0 0 463.54KB 8 页 10玖币

侵权投诉

Machine Learning Meets The Herbrand Universe

Jelle Piepenbrock, 1, 2 Josef Urban, 2Konstantin Korovin, 3Miroslav Olˇ

s´

ak, 4Tom Heskes 1and

Mikolaˇ

s Janota 2

1Radboud University Nijmegen, the Netherlands

2Czech Technical University in Prague, Czech Republic

3University of Manchester, United Kingdom

4Institut des Hautes ´

Etudes Scientiﬁques Paris, France

Abstract

The appearance of strong CDCL-based propositional (SAT)

solvers has greatly advanced several areas of automated rea-

soning (AR). One of the directions in AR is thus to apply SAT

solvers to expressive formalisms such as ﬁrst-order logic, for

which large corpora of general mathematical problems exist

today. This is possible due to Herbrand’s theorem, which al-

lows reduction of ﬁrst-order problems to propositional prob-

lems by instantiation. The core challenge is choosing the right

instances from the typically inﬁnite Herbrand universe.

In this work, we develop the ﬁrst machine learning system

targeting this task, addressing its combinatorial and invari-

ance properties. In particular, we develop a GNN2RNN ar-

chitecture based on an invariant graph neural network (GNN)

that learns from problems and their solutions independently

of symbol names (addressing the abundance of skolems),

combined with a recurrent neural network (RNN) that pro-

poses for each clause its instantiations. The architecture is

then trained on a corpus of mathematical problems and their

instantiation-based proofs, and its performance is evaluated in

several ways. We show that the trained system achieves high

accuracy in predicting the right instances, and that it is ca-

pable of solving many problems by educated guessing when

combined with a ground solver. To our knowledge, this is the

ﬁrst convincing use of machine learning in synthesizing rele-

vant elements from arbitrary Herbrand universes.

1 Introduction

Quantiﬁers lie at the heart of mathematical logic, modern

mathematics and reasoning. They enable expressing state-

ments about inﬁnite domains. Practically all today’s systems

used for formalization of mathematics and software veriﬁca-

tion are based on expressive foundations such as ﬁrst-order

and higher-order logic, set theory and type theory, that make

essential use of quantiﬁcation.

Instantiation is a powerful tool for formal reasoning with

quantiﬁers. The power of instantiation is formalized by Her-

brand’s theorem (Herbrand 1930), which states, roughly

speaking, that within ﬁrst-order logic (FOL), quantiﬁers can

always be eliminated by the right instantiations. Herbrand’s

theorem further states that it is sufﬁcient to consider instanti-

ations from the Herbrand universe, which consists of terms

with no variables (ground terms) constructed from the sym-

bols appearing in the problem. This fundamental result has

been explored in automated reasoning (AR) systems since

the 1950s (Davis 2001). In particular, once the right in-

stantiations are discovered, the problem typically becomes

easy to decide by methods based on state-of-the-art SAT

solvers (Silva, Lynce, and Malik 2009).

Coming up with the right instantiations is however non-

trivial. The space of possible instantiations (the Herbrand

universe) is typically inﬁnite and complex. The general un-

decidability of theorem proving is obviously connected to

the hardness of ﬁnding the right instantiations, which in-

cludes ﬁnding arbitrarily complex mathematical objects.

Contributions: In this work we develop the ﬁrst machine

learning (ML) methods that automatically propose suitable

instantiations. This is motivated both by the growing ability

of ML methods to prune the search space of automated theo-

rem provers (ATPs) (Kaliszyk et al. 2018), and also by their

growing ability to synthesize various logical data (Gauthier

2020; Urban and Jakub˚

uv 2020). In particular:

1. We construct an initial corpus of instantiations by re-

peatedly running a randomized grounding procedure fol-

lowed by a ground solver (Section 2) on 113332 clausal

ATP problems extracted from the Mizar Mathematical

Library. We analyze the solutions, showing that almost

two thirds of the instances contain newly introduced

skolem symbols created by the clausiﬁcation (Section 3).

2. We develop a targeted GNN2RNN neural architecture

based on a graph neural network (GNN) that learns

to characterize the problems and their clauses indepen-

dently of the symbol names (addressing the abundance

of skolems), combined with a recurrent neural network

(RNN) that proposes for each clause its instantiations

based on the GNN characterization (Section 4).

3. The GNN2RNN is trained and used to propose instances

for the problems. Its training starts with the randomized

solutions and continues by learning from its own success-

ful predictions. We show that the system achieves high

accuracy in predicting the instances (Section 5).

4. Finally, the trained neural network when combined with

the ground solver is shown to be able to solve a large

number of testing problems by educated guessing (Sec-

tion 5). To our knowledge, this is the ﬁrst convincing use

of machine learning in general synthesis of relevant ele-

ments from arbitrary Herbrand universes.

arXiv:2210.03590v1 [cs.LG] 7 Oct 2022

(1) instantiate xby head symbol t

with arity 2and zby gof arity 1

(going from level0to level1)

(2) instantiate x1, x2, z1by

constants c,c, and e, respectively

(going from level1to level2)

∀x z P(f(x,z) )

∀x1x2z1P(f(t(x1,x2),g(z1) ) )

P(f(t(c,c),g(e) ) )

t/2g/1

c/0c/0e/0

Figure 1: Term instantiation through incremental deepening. In the ﬁgure, there are two instantiation steps, one after the other.

2 Ground Solver

There are several ways how to combine instantiation of

clausal ﬁrst-order problems with decidable and efﬁcient

(un)satisﬁability checking of their proposed ground in-

stances. The most direct approach (used in instantiation-

based ATPs such as iProver (Korovin 2008)) is to explic-

itly add axioms for equality, allowing their instantiation

as for any other axioms, and directly use SAT solvers for

the ground checking. An alternative approach is to avoid

explicit addition of the equality axioms, and instead use

combinations of SAT solvers with ground congruence clo-

sure (Detlefs, Nelson, and Saxe 2005; Nieuwenhuis and

Oliveras 2007).

We have explored both approaches and ultimately decided

to use the latter in this work. The main reason is that the

combinations of SAT solvers with ground congruence clo-

sure are today very efﬁciently implemented (Barrett et al.

2021), posing practically no issues even with thousands of

instances. Using the most direct approach would, on the

other hand, require a large number of additional instances of

the equality axioms to successfully solve the ground prob-

lems. In our preliminary measurements, the average ratio of

such necessary additional instances was over 40%, which

would exponentially decrease the chance of randomly pre-

dicting the right set of instances.

In more detail, we use as our ground solver an efﬁ-

cient combination of a SAT solver with ground congru-

ence closure provided in the Vampire automated theorem

prover (Kov´

acs and Voronkov 2013). Here, the SAT solver

abstracts ﬁrst-order logic atoms as propositional variables

and starts producing satisfying assignments (models) of this

abstraction, which are then checked against the properties

of equality (reﬂexivity, transitivity, congruence, symmetry).

This process terminates when a model is found that satisﬁes

the equality properties, or when the SAT solver runs out of

models to try. In that case, the original problem is unsatisﬁ-

able, which means that the ground instances were proposed

correctly by the ML system.

3 Dataset of Mathematical Problems

We construct a corpus of instantiations by repeatedly run-

ning a randomized grounding procedure (Section 3.1) on

113 332 ﬁrst-order ATP problems made available to us

by the AI4REASON project.1They originate from the

Mizar Mathematical Library (MML) (Kaliszyk and Urban

2015) and are exported to ﬁrst-order logic by the MPTP

system (Urban 2006). All these problems have an ATP

1https://github.com/ai4reason/ATP Proofs

proof (in general in a high time limit) found by either

the E/ENIGMA (Schulz 2013; Jakub˚

uv et al. 2020) or

Vampire/Deepire (Kov´

acs and Voronkov 2013; Suda 2021)

systems. Additionally, the problems’ premises have been

pseudo-minimized (Kaliszyk and Urban 2014) by iterated

Vampire runs. We use the pseudo-minimized versions be-

cause our focus here is on guiding instantiation rather than

premise selection. The problems come from 38 108 prob-

lem families, where each problem family corresponds to

one original Mizar theorem. Each of these theorems can

have multiple minimized ATP proofs using different sets of

premises. The problems range from easier to challenging

ones, across various mathematical ﬁelds such as topology,

set theory, logic, algebra and linear algebra, real, complex

and multivariate analysis, trigonometry, number and graph

theory, etc.

We ﬁrst clausify the problems by E, and then repeatedly

run the randomized grounding procedure on all of them, fol-

lowed by the ground solver using a 30s time limit. The ﬁrst

run solves 3897 of the problems, growing to 7790 for the

union of the ﬁrst 9 runs, and to 11675 for the union of the

ﬁrst 100 runs. The 113332 problems have on average 35.6

input clauses and the 3897 problems solved in the ﬁrst run

have on average 12.8 input clauses. 6.0 instances are needed

on average to solve a problem.2

Note that each clause can in general be instantiated more

than once. Also, 3.9 (almost two thirds) of the instances con-

tain on average at least one skolem symbol.

This means that we strongly need a learning architec-

ture invariant under symbol renamings, rather than off-the-

shelf architectures (e.g., transformers) that depend on ﬁxed

consistent naming. This motivates our use of a property-

invariant graph neural architecture (Section 4).

3.1 Randomized Grounding Procedure

Randomized grounding can be parameterized in various

ways. To develop the initial dataset here we use a sim-

ple multi-pass randomized grounding with settings that

roughly correspond to our ML-guided instantiation archi-

tecture (Section 4). These settings are as follows. We use

at most two passes (levels) of instantiation for every input

clause. In the ﬁrst pass, for each variable we randomly se-

lect an arbitrary function symbol from the problem’s signa-

ture, and provide it (if non-constant) with fresh variables as

arguments. In the second pass, we ground all variables with

randomly selected constants from the problem’s signature.

The ﬁrst pass is repeated 25 times for each clause in its in-

2Over 40 instances (max. 63) are used in some problems

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

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

10 玖币 0人已下载

立即下载

摘要：

MachineLearningMeetsTheHerbrandUniverseJellePiepenbrock,1,2JosefUrban,2KonstantinKorovin,3MiroslavOls´ak,4TomHeskes1andMikolasJanota21RadboudUniversityNijmegen,theNetherlands2CzechTechnicalUniversityinPrague,CzechRepublic3UniversityofManchester,UnitedKingdom4InstitutdesHautes´EtudesScientiquesPar...

展开>> 收起<<

Machine Learning Meets The Herbrand Universe Jelle Piepenbrock1 2Josef Urban2Konstantin Korovin3Miroslav Ol ˇsak4Tom Heskes1and Mikola ˇs Janota2.pdf

共8页,预览2页

还剩页未读，继续阅读

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

Machine Learning Meets The Herbrand Universe Jelle Piepenbrock1 2Josef Urban2Konstantin Korovin3Miroslav Ol ˇsak4Tom Heskes1and Mikola ˇs Janota2

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: