A Neural Network Solves and Generates Mathematics

--00000000000034462705d4eb1a5c--
From MAILER-DAEMON Thu Jan 06 10:30:08 2022
Received: from list by lists.gnu.org with archive (Exim 4.90_1)
id 1n5UiO-0003EM-2b
for mharc-axiom-developer@gnu.org; Thu, 06 Jan 2022 10:30:08 -0500
Received: from eggs.gnu.org ([209.51.188.92]:48796)
by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from )
id 1n5UiM-0003CJ-Hm
for axiom-developer@nongnu.org; Thu, 06 Jan 2022 10:30:06 -0500
Received: from [2607:f8b0:4864:20::72e] (port=42911
helo=mail-qk1-x72e.google.com)
by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
(Exim 4.90_1) (envelope-from )
id 1n5UiE-0007ev-6T
for axiom-developer@nongnu.org; Thu, 06 Jan 2022 10:30:00 -0500
Received: by mail-qk1-x72e.google.com with SMTP id r139so2964359qke.9
for ; Thu, 06 Jan 2022 07:29:57 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112;
h=mime-version:from:date:message-id:subject:to;
bh=IMEnSBETC7eButmPxoofZswdQB8NocXxjUP1TKUc4Os=;
b=IlpR6BYyd128d6kx0vfV7OedX3i9zMxgecbADQHzYo+ZREeDqFdIdBJ7x3iRR0plQb
zWGR5c2iLJKmziKcxYfxLUCOt7C2HfSMWV/1K4GR9LODUacZLZUoGEiVXYjtdqEvvR9p
WG4J47e2hlhMl7pZ5J94mjCyiSKkpKeKeImbRRg9CObe6K1xPx3TBARquJd0zkzzMEXu
J6SpLosnQJ7mXrwMeJ1PFtbUM3Nk0txL579pBcF0PeW4Ex1ZalI6m+Cu8NMCyQk6PveH
g9ut1AQKDGlB5SHGVQMw4NFRLJBktjj0WNAkmxcdF15IUPs5dJUZTpjxDwrxY8xjN02i
0TSg==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=1e100.net; s=20210112;
h=x-gm-message-state:mime-version:from:date:message-id:subject:to;
bh=IMEnSBETC7eButmPxoofZswdQB8NocXxjUP1TKUc4Os=;
b=PSL8W0fNWdUYSbvYGlkw7ZBchSqvNN4edQLhNLUoeSZZuqkuaA475L6jvUA9LNQUIv
IR/p9AzSfmI3HMLrqavN3VQ7vuqC69hx2HCvCcYo4YBhECKhB1zfhwHvFsdXUoIT4VxZ
v8t6BTs9+Dhov4gPeHo9F1ggjUGXESZWqGANr7FJDtZgEgrcQDSJ6z4HxH3aO98CfM0r
Fjp3OCVOZybJrbTJFD/pA38iGM6N2HH/u/fKKYuxvCaJ7cYp/Y6FqKjUEFXa9fKsi+WG
Q623a3Goy2jQ9Uls7ERUEl/tgNDPVRzKceLHcSFpdKlQRJz7StCHKN7iW41rDt+m6DtL
SVbQ==
X-Gm-Message-State: AOAM530QibPDp04v7NCwdnrRr8Fbh1ILRtiJgzfGm0OL7OVGUjkr7Rem
PPb6F4ZGXm2eA9l2LRvUBCqq3h/wlcNgjwDVd/s=
X-Google-Smtp-Source: ABdhPJwTw8zQoPbY6MQqsuTHUOlSkwY8JWLSjLkbIDulmDTool+btPF1MPg5151aWlgKlajG6VQxtwkKc0b4tRvBimk=
X-Received: by 2002:a05:620a:371e:: with SMTP id
de30mr42630155qkb.136.1641482997018;
Thu, 06 Jan 2022 07:29:57 -0800 (PST)
MIME-Version: 1.0
From: Tim Daly
Date: Thu, 6 Jan 2022 10:29:43 -0500
Message-ID:
Subject: A NN Solves and Generates Math Problems
To: Frank Pfenning , Prof Robert Harper ,
mcarneir ,
Jeremy Avigad , axiom-dev ,
Tim Daly
Content-Type: multipart/alternative; boundary="000000000000f134e205d4eb8a72"
X-Host-Lookup-Failed: Reverse DNS lookup failed for 2607:f8b0:4864:20::72e
(failed)
Received-SPF: pass client-ip=2607:f8b0:4864:20::72e;
envelope-from=axiomcas@gmail.com; helo=mail-qk1-x72e.google.com
X-Spam_score_int: -12
X-Spam_score: -1.3
X-Spam_bar: -
X-Spam_report: (-1.3 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1,
DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, FREEMAIL_FROM=0.001,
HTML_MESSAGE=0.001, RCVD_IN_DNSWL_NONE=-0.0001, RDNS_NONE=0.793,
SPF_HELO_NONE=0.001, SPF_PASS=-0.001 autolearn=no autolearn_force=no
X-Spam_action: no action
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.29
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Thu, 06 Jan 2022 15:30:06 -0000
--000000000000f134e205d4eb8a72
Content-Type: text/plain; charset="UTF-8"
This is an interesting paper (especially given that it
is work under Gilbert Strang):
A Neural Network Solves and Generates Mathematics
Problems by Progam Synthesis: Calculus, Differential
Equations, Linear Algebra, and More.
https://arxiv.org/pdf/2112.15594.pdf
"This work shows that a neural network that generates
programs (i.e. program synthesis) is the key to solving
math and STEM courses at scale, as it turns question
answering into a programming task."
This seems interesting from several aspects:
1) Can this be applied to logic systems? Can it help
generate "proven code" from a proof system? (LEAN)
2) Can it be applied in programs like NuPRL / RedPRL?
(Innovations in Computational Type Theory using Nuprl
Journal of Applied Logic 4 (2006) pp 428--469
https://reader.elsevier.com/reader/sd/pii/S1570868305000704?token=C11F82ADA94390097338EF7E421A4D9DFEF909336A451BF51D3099EDF1025177323CCD7B46510F77FFC4955D0AC6724F&originRegion=us-east-1&originCreation=20220106150458
3) Can the type of an object be inferred by casting it as a
question in mathematics? Is the generated program correctly
typed?
4) Can this be layered on MetaMath (LEAN) or FDL (Nuprl)
to generate logically equivalent code?
5) Can this be applied to gradual typing?
In any case, this represents an interesting "interdisciplinary"
effort connecting the math department and CS.
Tim
There are various connections to Neural Networks and Math:
@misc{Crou19,
author = "Crouse, Maxwell and Whitehead, Spencer and
Abdelaziz, Ibrahim and Makni, Bassem and
Cornelio, Cristina and Kapanipathi, Pavan and
Pell, Edwin and Srinivas, Kavitha and
Thost, Veronika and Witbrock, Michael and
Fokoue, Achille",
title = {{A Deep Reinforcement Learning Base Approach to Learning
Transferable Proof Guidance Strategies}},
year = "2019",
linke = "\url{https://arxiv.org/pdf/1911.02065.pdf}",
abstract =
"Traditional first-order logic (FOL) reasoning systems usually
rely on manual heuristics for proof guidance. We propose TRAIL: a
system that learns to perform proof guidance using reinforcement
learning. A key design principle of our system is that it is
general enough to allow transfer to problems in different domains
that do not share the same vocabulary of the training set. To do
so, we developed a novel representation of the internal state of a
prover in terms of clauses and inference actions, and a novel
neural-based attention mechanism to learn interactions between
clauses. We demonstrate that this approach enables the system to
generalize from training to test data across domains with
different vocabularies, suggesting that the nerual architecture in
TRAIL is well suited for representing and processing of logical
formalisms.",
paper = "Crou19.pdf"
}
@misc{Crou19a,
author = "Crouse, Maxwell and Abdelaziz, Ibrahim and
Cornelio, Cristina and Thost, Veronika and
Wu, Lingfei and Forbus, Kenneth and Fokoue, Achille",
title = {{Improving Graph Neural Network Representations of Logical
Formulae with Subgraph Pooling}},
year = "2019",
linke = "\url{https://arxiv.org/pdf/1911.06904.pdf}",
abstract =
"Recent advances in the integration of deep learning with
automated theorem proving have centered around the representation
of graph-structured representations, in large part driven by the
rapidly emerging body of research in geometric deep
learning. Typically, structure-aware neural methods for embedding
logical formulae have been variants of either Tree LSTMs or
GNNs. While more effective than character and token-level
approaches, such methods have often made representational
trade-offs that limited their ability to effectively represent the
global structure of their inputs. In this work, we introduce a
novel approach for embedding logical formulae using DAG LSTMs that
is designed to overome the limitations of both Tree LSTMs and
GNNs. The effectiveness of the proposed framework is demonstrated
on the tasks of premise selection and proof step classification
where it achieves the state-of-the-art performance on two standard
datasets.",
paper = "Crou19a.pdf"
}
@misc{Gaut19,
author = "Gauthier, Thibault",
title = {{Deep Reinforcement Learning in HOL4}},
year = "2019",
link = "\url{https://arxiv.org/pdf/1910.11797.pdf}",
abstract =
"The paper describes an implementation of deep reinforcement
learning through self-supervised learning within the proof
assistant HOL4. A close interaction between the machine learning
modules and the HOL4 library is achieved by the choice of tree
neural networks (TNNs) as machine learning models and the internal
use of HOL4 terms to represent tree structures of TNNs. Recursive
improvement is possible when a given task is expressed as a search
problem. In this case, a Monte Carlo Tree Search (MCTS) algorithm
guided by a TNN can be used to explore the search space and
produce better examples for training the next TNN. As an
illustration, tasks over propositional and arithmetical terms,
representative of fundamental theorem proving techniques, are
specified and learned: truth estimation, end-to-end computation,
term rewriting and term synthesis.",
paper = "Gaut19.pdf"
}
@misc{Lamp19,
author = "Lample, Guillaume and Charton, Francois",
title = {{Deep Learning for Symbolic Mathematics}},
year = "2019",
link = "\url{https://arxiv.org/pdf/1912.01412.pdf}",
link = "\url{https://www.youtube.com/watch?v=O_sHHG5_lr8}",
abstract =
"Neural networks have a reputation for being better at solving
statistical or approximate problems than at performing
calculations or working with symbolic data. In this paper, we show
that they can be surprisingly good at more elaborated tasks in
mathematics, such as symbolic integration and solving differential
equations. We propose a syntax for representing mathematical
problems, and methods for generating large datasets that can be
used to train sequence-to-sequence models. We achieve results that
outperform commercial Computer Algebra Systems such as Matlab or
Mathematica.",
paper = "Lamp19.pdf",
keywords = "printed, DONE"
}
@misc{Olsa19,
author = "Olsak, Miroslav and Kaliszyk, Cezary and Urban, Josef",
title = {{Property Invariant Embedding for Automated Reasoning}},
year = "2019",
link = "\url{https://arxiv.org/pdf/1911.12073.pdf}",
abstract =
"Automated reasoning and theorem proving have recently become
major challenges for machine learning. In other domains,
representations that are able to abstract over unimportant
transformations, such as abstraction over translations and
rotations in vision, are becoming more common. Standard methods of
embedding mathematical formulas for learning theorem proving are
however yet unable to handle many important transformations. In
particular, embedding previously unseen labels, that often arise
in definitional encodings and in Skolemizatin, has been very weak
so far. Similar problems appear when tranferring knowledge between
known symbols.
We propose a novel encoding of formulas that extends existing
graph neural network models. This encoding represents symbols only
by nodes in the graph, without giving the network any knowledge of
the original labels. We provide additional links between such
nodes that allow the network to recover the meaning and therefore
correctly embed such nodes irrespective of the given labels. We
test the proposed encoding in an automated theorem prover based on
the tableaux connection calculus, and show that it improves on the
best characterizations used so far. The encoding is further
evaluated on the premise selection task and a newly introduced
symbol guessing task, and shown to correctly predict 65\% of the
symbol names.",
paper = "Olsa19.pdf"
}
@misc{Piot19,
author = "Piotrowski, Bartosz and Brown, Chad E. and
Kaliszyk, Cezary",
title = {{Can Neural Networks Learn Symbolic Rewriting?}},
year = "2019",
link = "\url{https://arxiv.org/pdf/1911.04783.pdf}",
abstract =
"This work investigates if the current neural architectures are
adequate for learning symbolic rewriting. Two kinds of data sets
are proposed for this research -- one based on automated proofs
and the other being a synthetic set of polynomial terms. The
experiments with use of the current neural machine translation
models are performed and its results are discussed. Ideas for
extending this line of research are proposed and its relevance is
motivated.",
paper = "Piot19.pdf"
}
@misc{Sanc19,
author = "Sanchez-Stern, Alex and Alhessi, Yousef and Saul, Lawrence
and Lerner, Sorin",
title = {{Generating Correctness Proofs with Neural Networks}},
year = "2019",
link = "\url{https://arxiv.org/pdf/1907.07794.pdf}",
abstract =
"Foundational verification allows programmers to build software
which has been empirically shown to have high levels of assurance
in a variety of important domains. However, the cost of producing
foundationally verified software remains prohibitively high for
most projects, as it requires significant manual effort by highly
trained experts. In this paper we present Proverbot9001 a proof
search system using machine learning techniques to produce proofs
of software correctness in interactive theorem provers. We
deomonstrate Proverbot9001 on the proof obligations from a large
practical proof project, the CompCert verified C compiler, and
show that it can effectively automate what was previously manual
proofs, automatically solving 15.77\% of proofs in our test
dataset. This corresponds to an over 3X improvement over the prior
state of the art machine learning technique for generating proofs
in Coq.",
paper = "Sanc19.pdf"
}
@misc{Wang19a,
author = "Wang, Qingxiang and Brown, Chad and Kaliszyk, Cezary and
Urban, Josef",
title = {{Exploration of Neural Machine Translation in
Autoformalization of Mathematics in Mizar}},
year = "2019",
link = "\url{https://arxiv.org/pdf/1912.02636.pdf}",
abstract =
"In this paper we share several experiments trying to
automatically translate informal mathematics into formal
mathematics. In our context informal mathematics refers to
human-written mathematical sentences in the LaTeX format; and
formal mathematics refers to statements in the Mizar language. We
conducted our experiments against three established neural
network-based machine translation models that are know to deliver
competitive results on translating between natural languages. To
train these models we also prepared four informal-to-formal
datasets. We compare and analyze our results according to whether
the model is supervised or unsupervised. In order to augment the
data available for auto-formalization and improve the results, we
develop a custom type-elaboration mechanism and integrate it into
the supervised translation.",
paper = "Wang19a.pdf"
}
--000000000000f134e205d4eb8a72
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

--000000000000c3745f05d5397925--
From MAILER-DAEMON Sat Jan 22 21:16:46 2022
Received: from list by lists.gnu.org with archive (Exim 4.90_1)
id 1nBSQw-0001MH-GP
for mharc-axiom-developer@gnu.org; Sat, 22 Jan 2022 21:16:46 -0500
Received: from eggs.gnu.org ([209.51.188.92]:47702)
by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from )
id 1nBSQu-0001M8-3K
for axiom-developer@nongnu.org; Sat, 22 Jan 2022 21:16:44 -0500
Received: from [2607:f8b0:4864:20::733] (port=37408
helo=mail-qk1-x733.google.com)
by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
(Exim 4.90_1) (envelope-from )
id 1nBSQk-0006GH-Nm
for axiom-developer@nongnu.org; Sat, 22 Jan 2022 21:16:42 -0500
Received: by mail-qk1-x733.google.com with SMTP id g9so9394696qka.4
for ; Sat, 22 Jan 2022 18:16:33 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112;
h=mime-version:references:in-reply-to:from:date:message-id:subject:to;
bh=vWBcuOGwB6uI53XDaQ3GU4oN5siZ3pSA4EXTHYAZ8aU=;
b=gDzU87+sAbKagdhn1yrf71GYfu6611cAwhjezdH5JSAYFZVaIQGDK7GCxIJKCI40FA
yGofDrcBxHQ8/7Pi7dgKxDXWRIMd6G3DvAeG1LL3Ef6kD20QCPwpshRUThyxZycegKZW
QzNWCB9CUZhtSpVtmPpMgJZdW8Rl2cXEJMmh4DNNxyTgOxlF5IpwU5zbak6Yy5Vcd11F
CCU2Pdi/rpj5If2SRwkki636BGAgm9ShfFAJW2Gw8Kmv+/uqpUGFQ4qGesPEIo0y6Z6h
VmPBjO5C7p39tQ7tLDOF9qTwFLnvJzZgOIY/6KdjXeBEdFGDJOxAl9berjp3kIMvacyD
bQ3g==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=1e100.net; s=20210112;
h=x-gm-message-state:mime-version:references:in-reply-to:from:date
:message-id:subject:to;
bh=vWBcuOGwB6uI53XDaQ3GU4oN5siZ3pSA4EXTHYAZ8aU=;
b=flqVvPE+dJEbexVx9hppKmGSb0cTSY/c0TWXepTQ5PpczTlMHfNtE9tKAkVI9pZZS4
+QWUgsuzcvNI2mk4Hw5zmBSuEi/Cbj2Uvm1BE5qb71PFHmlEvP8kgy4fQ09mUJJG0VCg
VgMc99drHGmcSI6wLC1f7hVomAwYKzjNgGRSZNR/Mc9QYsXk4TGheAaGVDqehf7P0fXj
gThZQj2drwCNJ8o2RHFw6OY+DUpg8GKTTsOlu4k5NGCfgJvHxVcUESRH9cJt6JErpnFJ
htWMLQq73XelHZyqv92jk74iIe7iLQIZGNxAN0J3oNKObeGmzrgYuuVECI/igNaTTESm
VZ/A==
X-Gm-Message-State: AOAM5304+VodyjzDJ2+HjRSc2gDvUeTeQ+QfNUZ7Cwk2+dwMMvBtaSUJ
0hHftgDgM10Ino3E2qG38lR2/AcrZd3V0Rfm/Dyg90H64W/MNQ==
X-Google-Smtp-Source: ABdhPJxQVgfLw8lBL7o5WSGhwMCkH5nR16IQYxo9TM1vziigIVabIIc3BpbNrA9PD3LFMaww2e5YUnGDESU9jo+Yo/o=
X-Received: by 2002:a05:620a:2a08:: with SMTP id
o8mr7353711qkp.643.1642904190846;
Sat, 22 Jan 2022 18:16:30 -0800 (PST)
MIME-Version: 1.0
References:
<1601071096648.17321@ccny.cuny.edu>
<20200928114929.GA1113@math.uni.wroc.pl>
<1607842080069.93596@ccny.cuny.edu> <1607845528644.76141@ccny.cuny.edu>
In-Reply-To:
From: Tim Daly
Date: Sat, 22 Jan 2022 21:16:18 -0500
Message-ID:
Subject: Re: Axiom musings...
To: axiom-dev , Tim Daly
Content-Type: multipart/alternative; boundary="000000000000b20b2205d63670f9"
X-Host-Lookup-Failed: Reverse DNS lookup failed for 2607:f8b0:4864:20::733
(failed)
Received-SPF: pass client-ip=2607:f8b0:4864:20::733;
envelope-from=axiomcas@gmail.com; helo=mail-qk1-x733.google.com
X-Spam_score_int: 7
X-Spam_score: 0.7
X-Spam_bar: /
X-Spam_report: (0.7 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1,
DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, FREEMAIL_FROM=0.001,
HTML_MESSAGE=0.001, PDS_HP_HELO_NORDNS=0.001, RDNS_NONE=0.793,
SPF_HELO_NONE=0.001, SPF_PASS=-0.001,
URI_DOTEDU=1.997 autolearn=no autolearn_force=no
X-Spam_action: no action
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.29
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Sun, 23 Jan 2022 02:16:44 -0000
--000000000000b20b2205d63670f9
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
I can't stress enough how important it is to listen to Hamming's talk
https://www.youtube.com/watch?v=3Da1zDuOPkMSw
Axiom will begin to die the day I stop working on it.
However, proving Axiom correct "down to the metal", is fundamental.
It will merge computer algebra and logic, spawning years of new
research.
Work on fundamental problems.
Tim
On Thu, Dec 30, 2021 at 6:46 PM Tim Daly wrote:
> One of the interesting questions when obtaining a result
> is "what functions were called and what was their return value?"
> Otherwise known as the "show your work" idea.
>
> There is an idea called the "writer monad" [0], usually
> implemented to facilitate logging. We can exploit this
> idea to provide "show your work" capability. Each function
> can provide this information inside the monad enabling the
> question to be answered at any time.
>
> For those unfamiliar with the monad idea, the best explanation
> I've found is this video [1].
>
> Tim
>
> [0] Deriving the writer monad from first principles
> https://williamyaoh.com/posts/2020-07-26-deriving-writer-monad.html
>
> [1] The Absolute Best Intro to Monads for Software Engineers
> https://www.youtube.com/watch?v=3DC2w45qRc3aU
>
> On Mon, Dec 13, 2021 at 12:30 AM Tim Daly wrote:
>
>> ...(snip)...
>>
>> Common Lisp has an "open compiler". That allows the ability
>> to deeply modify compiler behavior using compiler macros
>> and macros in general. CLOS takes advantage of this to add
>> typed behavior into the compiler in a way that ALLOWS strict
>> typing such as found in constructive type theory and ML.
>> Judgments, ala Crary, are front-and-center.
>>
>> Whether you USE the discipline afforded is the real question.
>>
>> Indeed, the Axiom research struggle is essentially one of how
>> to have a disciplined use of first-class dependent types. The
>> struggle raises issues of, for example, compiling a dependent
>> type whose argument is recursive in the compiled type. Since
>> the new type is first-class it can be constructed at what you
>> improperly call "run-time". However, it appears that the recursive
>> type may have to call the compiler at each recursion to generate
>> the next step since in some cases it cannot generate "closed code".
>>
>> I am embedding proofs (in LEAN language) into the type
>> hierarchy so that theorems, which depend on the type hierarchy,
>> are correctly inherited. The compiler has to check the proofs of functio=
ns
>> at compile time using these. Hacking up nonsense just won't cut it. Thin=
k
>> of the problem of embedding LEAN proofs in ML or ML in LEAN.
>> (Actually, Jeremy Avigad might find that research interesting.)
>>
>> So Matrix(3,3,Float) has inverses (assuming Float is a
>> field (cough)). The type inherits this theorem and proofs of
>> functions can use this. But Matrix(3,4,Integer) does not have
>> inverses so the proofs cannot use this. The type hierarchy has
>> to ensure that the proper theorems get inherited.
>>
>> Making proof technology work at compile time is hard.
>> (Worse yet, LEAN is a moving target. Sigh.)
>>
>>
>>
>> On Thu, Nov 25, 2021 at 9:43 AM Tim Daly wrote:
>>
>>>
>>> As you know I've been re-architecting Axiom to use first class
>>> dependent types and proving the algorithms correct. For example,
>>> the GCD of natural numbers or the GCD of polynomials.
>>>
>>> The idea involves "boxing up" the proof with the algorithm (aka
>>> proof carrying code) in the ELF file (under a crypto hash so it
>>> can't be changed).
>>>
>>> Once the code is running on the CPU, the proof is run in parallel
>>> on the field programmable gate array (FPGA). Intel data center
>>> servers have CPUs with built-in FPGAs these days.
>>>
>>> There is a bit of a disconnect, though. The GCD code is compiled
>>> machine code but the proof is LEAN-level.
>>>
>>> What would be ideal is if the compiler not only compiled the GCD
>>> code to machine code, it also compiled the proof to "machine code".
>>> That is, for each machine instruction, the FPGA proof checker
>>> would ensure that the proof was not violated at the individual
>>> instruction level.
>>>
>>> What does it mean to "compile a proof to the machine code level"?
>>>
>>> The Milawa effort (Myre14.pdf) does incremental proofs in layers.
>>> To quote from the article [0]:
>>>
>>> We begin with a simple proof checker, call it A, which is short
>>> enough to verify by the ``social process'' of mathematics -- and
>>> more recently with a theorem prover for a more expressive logic.
>>>
>>> We then develop a series of increasingly powerful proof checkers,
>>> call the B, C, D, and so on. We show each of these programs only
>>> accepts the same formulas as A, using A to verify B, and B to verify
>>> C, and so on. Then, since we trust A, and A says B is trustworthy, w=
e
>>> can trust B. Then, since we trust B, and B says C is trustworthy, we
>>> can trust C.
>>>
>>> This gives a technique for "compiling the proof" down the the machine
>>> code level. Ideally, the compiler would have judgments for each step of
>>> the compilation so that each compile step has a justification. I don't
>>> know of any compiler that does this yet. (References welcome).
>>>
>>> At the machine code level, there are techniques that would allow
>>> the FPGA proof to "step in sequence" with the executing code.
>>> Some work has been done on using "Hoare Logic for Realistically
>>> Modelled Machine Code" (paper attached, Myre07a.pdf),
>>> "Decompilation into Logic -- Improved (Myre12a.pdf).
>>>
>>> So the game is to construct a GCD over some type (Nats, Polys, etc.
>>> Axiom has 22), compile the dependent type GCD to machine code.
>>> In parallel, the proof of the code is compiled to machine code. The
>>> pair is sent to the CPU/FPGA and, while the algorithm runs, the FPGA
>>> ensures the proof is not violated, instruction by instruction.
>>>
>>> (I'm ignoring machine architecture issues such pipelining, out-of-order=
,
>>> branch prediction, and other machine-level things to ponder. I'm lookin=
g
>>> at the RISC-V Verilog details by various people to understand better bu=
t
>>> it is still a "misty fog" for me.)
>>>
>>> The result is proven code "down to the metal".
>>>
>>> Tim
>>>
>>>
>>>
>>> [0]
>>> https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index=
-seo.php/ACL2____MILAWA
>>>
>>> On Thu, Nov 25, 2021 at 6:05 AM Tim Daly wrote:
>>>
>>>>
>>>> As you know I've been re-architecting Axiom to use first class
>>>> dependent types and proving the algorithms correct. For example,
>>>> the GCD of natural numbers or the GCD of polynomials.
>>>>
>>>> The idea involves "boxing up" the proof with the algorithm (aka
>>>> proof carrying code) in the ELF file (under a crypto hash so it
>>>> can't be changed).
>>>>
>>>> Once the code is running on the CPU, the proof is run in parallel
>>>> on the field programmable gate array (FPGA). Intel data center
>>>> servers have CPUs with built-in FPGAs these days.
>>>>
>>>> There is a bit of a disconnect, though. The GCD code is compiled
>>>> machine code but the proof is LEAN-level.
>>>>
>>>> What would be ideal is if the compiler not only compiled the GCD
>>>> code to machine code, it also compiled the proof to "machine code".
>>>> That is, for each machine instruction, the FPGA proof checker
>>>> would ensure that the proof was not violated at the individual
>>>> instruction level.
>>>>
>>>> What does it mean to "compile a proof to the machine code level"?
>>>>
>>>> The Milawa effort (Myre14.pdf) does incremental proofs in layers.
>>>> To quote from the article [0]:
>>>>
>>>> We begin with a simple proof checker, call it A, which is short
>>>> enough to verify by the ``social process'' of mathematics -- and
>>>> more recently with a theorem prover for a more expressive logic.
>>>>
>>>> We then develop a series of increasingly powerful proof checkers,
>>>> call the B, C, D, and so on. We show each of these programs only
>>>> accepts the same formulas as A, using A to verify B, and B to verif=
y
>>>> C, and so on. Then, since we trust A, and A says B is trustworthy, =
we
>>>> can trust B. Then, since we trust B, and B says C is trustworthy, w=
e
>>>> can trust C.
>>>>
>>>> This gives a technique for "compiling the proof" down the the machine
>>>> code level. Ideally, the compiler would have judgments for each step o=
f
>>>> the compilation so that each compile step has a justification. I don't
>>>> know of any compiler that does this yet. (References welcome).
>>>>
>>>> At the machine code level, there are techniques that would allow
>>>> the FPGA proof to "step in sequence" with the executing code.
>>>> Some work has been done on using "Hoare Logic for Realistically
>>>> Modelled Machine Code" (paper attached, Myre07a.pdf),
>>>> "Decompilation into Logic -- Improved (Myre12a.pdf).
>>>>
>>>> So the game is to construct a GCD over some type (Nats, Polys, etc.
>>>> Axiom has 22), compile the dependent type GCD to machine code.
>>>> In parallel, the proof of the code is compiled to machine code. The
>>>> pair is sent to the CPU/FPGA and, while the algorithm runs, the FPGA
>>>> ensures the proof is not violated, instruction by instruction.
>>>>
>>>> (I'm ignoring machine architecture issues such pipelining, out-of-orde=
r,
>>>> branch prediction, and other machine-level things to ponder. I'm looki=
ng
>>>> at the RISC-V Verilog details by various people to understand better b=
ut
>>>> it is still a "misty fog" for me.)
>>>>
>>>> The result is proven code "down to the metal".
>>>>
>>>> Tim
>>>>
>>>>
>>>>
>>>> [0]
>>>> https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/inde=
x-seo.php/ACL2____MILAWA
>>>>
>>>> On Sat, Nov 13, 2021 at 5:28 PM Tim Daly wrote:
>>>>
>>>>> Full support for general, first-class dependent types requires
>>>>> some changes to the Axiom design. That implies some language
>>>>> design questions.
>>>>>
>>>>> Given that mathematics is such a general subject with a lot of
>>>>> "local" notation and ideas (witness logical judgment notation)
>>>>> careful thought is needed to design a language that is able to
>>>>> handle a wide range.
>>>>>
>>>>> Normally language design is a two-level process. The language
>>>>> designer creates a language and then an implementation. Various
>>>>> design choices affect the final language.
>>>>>
>>>>> There is "The Metaobject Protocol" (MOP)
>>>>>
>>>>> https://www.amazon.com/Art-Metaobject-Protocol-Gregor-Kiczales/dp/026=
2610744
>>>>> which encourages a three-level process. The language designer
>>>>> works at a Metalevel to design a family of languages, then the
>>>>> language specializations, then the implementation. A MOP design
>>>>> allows the language user to optimize the language to their problem.
>>>>>
>>>>> A simple paper on the subject is "Metaobject Protocols"
>>>>> https://users.cs.duke.edu/~vahdat/ps/mop.pdf
>>>>>
>>>>> Tim
>>>>>
>>>>>
>>>>> On Mon, Oct 25, 2021 at 7:42 PM Tim Daly wrote:
>>>>>
>>>>>> I have a separate thread of research on Self-Replicating Systems
>>>>>> (ref: Kinematics of Self Reproducing Machines
>>>>>> http://www.molecularassembler.com/KSRM.htm)
>>>>>>
>>>>>> which led to watching "Strange Dreams of Stranger Loops" by Will Byr=
d
>>>>>> https://www.youtube.com/watch?v=3DAffW-7ika0E
>>>>>>
>>>>>> Will referenced a PhD Thesis by Jon Doyle
>>>>>> "A Model for Deliberation, Action, and Introspection"
>>>>>>
>>>>>> I also read the thesis by J.C.G. Sturdy
>>>>>> "A Lisp through the Looking Glass"
>>>>>>
>>>>>> Self-replication requires the ability to manipulate your own
>>>>>> representation in such a way that changes to that representation
>>>>>> will change behavior.
>>>>>>
>>>>>> This leads to two thoughts in the SANE research.
>>>>>>
>>>>>> First, "Declarative Representation". That is, most of the things
>>>>>> about the representation should be declarative rather than
>>>>>> procedural. Applying this idea as much as possible makes it
>>>>>> easier to understand and manipulate.
>>>>>>
>>>>>> Second, "Explicit Call Stack". Function calls form an implicit
>>>>>> call stack. This can usually be displayed in a running lisp system.
>>>>>> However, having the call stack explicitly available would mean
>>>>>> that a system could "introspect" at the first-class level.
>>>>>>
>>>>>> These two ideas would make it easy, for example, to let the
>>>>>> system "show the work". One of the normal complaints is that
>>>>>> a system presents an answer but there is no way to know how
>>>>>> that answer was derived. These two ideas make it possible to
>>>>>> understand, display, and even post-answer manipulate
>>>>>> the intermediate steps.
>>>>>>
>>>>>> Having the intermediate steps also allows proofs to be
>>>>>> inserted in a step-by-step fashion. This aids the effort to
>>>>>> have proofs run in parallel with computation at the hardware
>>>>>> level.
>>>>>>
>>>>>> Tim
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>>> On Thu, Oct 21, 2021 at 9:50 AM Tim Daly wrote:
>>>>>>
>>>>>>> So the current struggle involves the categories in Axiom.
>>>>>>>
>>>>>>> The categories and domains constructed using categories
>>>>>>> are dependent types. When are dependent types "equal"?
>>>>>>> Well, hummmm, that depends on the arguments to the
>>>>>>> constructor.
>>>>>>>
>>>>>>> But in order to decide(?) equality we have to evaluate
>>>>>>> the arguments (which themselves can be dependent types).
>>>>>>> Indeed, we may, and in general, we must evaluate the
>>>>>>> arguments at compile time (well, "construction time" as
>>>>>>> there isn't really a compiler / interpreter separation anymore.)
>>>>>>>
>>>>>>> That raises the question of what "equality" means. This
>>>>>>> is not simply a "set equality" relation. It falls into the
>>>>>>> infinite-groupoid of homotopy type theory. In general
>>>>>>> it appears that deciding category / domain equivalence
>>>>>>> might force us to climb the type hierarchy.
>>>>>>>
>>>>>>> Beyond that, there is the question of "which proof"
>>>>>>> applies to the resulting object. Proofs depend on their
>>>>>>> assumptions which might be different for different
>>>>>>> constructions. As yet I have no clue how to "index"
>>>>>>> proofs based on their assumptions, nor how to
>>>>>>> connect these assumptions to the groupoid structure.
>>>>>>>
>>>>>>> My brain hurts.
>>>>>>>
>>>>>>> Tim
>>>>>>>
>>>>>>>
>>>>>>> On Mon, Oct 18, 2021 at 2:00 AM Tim Daly wrote=
:
>>>>>>>
>>>>>>>> "Birthing Computational Mathematics"
>>>>>>>>
>>>>>>>> The Axiom SANE project is difficult at a very fundamental
>>>>>>>> level. The title "SANE" was chosen due to the various
>>>>>>>> words found in a thesuarus... "rational", "coherent",
>>>>>>>> "judicious" and "sound".
>>>>>>>>
>>>>>>>> These are very high level, amorphous ideas. But so is
>>>>>>>> the design of SANE. Breaking away from tradition in
>>>>>>>> computer algebra, type theory, and proof assistants
>>>>>>>> is very difficult. Ideas tend to fall into standard jargon
>>>>>>>> which limits both the frame of thinking (e.g. dependent
>>>>>>>> types) and the content (e.g. notation).
>>>>>>>>
>>>>>>>> Questioning both frame and content is very difficult.
>>>>>>>> It is hard to even recognize when they are accepted
>>>>>>>> "by default" rather than "by choice". What does the idea
>>>>>>>> "power tools" mean in a primitive, hand labor culture?
>>>>>>>>
>>>>>>>> Christopher Alexander [0] addresses this problem in
>>>>>>>> a lot of his writing. Specifically, in his book "Notes on
>>>>>>>> the Synthesis of Form", in his chapter 5 "The Selfconsious
>>>>>>>> Process", he addresses this problem directly. This is a
>>>>>>>> "must read" book.
>>>>>>>>
>>>>>>>> Unlike building design and contruction, however, there
>>>>>>>> are almost no constraints to use as guides. Alexander
>>>>>>>> quotes Plato's Phaedrus:
>>>>>>>>
>>>>>>>> "First, the taking in of scattered particulars under
>>>>>>>> one Idea, so that everyone understands what is being
>>>>>>>> talked about ... Second, the separation of the Idea
>>>>>>>> into parts, by dividing it at the joints, as nature
>>>>>>>> directs, not breaking any limb in half as a bad
>>>>>>>> carver might."
>>>>>>>>
>>>>>>>> Lisp, which has been called "clay for the mind" can
>>>>>>>> build virtually anything that can be thought. The
>>>>>>>> "joints" are also "of one's choosing" so one is
>>>>>>>> both carver and "nature".
>>>>>>>>
>>>>>>>> Clearly the problem is no longer "the tools".
>>>>>>>> *I* am the problem constraining the solution.
>>>>>>>> Birthing this "new thing" is slow, difficult, and
>>>>>>>> uncertain at best.
>>>>>>>>
>>>>>>>> Tim
>>>>>>>>
>>>>>>>> [0] Alexander, Christopher "Notes on the Synthesis
>>>>>>>> of Form" Harvard University Press 1964
>>>>>>>> ISBN 0-674-62751-2
>>>>>>>>
>>>>>>>>
>>>>>>>> On Sun, Oct 10, 2021 at 4:40 PM Tim Daly
>>>>>>>> wrote:
>>>>>>>>
>>>>>>>>> Re: writing a paper... I'm not connected to Academia
>>>>>>>>> so anything I'd write would never make it into print.
>>>>>>>>>
>>>>>>>>> "Language level parsing" is still a long way off. The talk
>>>>>>>>> by Guy Steele [2] highlights some of the problems we
>>>>>>>>> currently face using mathematical metanotation.
>>>>>>>>>
>>>>>>>>> For example, a professor I know at CCNY (City College
>>>>>>>>> of New York) didn't understand Platzer's "funny
>>>>>>>>> fraction notation" (proof judgements) despite being
>>>>>>>>> an expert in Platzer's differential equations area.
>>>>>>>>>
>>>>>>>>> Notation matters and is not widely common.
>>>>>>>>>
>>>>>>>>> I spoke to Professor Black (in LTI) about using natural
>>>>>>>>> language in the limited task of a human-robot cooperation
>>>>>>>>> in changing a car tire. I looked at the current machine
>>>>>>>>> learning efforts. They are no where near anything but
>>>>>>>>> toy systems, taking too long to train and are too fragile.
>>>>>>>>>
>>>>>>>>> Instead I ended up using a combination of AIML [3]
>>>>>>>>> (Artificial Intelligence Markup Language), the ALICE
>>>>>>>>> Chatbot [4], Forgy's OPS5 rule based program [5],
>>>>>>>>> and Fahlman's SCONE [6] knowledge base. It was
>>>>>>>>> much less fragile in my limited domain problem.
>>>>>>>>>
>>>>>>>>> I have no idea how to extend any system to deal with
>>>>>>>>> even undergraduate mathematics parsing.
>>>>>>>>>
>>>>>>>>> Nor do I have any idea how I would embed LEAN
>>>>>>>>> knowledge into a SCONE database, although I
>>>>>>>>> think the combination would be useful and interesting.
>>>>>>>>>
>>>>>>>>> I do believe that, in the limited area of computational
>>>>>>>>> mathematics, we are capable of building robust, proven
>>>>>>>>> systems that are quite general and extensible. As you
>>>>>>>>> might have guessed I've given it a lot of thought over
>>>>>>>>> the years :-)
>>>>>>>>>
>>>>>>>>> A mathematical language seems to need >6 components
>>>>>>>>>
>>>>>>>>> 1) We need some sort of a specification language, possibly
>>>>>>>>> somewhat 'propositional' that introduces the assumptions
>>>>>>>>> you mentioned (ref. your discussion of numbers being
>>>>>>>>> abstract and ref. your discussion of relevant choice of
>>>>>>>>> assumptions related to a problem).
>>>>>>>>>
>>>>>>>>> This is starting to show up in the hardware area (e.g.
>>>>>>>>> Lamport's TLC[0])
>>>>>>>>>
>>>>>>>>> Of course, specifications relate to proving programs
>>>>>>>>> and, as you recall, I got a cold reception from the
>>>>>>>>> LEAN community about using LEAN for program proofs.
>>>>>>>>>
>>>>>>>>> 2) We need "scaffolding". That is, we need a theory
>>>>>>>>> that can be reduced to some implementable form
>>>>>>>>> that provides concept-level structure.
>>>>>>>>>
>>>>>>>>> Axiom uses group theory for this. Axiom's "category"
>>>>>>>>> structure has "Category" things like Ring. Claiming
>>>>>>>>> to be a Ring brings in a lot of "Signatures" of functions
>>>>>>>>> you have to implement to properly be a Ring.
>>>>>>>>>
>>>>>>>>> Scaffolding provides a firm mathematical basis for
>>>>>>>>> design. It provides a link between the concept of a
>>>>>>>>> Ring and the expectations you can assume when
>>>>>>>>> you claim your "Domain" "is a Ring". Category
>>>>>>>>> theory might provide similar structural scaffolding
>>>>>>>>> (eventually... I'm still working on that thought garden)
>>>>>>>>>
>>>>>>>>> LEAN ought to have a textbook(s?) that structures
>>>>>>>>> the world around some form of mathematics. It isn't
>>>>>>>>> sufficient to say "undergraduate math" is the goal.
>>>>>>>>> There needs to be some coherent organization so
>>>>>>>>> people can bring ideas like Group Theory to the
>>>>>>>>> organization. Which brings me to ...
>>>>>>>>>
>>>>>>>>> 3) We need "spreading". That is, we need to take
>>>>>>>>> the various definitions and theorems in LEAN and
>>>>>>>>> place them in their proper place in the scaffold.
>>>>>>>>>
>>>>>>>>> For example, the Ring category needs the definitions
>>>>>>>>> and theorems for a Ring included in the code for the
>>>>>>>>> Ring category. Similarly, the Commutative category
>>>>>>>>> needs the definitions and theorems that underlie
>>>>>>>>> "commutative" included in the code.
>>>>>>>>>
>>>>>>>>> That way, when you claim to be a "Commutative Ring"
>>>>>>>>> you get both sets of definitions and theorems. That is,
>>>>>>>>> the inheritance mechanism will collect up all of the
>>>>>>>>> definitions and theorems and make them available
>>>>>>>>> for proofs.
>>>>>>>>>
>>>>>>>>> I am looking at LEAN's definitions and theorems with
>>>>>>>>> an eye to "spreading" them into the group scaffold of
>>>>>>>>> Axiom.
>>>>>>>>>
>>>>>>>>> 4) We need "carriers" (Axiom calls them representations,
>>>>>>>>> aka "REP"). REPs allow data structures to be defined
>>>>>>>>> independent of the implementation.
>>>>>>>>>
>>>>>>>>> For example, Axiom can construct Polynomials that
>>>>>>>>> have their coefficients in various forms of representation.
>>>>>>>>> You can define "dense" (all coefficients in a list),
>>>>>>>>> "sparse" (only non-zero coefficients), "recursive", etc.
>>>>>>>>>
>>>>>>>>> A "dense polynomial" and a "sparse polynomial" work
>>>>>>>>> exactly the same way as far as the user is concerned.
>>>>>>>>> They both implement the same set of functions. There
>>>>>>>>> is only a difference of representation for efficiency and
>>>>>>>>> this only affects the implementation of the functions,
>>>>>>>>> not their use.
>>>>>>>>>
>>>>>>>>> Axiom "got this wrong" because it didn't sufficiently
>>>>>>>>> separate the REP from the "Domain". I plan to fix this.
>>>>>>>>>
>>>>>>>>> LEAN ought to have a "data structures" subtree that
>>>>>>>>> has all of the definitions and axioms for all of the
>>>>>>>>> existing data structures (e.g. Red-Black trees). This
>>>>>>>>> would be a good undergraduate project.
>>>>>>>>>
>>>>>>>>> 5) We need "Domains" (in Axiom speak). That is, we
>>>>>>>>> need a box that holds all of the functions that implement
>>>>>>>>> a "Domain". For example, a "Polynomial Domain" would
>>>>>>>>> hold all of the functions for manipulating polynomials
>>>>>>>>> (e.g polynomial multiplication). The "Domain" box
>>>>>>>>> is a dependent type that:
>>>>>>>>>
>>>>>>>>> A) has an argument list of "Categories" that this "Domain"
>>>>>>>>> box inherits. Thus, the "Integer Domain" inherits
>>>>>>>>> the definitions and axioms from "Commutative"
>>>>>>>>>
>>>>>>>>> Functions in the "Domain" box can now assume
>>>>>>>>> and use the properties of being commutative. Proofs
>>>>>>>>> of functions in this domain can use the definitions
>>>>>>>>> and proofs about being commutative.
>>>>>>>>>
>>>>>>>>> B) contains an argument that specifies the "REP"
>>>>>>>>> (aka, the carrier). That way you get all of the
>>>>>>>>> functions associated with the data structure
>>>>>>>>> available for use in the implementation.
>>>>>>>>>
>>>>>>>>> Functions in the Domain box can use all of
>>>>>>>>> the definitions and axioms about the representation
>>>>>>>>> (e.g. NonNegativeIntegers are always positive)
>>>>>>>>>
>>>>>>>>> C) contains local "spread" definitions and axioms
>>>>>>>>> that can be used in function proofs.
>>>>>>>>>
>>>>>>>>> For example, a "Square Matrix" domain would
>>>>>>>>> have local axioms that state that the matrix is
>>>>>>>>> always square. Thus, functions in that box could
>>>>>>>>> use these additional definitions and axioms in
>>>>>>>>> function proofs.
>>>>>>>>>
>>>>>>>>> D) contains local state. A "Square Matrix" domain
>>>>>>>>> would be constructed as a dependent type that
>>>>>>>>> specified the size of the square (e.g. a 2x2
>>>>>>>>> matrix would have '2' as a dependent parameter.
>>>>>>>>>
>>>>>>>>> E) contains implementations of inherited functions.
>>>>>>>>>
>>>>>>>>> A "Category" could have a signature for a GCD
>>>>>>>>> function and the "Category" could have a default
>>>>>>>>> implementation. However, the "Domain" could
>>>>>>>>> have a locally more efficient implementation which
>>>>>>>>> overrides the inherited implementation.
>>>>>>>>>
>>>>>>>>> Axiom has about 20 GCD implementations that
>>>>>>>>> differ locally from the default in the category. They
>>>>>>>>> use properties known locally to be more efficient.
>>>>>>>>>
>>>>>>>>> F) contains local function signatures.
>>>>>>>>>
>>>>>>>>> A "Domain" gives the user more and more unique
>>>>>>>>> functions. The signature have associated
>>>>>>>>> "pre- and post- conditions" that can be used
>>>>>>>>> as assumptions in the function proofs.
>>>>>>>>>
>>>>>>>>> Some of the user-available functions are only
>>>>>>>>> visible if the dependent type would allow them
>>>>>>>>> to exist. For example, a general Matrix domain
>>>>>>>>> would have fewer user functions that a Square
>>>>>>>>> Matrix domain.
>>>>>>>>>
>>>>>>>>> In addition, local "helper" functions need their
>>>>>>>>> own signatures that are not user visible.
>>>>>>>>>
>>>>>>>>> G) the function implementation for each signature.
>>>>>>>>>
>>>>>>>>> This is obviously where all the magic happens
>>>>>>>>>
>>>>>>>>> H) the proof of each function.
>>>>>>>>>
>>>>>>>>> This is where I'm using LEAN.
>>>>>>>>>
>>>>>>>>> Every function has a proof. That proof can use
>>>>>>>>> all of the definitions and axioms inherited from
>>>>>>>>> the "Category", "Representation", the "Domain
>>>>>>>>> Local", and the signature pre- and post-
>>>>>>>>> conditions.
>>>>>>>>>
>>>>>>>>> I) literature links. Algorithms must contain a link
>>>>>>>>> to at least one literature reference. Of course,
>>>>>>>>> since everything I do is a Literate Program
>>>>>>>>> this is obviously required. Knuth said so :-)
>>>>>>>>>
>>>>>>>>>
>>>>>>>>> LEAN ought to have "books" or "pamphlets" that
>>>>>>>>> bring together all of this information for a domain
>>>>>>>>> such as Square Matrices. That way a user can
>>>>>>>>> find all of the related ideas, available functions,
>>>>>>>>> and their corresponding proofs in one place.
>>>>>>>>>
>>>>>>>>> 6) User level presentation.
>>>>>>>>>
>>>>>>>>> This is where the systems can differ significantly.
>>>>>>>>> Axiom and LEAN both have GCD but they use
>>>>>>>>> that for different purposes.
>>>>>>>>>
>>>>>>>>> I'm trying to connect LEAN's GCD and Axiom's GCD
>>>>>>>>> so there is a "computational mathematics" idea that
>>>>>>>>> allows the user to connect proofs and implementations.
>>>>>>>>>
>>>>>>>>> 7) Trust
>>>>>>>>>
>>>>>>>>> Unlike everything else, computational mathematics
>>>>>>>>> can have proven code that gives various guarantees.
>>>>>>>>>
>>>>>>>>> I have been working on this aspect for a while.
>>>>>>>>> I refer to it as trust "down to the metal" The idea is
>>>>>>>>> that a proof of the GCD function and the implementation
>>>>>>>>> of the GCD function get packaged into the ELF format.
>>>>>>>>> (proof carrying code). When the GCD algorithm executes
>>>>>>>>> on the CPU, the GCD proof is run through the LEAN
>>>>>>>>> proof checker on an FPGA in parallel.
>>>>>>>>>
>>>>>>>>> (I just recently got a PYNQ Xilinx board [1] with a CPU
>>>>>>>>> and FPGA together. I'm trying to implement the LEAN
>>>>>>>>> proof checker on the FPGA).
>>>>>>>>>
>>>>>>>>> We are on the cusp of a revolution in computational
>>>>>>>>> mathematics. But the two pillars (proof and computer
>>>>>>>>> algebra) need to get know each other.
>>>>>>>>>
>>>>>>>>> Tim
>>>>>>>>>
>>>>>>>>>
>>>>>>>>>
>>>>>>>>> [0] Lamport, Leslie "Chapter on TLA+"
>>>>>>>>> in "Software Specification Methods"
>>>>>>>>> https://www.springer.com/gp/book/9781852333539
>>>>>>>>> (I no longer have CMU library access or I'd send you
>>>>>>>>> the book PDF)
>>>>>>>>>
>>>>>>>>> [1] https://www.tul.com.tw/productspynq-z2.html
>>>>>>>>>
>>>>>>>>> [2] https://www.youtube.com/watch?v=3DdCuZkaaou0Q
>>>>>>>>>
>>>>>>>>> [3] "ARTIFICIAL INTELLIGENCE MARKUP LANGUAGE"
>>>>>>>>> https://arxiv.org/pdf/1307.3091.pdf
>>>>>>>>>
>>>>>>>>> [4] ALICE Chatbot
>>>>>>>>>
>>>>>>>>> http://www.scielo.org.mx/pdf/cys/v19n4/1405-5546-cys-19-04-00625.=
pdf
>>>>>>>>>
>>>>>>>>> [5] OPS5 User Manual
>>>>>>>>>
>>>>>>>>> https://kilthub.cmu.edu/articles/journal_contribution/OPS5_user_s=
_manual/6608090/1
>>>>>>>>>
>>>>>>>>> [6] Scott Fahlman "SCONE"
>>>>>>>>> http://www.cs.cmu.edu/~sef/scone/
>>>>>>>>>
>>>>>>>>> On 9/27/21, Tim Daly wrote:
>>>>>>>>> > I have tried to maintain a list of names of people who have
>>>>>>>>> > helped Axiom, going all the way back to the pre-Scratchpad
>>>>>>>>> > days. The names are listed at the beginning of each book.
>>>>>>>>> > I also maintain a bibliography of publications I've read or
>>>>>>>>> > that have had an indirect influence on Axiom.
>>>>>>>>> >
>>>>>>>>> > Credit is "the coin of the realm". It is easy to share and wron=
g
>>>>>>>>> > to ignore. It is especially damaging to those in Academia who
>>>>>>>>> > are affected by credit and citations in publications.
>>>>>>>>> >
>>>>>>>>> > Apparently I'm not the only person who feels that way. The ACM
>>>>>>>>> > Turing award seems to have ignored a lot of work:
>>>>>>>>> >
>>>>>>>>> > Scientific Integrity, the 2021 Turing Lecture, and the 2018
>>>>>>>>> Turing
>>>>>>>>> > Award for Deep Learning
>>>>>>>>> >
>>>>>>>>> https://people.idsia.ch/~juergen/scientific-integrity-turing-awar=
d-deep-learning.html
>>>>>>>>> >
>>>>>>>>> > I worked on an AI problem at IBM Research called Ketazolam.
>>>>>>>>> > (https://en.wikipedia.org/wiki/Ketazolam). The idea was to
>>>>>>>>> recognize
>>>>>>>>> > and associated 3D chemical drawings with their drug counterpart=
s.
>>>>>>>>> > I used Rumelhart, and McClelland's books. These books contained
>>>>>>>>> > quite a few ideas that seem to be "new and innovative" among th=
e
>>>>>>>>> > machine learning crowd... but the books are from 1987. I don't
>>>>>>>>> believe
>>>>>>>>> > I've seen these books mentioned in any recent bibliography.
>>>>>>>>> >
>>>>>>>>> https://mitpress.mit.edu/books/parallel-distributed-processing-vo=
lume-1
>>>>>>>>> >
>>>>>>>>> >
>>>>>>>>> >
>>>>>>>>> >
>>>>>>>>> > On 9/27/21, Tim Daly wrote:
>>>>>>>>> >> Greg Wilson asked "How Reliable is Scientific Software?"
>>>>>>>>> >>
>>>>>>>>> https://neverworkintheory.org/2021/09/25/how-reliable-is-scientif=
ic-software.html
>>>>>>>>> >>
>>>>>>>>> >> which is a really interesting read. For example"
>>>>>>>>> >>
>>>>>>>>> >> [Hatton1994], is now a quarter of a century old, but its
>>>>>>>>> conclusions
>>>>>>>>> >> are still fresh. The authors fed the same data into nine
>>>>>>>>> commercial
>>>>>>>>> >> geophysical software packages and compared the results; they
>>>>>>>>> found
>>>>>>>>> >> that, "numerical disagreement grows at around the rate of 1% i=
n
>>>>>>>>> >> average absolute difference per 4000 fines of implemented code=
,
>>>>>>>>> and,
>>>>>>>>> >> even worse, the nature of the disagreement is nonrandom" (i.e.=
,
>>>>>>>>> the
>>>>>>>>> >> authors of different packages make similar mistakes).
>>>>>>>>> >>
>>>>>>>>> >>
>>>>>>>>> >> On 9/26/21, Tim Daly wrote:
>>>>>>>>> >>> I should note that the lastest board I've just unboxed
>>>>>>>>> >>> (a PYNQ-Z2) is a Zynq Z-7020 chip from Xilinx (AMD).
>>>>>>>>> >>>
>>>>>>>>> >>> What makes it interesting is that it contains 2 hard
>>>>>>>>> >>> core processors and an FPGA, connected by 9 paths
>>>>>>>>> >>> for communication. The processors can be run
>>>>>>>>> >>> independently so there is the possibility of a parallel
>>>>>>>>> >>> version of some Axiom algorithms (assuming I had
>>>>>>>>> >>> the time, which I don't).
>>>>>>>>> >>>
>>>>>>>>> >>> Previously either the hard (physical) processor was
>>>>>>>>> >>> separate from the FPGA with minimal communication
>>>>>>>>> >>> or the soft core processor had to be created in the FPGA
>>>>>>>>> >>> and was much slower.
>>>>>>>>> >>>
>>>>>>>>> >>> Now the two have been combined in a single chip.
>>>>>>>>> >>> That means that my effort to run a proof checker on
>>>>>>>>> >>> the FPGA and the algorithm on the CPU just got to
>>>>>>>>> >>> the point where coordination is much easier.
>>>>>>>>> >>>
>>>>>>>>> >>> Now all I have to do is figure out how to program this
>>>>>>>>> >>> beast.
>>>>>>>>> >>>
>>>>>>>>> >>> There is no such thing as a simple job.
>>>>>>>>> >>>
>>>>>>>>> >>> Tim
>>>>>>>>> >>>
>>>>>>>>> >>>
>>>>>>>>> >>> On 9/26/21, Tim Daly wrote:
>>>>>>>>> >>>> I'm familiar with most of the traditional approaches
>>>>>>>>> >>>> like Theorema. The bibliography contains most of the
>>>>>>>>> >>>> more interesting sources. [0]
>>>>>>>>> >>>>
>>>>>>>>> >>>> There is a difference between traditional approaches to
>>>>>>>>> >>>> connecting computer algebra and proofs and my approach.
>>>>>>>>> >>>>
>>>>>>>>> >>>> Proving an algorithm, like the GCD, in Axiom is hard.
>>>>>>>>> >>>> There are many GCDs (e.g. NNI vs POLY) and there
>>>>>>>>> >>>> are theorems and proofs passed at runtime in the
>>>>>>>>> >>>> arguments of the newly constructed domains. This
>>>>>>>>> >>>> involves a lot of dependent type theory and issues of
>>>>>>>>> >>>> compile time / runtime argument evaluation. The issues
>>>>>>>>> >>>> that arise are difficult and still being debated in the type
>>>>>>>>> >>>> theory community.
>>>>>>>>> >>>>
>>>>>>>>> >>>> I am putting the definitions, theorems, and proofs (DTP)
>>>>>>>>> >>>> directly into the category/domain hierarchy. Each category
>>>>>>>>> >>>> will have the DTP specific to it. That way a commutative
>>>>>>>>> >>>> domain will inherit a commutative theorem and a
>>>>>>>>> >>>> non-commutative domain will not.
>>>>>>>>> >>>>
>>>>>>>>> >>>> Each domain will have additional DTPs associated with
>>>>>>>>> >>>> the domain (e.g. NNI vs Integer) as well as any DTPs
>>>>>>>>> >>>> it inherits from the category hierarchy. Functions in the
>>>>>>>>> >>>> domain will have associated DTPs.
>>>>>>>>> >>>>
>>>>>>>>> >>>> A function to be proven will then inherit all of the relevan=
t
>>>>>>>>> >>>> DTPs. The proof will be attached to the function and
>>>>>>>>> >>>> both will be sent to the hardware (proof-carrying code).
>>>>>>>>> >>>>
>>>>>>>>> >>>> The proof checker, running on a field programmable
>>>>>>>>> >>>> gate array (FPGA), will be checked at runtime in
>>>>>>>>> >>>> parallel with the algorithm running on the CPU
>>>>>>>>> >>>> (aka "trust down to the metal"). (Note that Intel
>>>>>>>>> >>>> and AMD have built CPU/FPGA combined chips,
>>>>>>>>> >>>> currently only available in the cloud.)
>>>>>>>>> >>>>
>>>>>>>>> >>>>
>>>>>>>>> >>>>
>>>>>>>>> >>>> I am (slowly) making progress on the research.
>>>>>>>>> >>>>
>>>>>>>>> >>>> I have the hardware and nearly have the proof
>>>>>>>>> >>>> checker from LEAN running on my FPGA.
>>>>>>>>> >>>>
>>>>>>>>> >>>> I'm in the process of spreading the DTPs from
>>>>>>>>> >>>> LEAN across the category/domain hierarchy.
>>>>>>>>> >>>>
>>>>>>>>> >>>> The current Axiom build extracts all of the functions
>>>>>>>>> >>>> but does not yet have the DTPs.
>>>>>>>>> >>>>
>>>>>>>>> >>>> I have to restructure the system, including the compiler
>>>>>>>>> >>>> and interpreter to parse and inherit the DTPs. I
>>>>>>>>> >>>> have some of that code but only some of the code
>>>>>>>>> >>>> has been pushed to the repository (volume 15) but
>>>>>>>>> >>>> that is rather trivial, out of date, and incomplete.
>>>>>>>>> >>>>
>>>>>>>>> >>>> I'm clearly not smart enough to prove the Risch
>>>>>>>>> >>>> algorithm and its associated machinery but the needed
>>>>>>>>> >>>> definitions and theorems will be available to someone
>>>>>>>>> >>>> who wants to try.
>>>>>>>>> >>>>
>>>>>>>>> >>>> [0] https://github.com/daly/PDFS/blob/master/bookvolbib.pdf
>>>>>>>>> >>>>
>>>>>>>>> >>>>
>>>>>>>>> >>>> On 8/19/21, Tim Daly wrote:
>>>>>>>>> >>>>> =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
>>>>>>>>> >>>>>
>>>>>>>>> >>>>> REVIEW (Axiom on WSL2 Windows)
>>>>>>>>> >>>>>
>>>>>>>>> >>>>>
>>>>>>>>> >>>>> So the steps to run Axiom from a Windows desktop
>>>>>>>>> >>>>>
>>>>>>>>> >>>>> 1 Windows) install XMing on Windows for X11 server
>>>>>>>>> >>>>>
>>>>>>>>> >>>>> http://www.straightrunning.com/XmingNotes/
>>>>>>>>> >>>>>
>>>>>>>>> >>>>> 2 WSL2) Install Axiom in WSL2
>>>>>>>>> >>>>>
>>>>>>>>> >>>>> sudo apt install axiom
>>>>>>>>> >>>>>
>>>>>>>>> >>>>> 3 WSL2) modify /usr/bin/axiom to fix the bug:
>>>>>>>>> >>>>> (someone changed the axiom startup script.
>>>>>>>>> >>>>> It won't work on WSL2. I don't know who or
>>>>>>>>> >>>>> how to get it fixed).
>>>>>>>>> >>>>>
>>>>>>>>> >>>>> sudo emacs /usr/bin/axiom
>>>>>>>>> >>>>>
>>>>>>>>> >>>>> (split the line into 3 and add quote marks)
>>>>>>>>> >>>>>
>>>>>>>>> >>>>> export SPADDEFAULT=3D/usr/local/axiom/mnt/linux
>>>>>>>>> >>>>> export AXIOM=3D/usr/lib/axiom-20170501
>>>>>>>>> >>>>> export "PATH=3D/usr/lib/axiom-20170501/bin:$PATH"
>>>>>>>>> >>>>>
>>>>>>>>> >>>>> 4 WSL2) create a .axiom.input file to include startup cmds:
>>>>>>>>> >>>>>
>>>>>>>>> >>>>> emacs .axiom.input
>>>>>>>>> >>>>>
>>>>>>>>> >>>>> )cd "/mnt/c/yourpath"
>>>>>>>>> >>>>> )sys pwd
>>>>>>>>> >>>>>
>>>>>>>>> >>>>> 5 WSL2) create a "myaxiom" command that sets the
>>>>>>>>> >>>>> DISPLAY variable and starts axiom
>>>>>>>>> >>>>>
>>>>>>>>> >>>>> emacs myaxiom
>>>>>>>>> >>>>>
>>>>>>>>> >>>>> #! /bin/bash
>>>>>>>>> >>>>> export DISPLAY=3D:0.0
>>>>>>>>> >>>>> axiom
>>>>>>>>> >>>>>
>>>>>>>>> >>>>> 6 WSL2) put it in the /usr/bin directory
>>>>>>>>> >>>>>
>>>>>>>>> >>>>> chmod +x myaxiom
>>>>>>>>> >>>>> sudo cp myaxiom /usr/bin/myaxiom
>>>>>>>>> >>>>>
>>>>>>>>> >>>>> 7 WINDOWS) start the X11 server
>>>>>>>>> >>>>>
>>>>>>>>> >>>>> (XMing XLaunch Icon on your desktop)
>>>>>>>>> >>>>>
>>>>>>>>> >>>>> 8 WINDOWS) run myaxiom from PowerShell
>>>>>>>>> >>>>> (this should start axiom with graphics available)
>>>>>>>>> >>>>>
>>>>>>>>> >>>>> wsl myaxiom
>>>>>>>>> >>>>>
>>>>>>>>> >>>>> 8 WINDOWS) make a PowerShell desktop
>>>>>>>>> >>>>>
>>>>>>>>> >>>>>
>>>>>>>>> https://superuser.com/questions/886951/run-powershell-script-when=
-you-open-powershell
>>>>>>>>> >>>>>
>>>>>>>>> >>>>> Tim
>>>>>>>>> >>>>>
>>>>>>>>> >>>>> On 8/13/21, Tim Daly wrote:
>>>>>>>>> >>>>>> A great deal of thought is directed toward making the SANE
>>>>>>>>> version
>>>>>>>>> >>>>>> of Axiom as flexible as possible, decoupling mechanism fro=
m
>>>>>>>>> theory.
>>>>>>>>> >>>>>>
>>>>>>>>> >>>>>> An interesting publication by Brian Cantwell Smith [0],
>>>>>>>>> "Reflection
>>>>>>>>> >>>>>> and Semantics in LISP" seems to contain interesting ideas
>>>>>>>>> related
>>>>>>>>> >>>>>> to our goal. Of particular interest is the ability to
>>>>>>>>> reason about
>>>>>>>>> >>>>>> and
>>>>>>>>> >>>>>> perform self-referential manipulations. In a
>>>>>>>>> dependently-typed
>>>>>>>>> >>>>>> system it seems interesting to be able "adapt" code to
>>>>>>>>> handle
>>>>>>>>> >>>>>> run-time computed arguments to dependent functions. The
>>>>>>>>> abstract:
>>>>>>>>> >>>>>>
>>>>>>>>> >>>>>> "We show how a computational system can be constructed =
to
>>>>>>>>> >>>>>> "reason",
>>>>>>>>> >>>>>> effectively
>>>>>>>>> >>>>>> and consequentially, about its own inferential
>>>>>>>>> processes. The
>>>>>>>>> >>>>>> analysis proceeds in two
>>>>>>>>> >>>>>> parts. First, we consider the general question of
>>>>>>>>> computational
>>>>>>>>> >>>>>> semantics, rejecting
>>>>>>>>> >>>>>> traditional approaches, and arguing that the declarativ=
e
>>>>>>>>> and
>>>>>>>>> >>>>>> procedural aspects of
>>>>>>>>> >>>>>> computational symbols (what they stand for, and what
>>>>>>>>> behaviour
>>>>>>>>> >>>>>> they
>>>>>>>>> >>>>>> engender) should be
>>>>>>>>> >>>>>> analysed independently, in order that they may be
>>>>>>>>> coherently
>>>>>>>>> >>>>>> related. Second, we
>>>>>>>>> >>>>>> investigate self-referential behavior in computational
>>>>>>>>> processes,
>>>>>>>>> >>>>>> and show how to embed an
>>>>>>>>> >>>>>> effective procedural model of a computational calculus
>>>>>>>>> within that
>>>>>>>>> >>>>>> calculus (a model not
>>>>>>>>> >>>>>> unlike a meta-circular interpreter, but connected to th=
e
>>>>>>>>> >>>>>> fundamental operations of the
>>>>>>>>> >>>>>> machine in such a way as to provide, at any point in a
>>>>>>>>> >>>>>> computation,
>>>>>>>>> >>>>>> fully articulated
>>>>>>>>> >>>>>> descriptions of the state of that computation, for
>>>>>>>>> inspection and
>>>>>>>>> >>>>>> possible modification). In
>>>>>>>>> >>>>>> terms of the theories that result from these
>>>>>>>>> investigations, we
>>>>>>>>> >>>>>> present a general architecture
>>>>>>>>> >>>>>> for procedurally reflective processes, able to shift
>>>>>>>>> smoothly
>>>>>>>>> >>>>>> between dealing with a given
>>>>>>>>> >>>>>> subject domain, and dealing with their own reasoning
>>>>>>>>> processes
>>>>>>>>> >>>>>> over
>>>>>>>>> >>>>>> that domain.
>>>>>>>>> >>>>>>
>>>>>>>>> >>>>>> An instance of the general solution is worked out in th=
e
>>>>>>>>> context
>>>>>>>>> >>>>>> of
>>>>>>>>> >>>>>> an applicative
>>>>>>>>> >>>>>> language. Specifically, we present three successive
>>>>>>>>> dialects of
>>>>>>>>> >>>>>> LISP: 1-LISP, a distillation of
>>>>>>>>> >>>>>> current practice, for comparison purposes; 2-LISP, a
>>>>>>>>> dialect
>>>>>>>>> >>>>>> constructed in terms of our
>>>>>>>>> >>>>>> rationalised semantics, in which the concept of
>>>>>>>>> evaluation is
>>>>>>>>> >>>>>> rejected in favour of
>>>>>>>>> >>>>>> independent notions of simplification and reference, an=
d
>>>>>>>>> in which
>>>>>>>>> >>>>>> the respective categories
>>>>>>>>> >>>>>> of notation, structure, semantics, and behaviour are
>>>>>>>>> strictly
>>>>>>>>> >>>>>> aligned; and 3-LISP, an
>>>>>>>>> >>>>>> extension of 2-LISP endowed with reflective powers."
>>>>>>>>> >>>>>>
>>>>>>>>> >>>>>> Axiom SANE builds dependent types on the fly. The ability
>>>>>>>>> to access
>>>>>>>>> >>>>>> both the refection
>>>>>>>>> >>>>>> of the tower of algebra and the reflection of the tower of
>>>>>>>>> proofs at
>>>>>>>>> >>>>>> the time of construction
>>>>>>>>> >>>>>> makes the construction of a new domain or specific
>>>>>>>>> algorithm easier
>>>>>>>>> >>>>>> and more general.
>>>>>>>>> >>>>>>
>>>>>>>>> >>>>>> This is of particular interest because one of the efforts
>>>>>>>>> is to build
>>>>>>>>> >>>>>> "all the way down to the
>>>>>>>>> >>>>>> metal". If each layer is constructed on top of previous
>>>>>>>>> proven layers
>>>>>>>>> >>>>>> and the new layer
>>>>>>>>> >>>>>> can "reach below" to lower layers then the tower of layers
>>>>>>>>> can be
>>>>>>>>> >>>>>> built without duplication.
>>>>>>>>> >>>>>>
>>>>>>>>> >>>>>> Tim
>>>>>>>>> >>>>>>
>>>>>>>>> >>>>>> [0], Smith, Brian Cantwell "Reflection and Semantics in
>>>>>>>>> LISP"
>>>>>>>>> >>>>>> POPL '84: Proceedings of the 11th ACM SIGACT-SIGPLAN
>>>>>>>>> >>>>>> ymposium on Principles of programming languagesJanuary 1
>>>>>>>>> >>>>>> 984 Pages 23=E2=80=9335https://doi.org/10.1145/800017.8005=
13
>>>>>>>>> >>>>>>
>>>>>>>>> >>>>>> On 6/29/21, Tim Daly wrote:
>>>>>>>>> >>>>>>> Having spent time playing with hardware it is perfectly
>>>>>>>>> clear that
>>>>>>>>> >>>>>>> future computational mathematics efforts need to adapt to
>>>>>>>>> using
>>>>>>>>> >>>>>>> parallel processing.
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>> I've spent a fair bit of time thinking about structuring
>>>>>>>>> Axiom to
>>>>>>>>> >>>>>>> be parallel. Most past efforts have tried to focus on
>>>>>>>>> making a
>>>>>>>>> >>>>>>> particular algorithm parallel, such as a matrix multiply.
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>> But I think that it might be more effective to make each
>>>>>>>>> domain
>>>>>>>>> >>>>>>> run in parallel. A computation crosses multiple domains s=
o
>>>>>>>>> a
>>>>>>>>> >>>>>>> particular computation could involve multiple parallel
>>>>>>>>> copies.
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>> For example, computing the Cylindrical Algebraic
>>>>>>>>> Decomposition
>>>>>>>>> >>>>>>> could recursively decompose the plane. Indeed, any
>>>>>>>>> tree-recursive
>>>>>>>>> >>>>>>> algorithm could be run in parallel "in the large" by
>>>>>>>>> creating new
>>>>>>>>> >>>>>>> running copies of the domain for each sub-problem.
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>> So the question becomes, how does one manage this?
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>> A similar problem occurs in robotics where one could have
>>>>>>>>> multiple
>>>>>>>>> >>>>>>> wheels, arms, propellers, etc. that need to act
>>>>>>>>> independently but
>>>>>>>>> >>>>>>> in coordination.
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>> The robot solution uses ROS2. The three ideas are ROSCORE=
,
>>>>>>>>> >>>>>>> TOPICS with publish/subscribe, and SERVICES with
>>>>>>>>> request/response.
>>>>>>>>> >>>>>>> These are communication paths defined between processes.
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>> ROS2 has a "roscore" which is basically a phonebook of
>>>>>>>>> "topics".
>>>>>>>>> >>>>>>> Any process can create or look up the current active
>>>>>>>>> topics. eq:
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>> rosnode list
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>> TOPICS:
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>> Any process can PUBLISH a topic (which is basically a
>>>>>>>>> typed data
>>>>>>>>> >>>>>>> structure), e.g the topic /hw with the String data "Hello
>>>>>>>>> World".
>>>>>>>>> >>>>>>> eg:
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>> rostopic pub /hw std_msgs/String "Hello, World"
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>> Any process can SUBSCRIBE to a topic, such as /hw, and ge=
t
>>>>>>>>> a
>>>>>>>>> >>>>>>> copy of the data. eg:
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>> rostopic echo /hw =3D=3D> "Hello, World"
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>> Publishers talk, subscribers listen.
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>> SERVICES:
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>> Any process can make a REQUEST of a SERVICE and get a
>>>>>>>>> RESPONSE.
>>>>>>>>> >>>>>>> This is basically a remote function call.
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>> Axiom in parallel?
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>> So domains could run, each in its own process. It could
>>>>>>>>> provide
>>>>>>>>> >>>>>>> services, one for each function. Any other process could
>>>>>>>>> request
>>>>>>>>> >>>>>>> a computation and get the result as a response. Domains
>>>>>>>>> could
>>>>>>>>> >>>>>>> request services from other domains, either waiting for
>>>>>>>>> responses
>>>>>>>>> >>>>>>> or continuing while the response is being computed.
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>> The output could be sent anywhere, to a terminal, to a
>>>>>>>>> browser,
>>>>>>>>> >>>>>>> to a network, or to another process using the
>>>>>>>>> publish/subscribe
>>>>>>>>> >>>>>>> protocol, potentially all at the same time since there ca=
n
>>>>>>>>> be many
>>>>>>>>> >>>>>>> subscribers to a topic.
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>> Available domains could be dynamically added by announcin=
g
>>>>>>>>> >>>>>>> themselves as new "topics" and could be dynamically
>>>>>>>>> looked-up
>>>>>>>>> >>>>>>> at runtime.
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>> This structure allows function-level / domain-level
>>>>>>>>> parallelism.
>>>>>>>>> >>>>>>> It is very effective in the robot world and I think it
>>>>>>>>> might be a
>>>>>>>>> >>>>>>> good structuring mechanism to allow computational
>>>>>>>>> mathematics
>>>>>>>>> >>>>>>> to take advantage of multiple processors in a disciplined
>>>>>>>>> fashion.
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>> Axiom has a thousand domains and each could run on its ow=
n
>>>>>>>>> core.
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>> In addition. notice that each domain is independent of th=
e
>>>>>>>>> others.
>>>>>>>>> >>>>>>> So if we want to use BLAS Fortran code, it could just be
>>>>>>>>> another
>>>>>>>>> >>>>>>> service node. In fact, any "foreign function" could
>>>>>>>>> transparently
>>>>>>>>> >>>>>>> cooperate in a distributed Axiom.
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>> Another key feature is that proofs can be "by node".
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>> Tim
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>> On 6/5/21, Tim Daly wrote:
>>>>>>>>> >>>>>>>> Axiom is based on first-class dependent types. Deciding
>>>>>>>>> when
>>>>>>>>> >>>>>>>> two types are equivalent may involve computation. See
>>>>>>>>> >>>>>>>> Christiansen, David Thrane "Checking Dependent Types wit=
h
>>>>>>>>> >>>>>>>> Normalization by Evaluation" (2019)
>>>>>>>>> >>>>>>>>
>>>>>>>>> >>>>>>>> This puts an interesting constraint on building types. T=
he
>>>>>>>>> >>>>>>>> constructed types has to export a function to decide if =
a
>>>>>>>>> >>>>>>>> given type is "equivalent" to itself.
>>>>>>>>> >>>>>>>>
>>>>>>>>> >>>>>>>> The notion of "equivalence" might involve category ideas
>>>>>>>>> >>>>>>>> of natural transformation and univalence. Sigh.
>>>>>>>>> >>>>>>>>
>>>>>>>>> >>>>>>>> That's an interesting design point.
>>>>>>>>> >>>>>>>>
>>>>>>>>> >>>>>>>> Tim
>>>>>>>>> >>>>>>>>
>>>>>>>>> >>>>>>>>
>>>>>>>>> >>>>>>>> On 5/5/21, Tim Daly wrote:
>>>>>>>>> >>>>>>>>> It is interesting that programmer's eyes and
>>>>>>>>> expectations adapt
>>>>>>>>> >>>>>>>>> to the tools they use. For instance, I use emacs and
>>>>>>>>> expect to
>>>>>>>>> >>>>>>>>> work directly in files and multiple buffers. When I try
>>>>>>>>> to use one
>>>>>>>>> >>>>>>>>> of the many IDE tools I find they tend to "get in the
>>>>>>>>> way". I
>>>>>>>>> >>>>>>>>> already
>>>>>>>>> >>>>>>>>> know or can quickly find whatever they try to tell me.
>>>>>>>>> If you use
>>>>>>>>> >>>>>>>>> an
>>>>>>>>> >>>>>>>>> IDE you probably find emacs "too sparse" for programmin=
g.
>>>>>>>>> >>>>>>>>>
>>>>>>>>> >>>>>>>>> Recently I've been working in a sparse programming
>>>>>>>>> environment.
>>>>>>>>> >>>>>>>>> I'm exploring the question of running a proof checker i=
n
>>>>>>>>> an FPGA.
>>>>>>>>> >>>>>>>>> The FPGA development tools are painful at best and not
>>>>>>>>> intuitive
>>>>>>>>> >>>>>>>>> since you SEEM to be programming but you're actually
>>>>>>>>> describing
>>>>>>>>> >>>>>>>>> hardware gates, connections, and timing. This is an
>>>>>>>>> environment
>>>>>>>>> >>>>>>>>> where everything happens all-at-once and all-the-time
>>>>>>>>> (like the
>>>>>>>>> >>>>>>>>> circuits in your computer). It is the "assembly languag=
e
>>>>>>>>> of
>>>>>>>>> >>>>>>>>> circuits".
>>>>>>>>> >>>>>>>>> Naturally, my eyes have adapted to this rather raw leve=
l.
>>>>>>>>> >>>>>>>>>
>>>>>>>>> >>>>>>>>> That said, I'm normally doing literate programming all
>>>>>>>>> the time.
>>>>>>>>> >>>>>>>>> My typical file is a document which is a mixture of
>>>>>>>>> latex and
>>>>>>>>> >>>>>>>>> lisp.
>>>>>>>>> >>>>>>>>> It is something of a shock to return to that world. It
>>>>>>>>> is clear
>>>>>>>>> >>>>>>>>> why
>>>>>>>>> >>>>>>>>> people who program in Python find lisp to be a "sea of
>>>>>>>>> parens".
>>>>>>>>> >>>>>>>>> Yet as a lisp programmer, I don't even see the parens,
>>>>>>>>> just code.
>>>>>>>>> >>>>>>>>>
>>>>>>>>> >>>>>>>>> It takes a few minutes in a literate document to adapt
>>>>>>>>> vision to
>>>>>>>>> >>>>>>>>> see the latex / lisp combination as natural. The latex
>>>>>>>>> markup,
>>>>>>>>> >>>>>>>>> like the lisp parens, eventually just disappears. What
>>>>>>>>> remains
>>>>>>>>> >>>>>>>>> is just lisp and natural language text.
>>>>>>>>> >>>>>>>>>
>>>>>>>>> >>>>>>>>> This seems painful at first but eyes quickly adapt. The
>>>>>>>>> upside
>>>>>>>>> >>>>>>>>> is that there is always a "finished" document that
>>>>>>>>> describes the
>>>>>>>>> >>>>>>>>> state of the code. The overhead of writing a paragraph =
to
>>>>>>>>> >>>>>>>>> describe a new function or change a paragraph to
>>>>>>>>> describe the
>>>>>>>>> >>>>>>>>> changed function is very small.
>>>>>>>>> >>>>>>>>>
>>>>>>>>> >>>>>>>>> Using a Makefile I latex the document to generate a
>>>>>>>>> current PDF
>>>>>>>>> >>>>>>>>> and then I extract, load, and execute the code. This
>>>>>>>>> loop catches
>>>>>>>>> >>>>>>>>> errors in both the latex and the source code. Keeping a=
n
>>>>>>>>> open file
>>>>>>>>> >>>>>>>>> in
>>>>>>>>> >>>>>>>>> my pdf viewer shows all of the changes in the document
>>>>>>>>> after every
>>>>>>>>> >>>>>>>>> run of make. That way I can edit the book as easily as
>>>>>>>>> the code.
>>>>>>>>> >>>>>>>>>
>>>>>>>>> >>>>>>>>> Ultimately I find that writing the book while writing
>>>>>>>>> the code is
>>>>>>>>> >>>>>>>>> more productive. I don't have to remember why I wrote
>>>>>>>>> something
>>>>>>>>> >>>>>>>>> since the explanation is already there.
>>>>>>>>> >>>>>>>>>
>>>>>>>>> >>>>>>>>> We all have our own way of programming and our own tool=
s.
>>>>>>>>> >>>>>>>>> But I find literate programming to be a real advance
>>>>>>>>> over IDE
>>>>>>>>> >>>>>>>>> style programming and "raw code" programming.
>>>>>>>>> >>>>>>>>>
>>>>>>>>> >>>>>>>>> Tim
>>>>>>>>> >>>>>>>>>
>>>>>>>>> >>>>>>>>>
>>>>>>>>> >>>>>>>>> On 2/27/21, Tim Daly wrote:
>>>>>>>>> >>>>>>>>>> The systems I use have the interesting property of
>>>>>>>>> >>>>>>>>>> "Living within the compiler".
>>>>>>>>> >>>>>>>>>>
>>>>>>>>> >>>>>>>>>> Lisp, Forth, Emacs, and other systems that present
>>>>>>>>> themselves
>>>>>>>>> >>>>>>>>>> through the Read-Eval-Print-Loop (REPL) allow the
>>>>>>>>> >>>>>>>>>> ability to deeply interact with the system, shaping it
>>>>>>>>> to your
>>>>>>>>> >>>>>>>>>> need.
>>>>>>>>> >>>>>>>>>>
>>>>>>>>> >>>>>>>>>> My current thread of study is software architecture. S=
ee
>>>>>>>>> >>>>>>>>>>
>>>>>>>>> https://www.youtube.com/watch?v=3DW2hagw1VhhI&feature=3Dyoutu.be
>>>>>>>>> >>>>>>>>>> and https://www.georgefairbanks.com/videos/
>>>>>>>>> >>>>>>>>>>
>>>>>>>>> >>>>>>>>>> My current thinking on SANE involves the ability to
>>>>>>>>> >>>>>>>>>> dynamically define categories, representations, and
>>>>>>>>> functions
>>>>>>>>> >>>>>>>>>> along with "composition functions" that permits
>>>>>>>>> choosing a
>>>>>>>>> >>>>>>>>>> combination at the time of use.
>>>>>>>>> >>>>>>>>>>
>>>>>>>>> >>>>>>>>>> You might want a domain for handling polynomials. Ther=
e
>>>>>>>>> are
>>>>>>>>> >>>>>>>>>> a lot of choices, depending on your use case. You migh=
t
>>>>>>>>> want
>>>>>>>>> >>>>>>>>>> different representations. For example, you might want
>>>>>>>>> dense,
>>>>>>>>> >>>>>>>>>> sparse, recursive, or "machine compatible fixnums"
>>>>>>>>> (e.g. to
>>>>>>>>> >>>>>>>>>> interface with C code). If these don't exist it ought
>>>>>>>>> to be
>>>>>>>>> >>>>>>>>>> possible
>>>>>>>>> >>>>>>>>>> to create them. Such "lego-like" building blocks
>>>>>>>>> require careful
>>>>>>>>> >>>>>>>>>> thought about creating "fully factored" objects.
>>>>>>>>> >>>>>>>>>>
>>>>>>>>> >>>>>>>>>> Given that goal, the traditional barrier of "compiler"
>>>>>>>>> vs
>>>>>>>>> >>>>>>>>>> "interpreter"
>>>>>>>>> >>>>>>>>>> does not seem useful. It is better to "live within the
>>>>>>>>> compiler"
>>>>>>>>> >>>>>>>>>> which
>>>>>>>>> >>>>>>>>>> gives the ability to define new things "on the fly".
>>>>>>>>> >>>>>>>>>>
>>>>>>>>> >>>>>>>>>> Of course, the SANE compiler is going to want an
>>>>>>>>> associated
>>>>>>>>> >>>>>>>>>> proof of the functions you create along with the other
>>>>>>>>> parts
>>>>>>>>> >>>>>>>>>> such as its category hierarchy and representation
>>>>>>>>> properties.
>>>>>>>>> >>>>>>>>>>
>>>>>>>>> >>>>>>>>>> There is no such thing as a simple job. :-)
>>>>>>>>> >>>>>>>>>>
>>>>>>>>> >>>>>>>>>> Tim
>>>>>>>>> >>>>>>>>>>
>>>>>>>>> >>>>>>>>>>
>>>>>>>>> >>>>>>>>>> On 2/18/21, Tim Daly wrote:
>>>>>>>>> >>>>>>>>>>> The Axiom SANE compiler / interpreter has a few desig=
n
>>>>>>>>> points.
>>>>>>>>> >>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>> 1) It needs to mix interpreted and compiled code in
>>>>>>>>> the same
>>>>>>>>> >>>>>>>>>>> function.
>>>>>>>>> >>>>>>>>>>> SANE allows dynamic construction of code as well as
>>>>>>>>> dynamic type
>>>>>>>>> >>>>>>>>>>> construction at runtime. Both of these can occur in a
>>>>>>>>> runtime
>>>>>>>>> >>>>>>>>>>> object.
>>>>>>>>> >>>>>>>>>>> So there is potentially a mixture of interpreted and
>>>>>>>>> compiled
>>>>>>>>> >>>>>>>>>>> code.
>>>>>>>>> >>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>> 2) It needs to perform type resolution at compile tim=
e
>>>>>>>>> without
>>>>>>>>> >>>>>>>>>>> overhead
>>>>>>>>> >>>>>>>>>>> where possible. Since this is not always possible
>>>>>>>>> there needs to
>>>>>>>>> >>>>>>>>>>> be
>>>>>>>>> >>>>>>>>>>> a "prefix thunk" that will perform the resolution.
>>>>>>>>> Trivially,
>>>>>>>>> >>>>>>>>>>> for
>>>>>>>>> >>>>>>>>>>> example,
>>>>>>>>> >>>>>>>>>>> if we have a + function we need to type-resolve the
>>>>>>>>> arguments.
>>>>>>>>> >>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>> However, if we can prove at compile time that the
>>>>>>>>> types are both
>>>>>>>>> >>>>>>>>>>> bounded-NNI and the result is bounded-NNI (i.e. fixnu=
m
>>>>>>>>> in lisp)
>>>>>>>>> >>>>>>>>>>> then we can inline a call to + at runtime. If not, we
>>>>>>>>> might have
>>>>>>>>> >>>>>>>>>>> + applied to NNI and POLY(FLOAT), which requires a
>>>>>>>>> thunk to
>>>>>>>>> >>>>>>>>>>> resolve types. The thunk could even "specialize and
>>>>>>>>> compile"
>>>>>>>>> >>>>>>>>>>> the code before executing it.
>>>>>>>>> >>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>> It turns out that the Forth implementation of
>>>>>>>>> >>>>>>>>>>> "threaded-interpreted"
>>>>>>>>> >>>>>>>>>>> languages model provides an efficient and effective
>>>>>>>>> way to do
>>>>>>>>> >>>>>>>>>>> this.[0]
>>>>>>>>> >>>>>>>>>>> Type resolution can be "inserted" in intermediate
>>>>>>>>> thunks.
>>>>>>>>> >>>>>>>>>>> The model also supports dynamic overloading and tail
>>>>>>>>> recursion.
>>>>>>>>> >>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>> Combining high-level CLOS code with low-level
>>>>>>>>> threading gives an
>>>>>>>>> >>>>>>>>>>> easy to understand and robust design.
>>>>>>>>> >>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>> Tim
>>>>>>>>> >>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>> [0] Loeliger, R.G. "Threaded Interpretive Languages"
>>>>>>>>> (1981)
>>>>>>>>> >>>>>>>>>>> ISBN 0-07-038360-X
>>>>>>>>> >>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>> On 2/5/21, Tim Daly wrote:
>>>>>>>>> >>>>>>>>>>>> I've worked hard to make Axiom depend on almost no
>>>>>>>>> other
>>>>>>>>> >>>>>>>>>>>> tools so that it would not get caught by "code rot" =
of
>>>>>>>>> >>>>>>>>>>>> libraries.
>>>>>>>>> >>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>> However, I'm also trying to make the new SANE versio=
n
>>>>>>>>> much
>>>>>>>>> >>>>>>>>>>>> easier to understand and debug.To that end I've been
>>>>>>>>> >>>>>>>>>>>> experimenting
>>>>>>>>> >>>>>>>>>>>> with some ideas.
>>>>>>>>> >>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>> It should be possible to view source code, of course=
.
>>>>>>>>> But the
>>>>>>>>> >>>>>>>>>>>> source
>>>>>>>>> >>>>>>>>>>>> code is not the only, nor possibly the best,
>>>>>>>>> representation of
>>>>>>>>> >>>>>>>>>>>> the
>>>>>>>>> >>>>>>>>>>>> ideas.
>>>>>>>>> >>>>>>>>>>>> In particular, source code gets compiled into data
>>>>>>>>> structures.
>>>>>>>>> >>>>>>>>>>>> In
>>>>>>>>> >>>>>>>>>>>> Axiom
>>>>>>>>> >>>>>>>>>>>> these data structures really are a graph of related
>>>>>>>>> structures.
>>>>>>>>> >>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>> For example, looking at the gcd function from NNI,
>>>>>>>>> there is the
>>>>>>>>> >>>>>>>>>>>> representation of the gcd function itself. But there
>>>>>>>>> is also a
>>>>>>>>> >>>>>>>>>>>> structure
>>>>>>>>> >>>>>>>>>>>> that is the REP (and, in the new system, is separate
>>>>>>>>> from the
>>>>>>>>> >>>>>>>>>>>> domain).
>>>>>>>>> >>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>> Further, there are associated specification and proo=
f
>>>>>>>>> >>>>>>>>>>>> structures.
>>>>>>>>> >>>>>>>>>>>> Even
>>>>>>>>> >>>>>>>>>>>> further, the domain inherits the category structures=
,
>>>>>>>>> and from
>>>>>>>>> >>>>>>>>>>>> those
>>>>>>>>> >>>>>>>>>>>> it
>>>>>>>>> >>>>>>>>>>>> inherits logical axioms and definitions through the
>>>>>>>>> proof
>>>>>>>>> >>>>>>>>>>>> structure.
>>>>>>>>> >>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>> Clearly the gcd function is a node in a much larger
>>>>>>>>> graph
>>>>>>>>> >>>>>>>>>>>> structure.
>>>>>>>>> >>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>> When trying to decide why code won't compile it woul=
d
>>>>>>>>> be useful
>>>>>>>>> >>>>>>>>>>>> to
>>>>>>>>> >>>>>>>>>>>> be able to see and walk these structures. I've
>>>>>>>>> thought about
>>>>>>>>> >>>>>>>>>>>> using
>>>>>>>>> >>>>>>>>>>>> the
>>>>>>>>> >>>>>>>>>>>> browser but browsers are too weak. Either everything
>>>>>>>>> has to be
>>>>>>>>> >>>>>>>>>>>> "in
>>>>>>>>> >>>>>>>>>>>> a
>>>>>>>>> >>>>>>>>>>>> single tab to show the graph" or "the nodes of the
>>>>>>>>> graph are in
>>>>>>>>> >>>>>>>>>>>> different
>>>>>>>>> >>>>>>>>>>>> tabs". Plus, constructing dynamic graphs that change
>>>>>>>>> as the
>>>>>>>>> >>>>>>>>>>>> software
>>>>>>>>> >>>>>>>>>>>> changes (e.g. by loading a new spad file or creating
>>>>>>>>> a new
>>>>>>>>> >>>>>>>>>>>> function)
>>>>>>>>> >>>>>>>>>>>> represents the huge problem of keeping the browser
>>>>>>>>> "in sync
>>>>>>>>> >>>>>>>>>>>> with
>>>>>>>>> >>>>>>>>>>>> the
>>>>>>>>> >>>>>>>>>>>> Axiom workspace". So something more dynamic and
>>>>>>>>> embedded is
>>>>>>>>> >>>>>>>>>>>> needed.
>>>>>>>>> >>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>> Axiom source gets compiled into CLOS data structures=
.
>>>>>>>>> Each of
>>>>>>>>> >>>>>>>>>>>> these
>>>>>>>>> >>>>>>>>>>>> new SANE structures has an associated surface
>>>>>>>>> representation,
>>>>>>>>> >>>>>>>>>>>> so
>>>>>>>>> >>>>>>>>>>>> they
>>>>>>>>> >>>>>>>>>>>> can be presented in user-friendly form.
>>>>>>>>> >>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>> Also, since Axiom is literate software, it should be
>>>>>>>>> possible
>>>>>>>>> >>>>>>>>>>>> to
>>>>>>>>> >>>>>>>>>>>> look
>>>>>>>>> >>>>>>>>>>>> at
>>>>>>>>> >>>>>>>>>>>> the code in its literate form with the surrounding
>>>>>>>>> explanation.
>>>>>>>>> >>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>> Essentially we'd like to have the ability to "deep
>>>>>>>>> dive" into
>>>>>>>>> >>>>>>>>>>>> the
>>>>>>>>> >>>>>>>>>>>> Axiom
>>>>>>>>> >>>>>>>>>>>> workspace, not only for debugging, but also for
>>>>>>>>> understanding
>>>>>>>>> >>>>>>>>>>>> what
>>>>>>>>> >>>>>>>>>>>> functions are used, where they come from, what they
>>>>>>>>> inherit,
>>>>>>>>> >>>>>>>>>>>> and
>>>>>>>>> >>>>>>>>>>>> how they are used in a computation.
>>>>>>>>> >>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>> To that end I'm looking at using McClim, a lisp
>>>>>>>>> windowing
>>>>>>>>> >>>>>>>>>>>> system.
>>>>>>>>> >>>>>>>>>>>> Since the McClim windows would be part of the lisp
>>>>>>>>> image, they
>>>>>>>>> >>>>>>>>>>>> have
>>>>>>>>> >>>>>>>>>>>> access to display (and modify) the Axiom workspace a=
t
>>>>>>>>> all
>>>>>>>>> >>>>>>>>>>>> times.
>>>>>>>>> >>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>> The only hesitation is that McClim uses quicklisp an=
d
>>>>>>>>> drags in
>>>>>>>>> >>>>>>>>>>>> a
>>>>>>>>> >>>>>>>>>>>> lot
>>>>>>>>> >>>>>>>>>>>> of other subsystems. It's all lisp, of course.
>>>>>>>>> >>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>> These ideas aren't new. They were available on
>>>>>>>>> Symbolics
>>>>>>>>> >>>>>>>>>>>> machines,
>>>>>>>>> >>>>>>>>>>>> a truly productive platform and one I sorely miss.
>>>>>>>>> >>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>> Tim
>>>>>>>>> >>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>> On 1/19/21, Tim Daly wrote:
>>>>>>>>> >>>>>>>>>>>>> Also of interest is the talk
>>>>>>>>> >>>>>>>>>>>>> "The Unreasonable Effectiveness of Dynamic Typing f=
or
>>>>>>>>> >>>>>>>>>>>>> Practical
>>>>>>>>> >>>>>>>>>>>>> Programs"
>>>>>>>>> >>>>>>>>>>>>> https://vimeo.com/74354480
>>>>>>>>> >>>>>>>>>>>>> which questions whether static typing really has an=
y
>>>>>>>>> benefit.
>>>>>>>>> >>>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>>> Tim
>>>>>>>>> >>>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>>> On 1/19/21, Tim Daly wrote:
>>>>>>>>> >>>>>>>>>>>>>> Peter Naur wrote an article of interest:
>>>>>>>>> >>>>>>>>>>>>>> http://pages.cs.wisc.edu/~remzi/Naur.pdf
>>>>>>>>> >>>>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>>>> In particular, it mirrors my notion that Axiom nee=
ds
>>>>>>>>> >>>>>>>>>>>>>> to embrace literate programming so that the "theor=
y
>>>>>>>>> >>>>>>>>>>>>>> of the problem" is presented as well as the "theor=
y
>>>>>>>>> >>>>>>>>>>>>>> of the solution". I quote the introduction:
>>>>>>>>> >>>>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>>>> This article is, to my mind, the most accurate
>>>>>>>>> account
>>>>>>>>> >>>>>>>>>>>>>> of what goes on in designing and coding a program.
>>>>>>>>> >>>>>>>>>>>>>> I refer to it regularly when discussing how much
>>>>>>>>> >>>>>>>>>>>>>> documentation to create, how to pass along tacit
>>>>>>>>> >>>>>>>>>>>>>> knowledge, and the value of the XP's
>>>>>>>>> metaphor-setting
>>>>>>>>> >>>>>>>>>>>>>> exercise. It also provides a way to examine a
>>>>>>>>> methodolgy's
>>>>>>>>> >>>>>>>>>>>>>> economic structure.
>>>>>>>>> >>>>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>>>> In the article, which follows, note that the
>>>>>>>>> quality of the
>>>>>>>>> >>>>>>>>>>>>>> designing programmer's work is related to the
>>>>>>>>> quality of
>>>>>>>>> >>>>>>>>>>>>>> the match between his theory of the problem and hi=
s
>>>>>>>>> theory
>>>>>>>>> >>>>>>>>>>>>>> of the solution. Note that the quality of a later
>>>>>>>>> >>>>>>>>>>>>>> programmer's
>>>>>>>>> >>>>>>>>>>>>>> work is related to the match between his theories
>>>>>>>>> and the
>>>>>>>>> >>>>>>>>>>>>>> previous programmer's theories.
>>>>>>>>> >>>>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>>>> Using Naur's ideas, the designer's job is not to
>>>>>>>>> pass along
>>>>>>>>> >>>>>>>>>>>>>> "the design" but to pass along "the theories"
>>>>>>>>> driving the
>>>>>>>>> >>>>>>>>>>>>>> design.
>>>>>>>>> >>>>>>>>>>>>>> The latter goal is more useful and more
>>>>>>>>> appropriate. It also
>>>>>>>>> >>>>>>>>>>>>>> highlights that knowledge of the theory is tacit i=
n
>>>>>>>>> the
>>>>>>>>> >>>>>>>>>>>>>> owning,
>>>>>>>>> >>>>>>>>>>>>>> and
>>>>>>>>> >>>>>>>>>>>>>> so passing along the thoery requires passing along
>>>>>>>>> both
>>>>>>>>> >>>>>>>>>>>>>> explicit
>>>>>>>>> >>>>>>>>>>>>>> and tacit knowledge.
>>>>>>>>> >>>>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>>>> Tim
>>>>>>>>> >>>>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>>
>>>>>>>>> >>>>>>>>>>
>>>>>>>>> >>>>>>>>>
>>>>>>>>> >>>>>>>>
>>>>>>>>> >>>>>>>
>>>>>>>>> >>>>>>
>>>>>>>>> >>>>>
>>>>>>>>> >>>>
>>>>>>>>> >>>
>>>>>>>>> >>
>>>>>>>>> >
>>>>>>>>>
>>>>>>>>
--000000000000b20b2205d63670f9
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

Problems by Progam Synthesis: Calculus, Differential

Equat=
ions, Linear Algebra, and More.

This is an interesting paper (especially given that i=
t

is work under Gilbert Strang):

A =
Neural Network Solves and Generates Mathematics

Problems by Proga=
m Synthesis: Calculus, Differential

Equations, Linear Algebra, an=
d More.

"This work s=
hows that a neural network that generates

programs (i.e. program =
synthesis) is the key to solving

math and STEM courses at scale, =
as it turns question

answering into a programming task."

This seems interesting from several aspects:

1) Can this be applied to logic systems? Can it help

<= /div>

--0000000000001fed7e05d52d4c44--
From MAILER-DAEMON Mon Jan 10 07:28:42 2022
Received: from list by lists.gnu.org with archive (Exim 4.90_1)
id 1n6tn0-0004VR-HO
for mharc-axiom-developer@gnu.org; Mon, 10 Jan 2022 07:28:42 -0500
Received: from eggs.gnu.org ([209.51.188.92]:45778)
by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from )
id 1n6tmz-0004VF-Cv
for axiom-developer@nongnu.org; Mon, 10 Jan 2022 07:28:41 -0500
Received: from [2607:f8b0:4864:20::730] (port=44756
helo=mail-qk1-x730.google.com)
by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
(Exim 4.90_1) (envelope-from )
id 1n6tmv-0008NO-Jk
for axiom-developer@nongnu.org; Mon, 10 Jan 2022 07:28:41 -0500
Received: by mail-qk1-x730.google.com with SMTP id l11so14553233qke.11
for ; Mon, 10 Jan 2022 04:28:37 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112;
h=mime-version:references:in-reply-to:from:date:message-id:subject:to
:cc; bh=6V3Qdu1DcKzqsanJhWY+g4NbJJDcWAAAZ5tyaIGOgkg=;
b=GScmImpLtMPOtQrwTVtPBMbjmz8TDnxgUVe9gRQuq0qgNB/fqIrccBZNK9jyIB13fJ
TOkdK6ViaX68k2aTk+SbLI/QPkhua7D1+gK68SVU9lg7WfmTvu538xmjQzqYHXBJqs1z
nQo4E09t5qg/kt7AdumiCnGndDedjFH4H2ZZFj+JStB8xCbvdPi23a9d59UcxKfKzmdo
RJcm6YDhv/qk3TukIkLdHn2eiIsVbfkLHcYwiWnCVplLR+blFIgzsl/KVWjt5IxIf4zL
664ah0teyOKNqDwrpAxkuyaWHPsgO5ytG5IqgHh4cKhWX8K+YzrXh69vIllbSiBXXFob
eQkw==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=1e100.net; s=20210112;
h=x-gm-message-state:mime-version:references:in-reply-to:from:date
:message-id:subject:to:cc;
bh=6V3Qdu1DcKzqsanJhWY+g4NbJJDcWAAAZ5tyaIGOgkg=;
b=HD5Yv/mg8ewps1F0k3NDGbI8FpS3306uT660GGzeey+s8zMf3P4l3GGYvAeT+Her/8
oR177RvL9LMkAkO4g/SGsuSgjqzF1hgWQVeOna32fEbMwd/o8RerDsZd02ytWmOYuDEQ
KBtPVaEmT1cWGP0cV8CukngNt2iUoBNXB7/dJytXHnLguBBGbU26+WevbKUaH5Ss+bhg
tzamxPRQ/TTGqmSqA8i1AtOORry3MQRQtOpfva1lbWVEeO2pQVIqWd5AcH1r6/0RywFr
FOL2MATb9qcOLOMTEkkqrYNIr5pDaWsLY5WC9ut5E5rZBUFeCLtRnGqDTA9A3EXataNV
Nz/A==
X-Gm-Message-State: AOAM533X7L1bccG8R8cHKD2UEx8N7Msa1+QdokHMqAtRIZgTFl6LYdbv
EKgg2luy25avRvFh2Q8XTklPNXOGTZpQFVXrmVU=
X-Google-Smtp-Source: ABdhPJxGj7tWXbhC0XadARj8iOqBL/lT/PDgk0GxpEiFbLr5MGGWQpUAl1QgmikVZIW/tSGcjoazjGnQNTYmkkCkiIk=
X-Received: by 2002:a05:620a:815:: with SMTP id
s21mr14620480qks.54.1641817716256;
Mon, 10 Jan 2022 04:28:36 -0800 (PST)
MIME-Version: 1.0
References:
In-Reply-To:
From: Tim Daly
Date: Mon, 10 Jan 2022 07:28:24 -0500
Message-ID:
Subject: Re: A NN Solves and Generates Math Problems
To: Jeremy Avigad
Cc: Frank Pfenning , Prof Robert Harper ,
mcarneir , axiom-dev
Content-Type: multipart/alternative; boundary="000000000000c3745f05d5397925"
X-Host-Lookup-Failed: Reverse DNS lookup failed for 2607:f8b0:4864:20::730
(failed)
Received-SPF: pass client-ip=2607:f8b0:4864:20::730;
envelope-from=axiomcas@gmail.com; helo=mail-qk1-x730.google.com
X-Spam_score_int: -12
X-Spam_score: -1.3
X-Spam_bar: -
X-Spam_report: (-1.3 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1,
DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, FREEMAIL_FROM=0.001,
HTML_MESSAGE=0.001, RCVD_IN_DNSWL_NONE=-0.0001, RDNS_NONE=0.793,
SPF_HELO_NONE=0.001, SPF_PASS=-0.001 autolearn=no autolearn_force=no
X-Spam_action: no action
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.29
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Mon, 10 Jan 2022 12:28:41 -0000
--000000000000c3745f05d5397925
Content-Type: text/plain; charset="UTF-8"
Suppose the goal was to generate code from proofs.
Suppose that certain tactics have "code-like" equivalents.
Can we define such a restricted set of tactics?
This would eliminate Coq's hammer tactic, for example.
The definition of an axiom could include the text for the
equivalent program, making them "effective theorems",
or "fully constructive theorems".
Given a proof of a theorem from this restricted set
it should be (somewhat) easier to create equivalent programs.
This amounts to "proving the theorem" by "writing the program",
albeit in a tactic language.
For example, a "reduce" tactic would apply a function to a
set of numbers (symbolically), with the proof condition that
the set is finite and the generated index decreases so we
can know that "reduce" terminates. That would then be
equivalent to the Lisp map operation.
Tim
On Sun, Jan 9, 2022 at 4:56 PM Tim Daly wrote:
> In general, I'm pretty skeptical of Neural Net generation of math,
> but I'm following the literature quite closely.
>
> I recently spent time with an effort that tried to do integration.
> It was interesting because they could "round trip" the solution by
> differentiating the result. I worked with the authors, added some
> of their results to Axiom, and suggested possible further work. But
> the approach, while it looks impressive, has quite a few flaws.
>
> I have yet to "deep dive" into this paper. It is really interesting to
> me that it claims to generate code. I would like to see a "round
> trip" where some LEAN math was used to generate code and
> then the code was proven using LEAN. Especially interesting
> would be the question of how the definitions and axioms of the
> original LEAN proof were used, if at all, in the proof of the code.
> (Of course, LEAN doesn't seem to focus on proving code.)
>
> From an Axiom point of view, "proven code generation" from a
> proven theorem is my holy grail. If there was a way to form a
> one-to-one, onto mapping between theorems and code I'd be
> rewriting all of Axiom using it. I doubt that a Neural Net can
> achieve such a mapping.
>
> Given that Axiom is using first-class dependent types I'm not
> at all clear how that could be possible using a Neural Net.
> Can a Neural Net even infer the correct Types? I suppose,
> for the simple case such as NAT, it could "learn" from the
> definitions but cubical types might be a tad bit harder.
>
> Nor is it clear to me how you would generate code that was
> sound but not complete.
>
> I just looked up Bartosz's body of work. It looks really interesting,
> giving me much more to read.
>
> Tim
>
>
>
> On Sun, Jan 9, 2022 at 1:22 PM Jeremy Avigad wrote:
>
>> Thanks for this! It seems to speak to the success of the OpenAI Codex
>> more than anything else, but the results are impressive.
>>
>> Bartosz Piotrowski, a PhD student and author of one of the papers you
>> cited, will be visiting Carnegie Mellon for a few months this spring.
>>
>> Best wishes,
>>
>> Jeremy
>>
>> On Thu, Jan 6, 2022 at 10:30 AM Tim Daly wrote:
>>
>>> This is an interesting paper (especially given that it
>>> is work under Gilbert Strang):
>>>
>>> A Neural Network Solves and Generates Mathematics
>>> Problems by Progam Synthesis: Calculus, Differential
>>> Equations, Linear Algebra, and More.
>>> https://arxiv.org/pdf/2112.15594.pdf
>>>
>>> "This work shows that a neural network that generates
>>> programs (i.e. program synthesis) is the key to solving
>>> math and STEM courses at scale, as it turns question
>>> answering into a programming task."
>>>
>>> This seems interesting from several aspects:
>>>
>>> 1) Can this be applied to logic systems? Can it help
>>> generate "proven code" from a proof system? (LEAN)
>>>
>>> 2) Can it be applied in programs like NuPRL / RedPRL?
>>> (Innovations in Computational Type Theory using Nuprl
>>> Journal of Applied Logic 4 (2006) pp 428--469
>>>
>>> https://reader.elsevier.com/reader/sd/pii/S1570868305000704?token=C11F82ADA94390097338EF7E421A4D9DFEF909336A451BF51D3099EDF1025177323CCD7B46510F77FFC4955D0AC6724F&originRegion=us-east-1&originCreation=20220106150458
>>>
>>> 3) Can the type of an object be inferred by casting it as a
>>> question in mathematics? Is the generated program correctly
>>> typed?
>>>
>>> 4) Can this be layered on MetaMath (LEAN) or FDL (Nuprl)
>>> to generate logically equivalent code?
>>>
>>> 5) Can this be applied to gradual typing?
>>>
>>> In any case, this represents an interesting "interdisciplinary"
>>> effort connecting the math department and CS.
>>>
>>> Tim
>>>
>>>
>>>
>>> There are various connections to Neural Networks and Math:
>>>
>>> @misc{Crou19,
>>> author = "Crouse, Maxwell and Whitehead, Spencer and
>>> Abdelaziz, Ibrahim and Makni, Bassem and
>>> Cornelio, Cristina and Kapanipathi, Pavan and
>>> Pell, Edwin and Srinivas, Kavitha and
>>> Thost, Veronika and Witbrock, Michael and
>>> Fokoue, Achille",
>>> title = {{A Deep Reinforcement Learning Base Approach to Learning
>>> Transferable Proof Guidance Strategies}},
>>> year = "2019",
>>> linke = "\url{https://arxiv.org/pdf/1911.02065.pdf}",
>>> abstract =
>>> "Traditional first-order logic (FOL) reasoning systems usually
>>> rely on manual heuristics for proof guidance. We propose TRAIL: a
>>> system that learns to perform proof guidance using reinforcement
>>> learning. A key design principle of our system is that it is
>>> general enough to allow transfer to problems in different domains
>>> that do not share the same vocabulary of the training set. To do
>>> so, we developed a novel representation of the internal state of a
>>> prover in terms of clauses and inference actions, and a novel
>>> neural-based attention mechanism to learn interactions between
>>> clauses. We demonstrate that this approach enables the system to
>>> generalize from training to test data across domains with
>>> different vocabularies, suggesting that the nerual architecture in
>>> TRAIL is well suited for representing and processing of logical
>>> formalisms.",
>>> paper = "Crou19.pdf"
>>> }
>>>
>>> @misc{Crou19a,
>>> author = "Crouse, Maxwell and Abdelaziz, Ibrahim and
>>> Cornelio, Cristina and Thost, Veronika and
>>> Wu, Lingfei and Forbus, Kenneth and Fokoue, Achille",
>>> title = {{Improving Graph Neural Network Representations of Logical
>>> Formulae with Subgraph Pooling}},
>>> year = "2019",
>>> linke = "\url{https://arxiv.org/pdf/1911.06904.pdf}",
>>> abstract =
>>> "Recent advances in the integration of deep learning with
>>> automated theorem proving have centered around the representation
>>> of graph-structured representations, in large part driven by the
>>> rapidly emerging body of research in geometric deep
>>> learning. Typically, structure-aware neural methods for embedding
>>> logical formulae have been variants of either Tree LSTMs or
>>> GNNs. While more effective than character and token-level
>>> approaches, such methods have often made representational
>>> trade-offs that limited their ability to effectively represent the
>>> global structure of their inputs. In this work, we introduce a
>>> novel approach for embedding logical formulae using DAG LSTMs that
>>> is designed to overome the limitations of both Tree LSTMs and
>>> GNNs. The effectiveness of the proposed framework is demonstrated
>>> on the tasks of premise selection and proof step classification
>>> where it achieves the state-of-the-art performance on two standard
>>> datasets.",
>>> paper = "Crou19a.pdf"
>>> }
>>>
>>> @misc{Gaut19,
>>> author = "Gauthier, Thibault",
>>> title = {{Deep Reinforcement Learning in HOL4}},
>>> year = "2019",
>>> link = "\url{https://arxiv.org/pdf/1910.11797.pdf}",
>>> abstract =
>>> "The paper describes an implementation of deep reinforcement
>>> learning through self-supervised learning within the proof
>>> assistant HOL4. A close interaction between the machine learning
>>> modules and the HOL4 library is achieved by the choice of tree
>>> neural networks (TNNs) as machine learning models and the internal
>>> use of HOL4 terms to represent tree structures of TNNs. Recursive
>>> improvement is possible when a given task is expressed as a search
>>> problem. In this case, a Monte Carlo Tree Search (MCTS) algorithm
>>> guided by a TNN can be used to explore the search space and
>>> produce better examples for training the next TNN. As an
>>> illustration, tasks over propositional and arithmetical terms,
>>> representative of fundamental theorem proving techniques, are
>>> specified and learned: truth estimation, end-to-end computation,
>>> term rewriting and term synthesis.",
>>> paper = "Gaut19.pdf"
>>> }
>>>
>>> @misc{Lamp19,
>>> author = "Lample, Guillaume and Charton, Francois",
>>> title = {{Deep Learning for Symbolic Mathematics}},
>>> year = "2019",
>>> link = "\url{https://arxiv.org/pdf/1912.01412.pdf}",
>>> link = "\url{https://www.youtube.com/watch?v=O_sHHG5_lr8}",
>>> abstract =
>>> "Neural networks have a reputation for being better at solving
>>> statistical or approximate problems than at performing
>>> calculations or working with symbolic data. In this paper, we show
>>> that they can be surprisingly good at more elaborated tasks in
>>> mathematics, such as symbolic integration and solving differential
>>> equations. We propose a syntax for representing mathematical
>>> problems, and methods for generating large datasets that can be
>>> used to train sequence-to-sequence models. We achieve results that
>>> outperform commercial Computer Algebra Systems such as Matlab or
>>> Mathematica.",
>>> paper = "Lamp19.pdf",
>>> keywords = "printed, DONE"
>>> }
>>>
>>> @misc{Olsa19,
>>> author = "Olsak, Miroslav and Kaliszyk, Cezary and Urban, Josef",
>>> title = {{Property Invariant Embedding for Automated Reasoning}},
>>> year = "2019",
>>> link = "\url{https://arxiv.org/pdf/1911.12073.pdf}",
>>> abstract =
>>> "Automated reasoning and theorem proving have recently become
>>> major challenges for machine learning. In other domains,
>>> representations that are able to abstract over unimportant
>>> transformations, such as abstraction over translations and
>>> rotations in vision, are becoming more common. Standard methods of
>>> embedding mathematical formulas for learning theorem proving are
>>> however yet unable to handle many important transformations. In
>>> particular, embedding previously unseen labels, that often arise
>>> in definitional encodings and in Skolemizatin, has been very weak
>>> so far. Similar problems appear when tranferring knowledge between
>>> known symbols.
>>>
>>> We propose a novel encoding of formulas that extends existing
>>> graph neural network models. This encoding represents symbols only
>>> by nodes in the graph, without giving the network any knowledge of
>>> the original labels. We provide additional links between such
>>> nodes that allow the network to recover the meaning and therefore
>>> correctly embed such nodes irrespective of the given labels. We
>>> test the proposed encoding in an automated theorem prover based on
>>> the tableaux connection calculus, and show that it improves on the
>>> best characterizations used so far. The encoding is further
>>> evaluated on the premise selection task and a newly introduced
>>> symbol guessing task, and shown to correctly predict 65\% of the
>>> symbol names.",
>>> paper = "Olsa19.pdf"
>>> }
>>>
>>> @misc{Piot19,
>>> author = "Piotrowski, Bartosz and Brown, Chad E. and
>>> Kaliszyk, Cezary",
>>> title = {{Can Neural Networks Learn Symbolic Rewriting?}},
>>> year = "2019",
>>> link = "\url{https://arxiv.org/pdf/1911.04783.pdf}",
>>> abstract =
>>> "This work investigates if the current neural architectures are
>>> adequate for learning symbolic rewriting. Two kinds of data sets
>>> are proposed for this research -- one based on automated proofs
>>> and the other being a synthetic set of polynomial terms. The
>>> experiments with use of the current neural machine translation
>>> models are performed and its results are discussed. Ideas for
>>> extending this line of research are proposed and its relevance is
>>> motivated.",
>>> paper = "Piot19.pdf"
>>> }
>>>
>>> @misc{Sanc19,
>>> author = "Sanchez-Stern, Alex and Alhessi, Yousef and Saul, Lawrence
>>> and Lerner, Sorin",
>>> title = {{Generating Correctness Proofs with Neural Networks}},
>>> year = "2019",
>>> link = "\url{https://arxiv.org/pdf/1907.07794.pdf}",
>>> abstract =
>>> "Foundational verification allows programmers to build software
>>> which has been empirically shown to have high levels of assurance
>>> in a variety of important domains. However, the cost of producing
>>> foundationally verified software remains prohibitively high for
>>> most projects, as it requires significant manual effort by highly
>>> trained experts. In this paper we present Proverbot9001 a proof
>>> search system using machine learning techniques to produce proofs
>>> of software correctness in interactive theorem provers. We
>>> deomonstrate Proverbot9001 on the proof obligations from a large
>>> practical proof project, the CompCert verified C compiler, and
>>> show that it can effectively automate what was previously manual
>>> proofs, automatically solving 15.77\% of proofs in our test
>>> dataset. This corresponds to an over 3X improvement over the prior
>>> state of the art machine learning technique for generating proofs
>>> in Coq.",
>>> paper = "Sanc19.pdf"
>>> }
>>>
>>> @misc{Wang19a,
>>> author = "Wang, Qingxiang and Brown, Chad and Kaliszyk, Cezary and
>>> Urban, Josef",
>>> title = {{Exploration of Neural Machine Translation in
>>> Autoformalization of Mathematics in Mizar}},
>>> year = "2019",
>>> link = "\url{https://arxiv.org/pdf/1912.02636.pdf}",
>>> abstract =
>>> "In this paper we share several experiments trying to
>>> automatically translate informal mathematics into formal
>>> mathematics. In our context informal mathematics refers to
>>> human-written mathematical sentences in the LaTeX format; and
>>> formal mathematics refers to statements in the Mizar language. We
>>> conducted our experiments against three established neural
>>> network-based machine translation models that are know to deliver
>>> competitive results on translating between natural languages. To
>>> train these models we also prepared four informal-to-formal
>>> datasets. We compare and analyze our results according to whether
>>> the model is supervised or unsupervised. In order to augment the
>>> data available for auto-formalization and improve the results, we
>>> develop a custom type-elaboration mechanism and integrate it into
>>> the supervised translation.",
>>> paper = "Wang19a.pdf"
>>> }
>>>
>>>
>>>
>>>
>>>
>>>
--000000000000c3745f05d5397925
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

=

It was interesting because they could "round trip" the solution=
by

proven theorem is my holy grail. If there was a way to form a

Tim

<= /div>

generate "proven code" from a proof system? (LEAN)

)
id 1n6cqC-0005A0-Hd
for axiom-developer@nongnu.org; Sun, 09 Jan 2022 13:22:52 -0500
Received: from [2a00:1450:4864:20::32c] (port=53958
helo=mail-wm1-x32c.google.com)
by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
(Exim 4.90_1) (envelope-from )
id 1n6cq8-0007et-9o
for axiom-developer@nongnu.org; Sun, 09 Jan 2022 13:22:52 -0500
Received: by mail-wm1-x32c.google.com with SMTP id l4so7366196wmq.3
for ; Sun, 09 Jan 2022 10:22:43 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=cmu.edu; s=google-2021;
h=mime-version:references:in-reply-to:from:date:message-id:subject:to
:cc; bh=kScvr7wcaSc0sVBnhNdAyiAmV5l8MF/+kCdXC1QIkRI=;
b=cLDsnqAA8tSBqrzCmvl/gZ5QUtgrZKg7RQzJPlu1mlhtQonWeIJj/GOfMWLkKMQ/81
TKEQSmms/vCx1ywlR2MMyEeLB/dJ+dJOR+3j/hGXJRD2Lv+P4Gf6cRLU0zq111CARBiu
2wBguYZHYEn/xhSiJiAMlaFWMa2nx31Aa3GVnHbjB8b+t9qlfSx7M4YINMtpXOm/VYMd
YbfcEq9wdSyGS00CN1gJ4I6DwodBJAgtw0OrSt4XFHiIh+psZFh5oR1UxfddX7nhtUFS
nOrjwL2j9DNHD/GTNMjD+Ph82NXjkdEAJoT5199hMj7M/tz4iyzxispA+GRbx97f3WZy
b8ig==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=1e100.net; s=20210112;
h=x-gm-message-state:mime-version:references:in-reply-to:from:date
:message-id:subject:to:cc;
bh=kScvr7wcaSc0sVBnhNdAyiAmV5l8MF/+kCdXC1QIkRI=;
b=AWoqzZyaPQDQuMoUweqDfzH4TQMbFESGPARSoJRSIX1pbS1mlUPGLBkddw85mmAxoQ
UGucTJUjCi2JPrbYSQqoFG4rMHBb9zB1p4ddCZMiesnMkWENBCdKBRqxl+PeI3R2J88W
9xUfC4Pl8lrIrO8U8QdQwu3kNn37AhIqb0QIGeb0pabHA6kuL0X9Zblp3IjuwTOjEBF/
If59u9/Uqetv7md7uBcr5q/IA4xj9+Bq2s8ptoVHgkRFIB7E+KDTyX8INaCjBKhBkHwK
HREG+EenXwMZ9gfRQcsEwYdwP5EEUeJS8e1+UIwVDGvM1/f54F+6apcZFuhkNoy8t6TT
y0bw==
X-Gm-Message-State: AOAM532Uy7Shw4xJE0S1anlJ6HNjEXa7XNLhy6lfFZ0Eilko8kPIP3Xy
GVBzg0CQHsGupGpkkyf/KQtw2b2VZEdzvwdOynk4zw==
X-Google-Smtp-Source: ABdhPJyWuLxJ+MwJmETUyZbcviIgfME4PZ2yWg9lmzpTvT2Vi1onk1D85kP4/THNDS7ukG98Hkk+0bx9K636fz7DbmQ=
X-Received: by 2002:a05:600c:2215:: with SMTP id
z21mr19158142wml.119.1641752562062;
Sun, 09 Jan 2022 10:22:42 -0800 (PST)
MIME-Version: 1.0
References:
In-Reply-To:
From: Jeremy Avigad
Date: Sun, 9 Jan 2022 13:22:31 -0500
Message-ID:
Subject: Re: A NN Solves and Generates Math Problems
To: Tim Daly
Cc: Frank Pfenning , Prof Robert Harper ,
mcarneir , axiom-dev
Content-Type: multipart/alternative; boundary="000000000000456b4a05d52a4e53"
X-Host-Lookup-Failed: Reverse DNS lookup failed for 2a00:1450:4864:20::32c
(failed)
Received-SPF: pass client-ip=2a00:1450:4864:20::32c;
envelope-from=avigad@andrew.cmu.edu; helo=mail-wm1-x32c.google.com
X-Spam_score_int: -12
X-Spam_score: -1.3
X-Spam_bar: -
X-Spam_report: (-1.3 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1,
DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, HTML_MESSAGE=0.001,
RCVD_IN_DNSWL_NONE=-0.0001, RDNS_NONE=0.793, SPF_HELO_NONE=0.001,
SPF_PASS=-0.001 autolearn=no autolearn_force=no
X-Spam_action: no action
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.29
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Sun, 09 Jan 2022 18:22:52 -0000
--000000000000456b4a05d52a4e53
Content-Type: text/plain; charset="UTF-8"
Thanks for this! It seems to speak to the success of the OpenAI Codex more
than anything else, but the results are impressive.
Bartosz Piotrowski, a PhD student and author of one of the papers you
cited, will be visiting Carnegie Mellon for a few months this spring.
Best wishes,
Jeremy
On Thu, Jan 6, 2022 at 10:30 AM Tim Daly wrote:
> This is an interesting paper (especially given that it
> is work under Gilbert Strang):
>
> A Neural Network Solves and Generates Mathematics
> Problems by Progam Synthesis: Calculus, Differential
> Equations, Linear Algebra, and More.
> https://arxiv.org/pdf/2112.15594.pdf
>
> "This work shows that a neural network that generates
> programs (i.e. program synthesis) is the key to solving
> math and STEM courses at scale, as it turns question
> answering into a programming task."
>
> This seems interesting from several aspects:
>
> 1) Can this be applied to logic systems? Can it help
> generate "proven code" from a proof system? (LEAN)
>
> 2) Can it be applied in programs like NuPRL / RedPRL?
> (Innovations in Computational Type Theory using Nuprl
> Journal of Applied Logic 4 (2006) pp 428--469
>
> https://reader.elsevier.com/reader/sd/pii/S1570868305000704?token=C11F82ADA94390097338EF7E421A4D9DFEF909336A451BF51D3099EDF1025177323CCD7B46510F77FFC4955D0AC6724F&originRegion=us-east-1&originCreation=20220106150458
>
> 3) Can the type of an object be inferred by casting it as a
> question in mathematics? Is the generated program correctly
> typed?
>
> 4) Can this be layered on MetaMath (LEAN) or FDL (Nuprl)
> to generate logically equivalent code?
>
> 5) Can this be applied to gradual typing?
>
> In any case, this represents an interesting "interdisciplinary"
> effort connecting the math department and CS.
>
> Tim
>
>
>
> There are various connections to Neural Networks and Math:
>
> @misc{Crou19,
> author = "Crouse, Maxwell and Whitehead, Spencer and
> Abdelaziz, Ibrahim and Makni, Bassem and
> Cornelio, Cristina and Kapanipathi, Pavan and
> Pell, Edwin and Srinivas, Kavitha and
> Thost, Veronika and Witbrock, Michael and
> Fokoue, Achille",
> title = {{A Deep Reinforcement Learning Base Approach to Learning
> Transferable Proof Guidance Strategies}},
> year = "2019",
> linke = "\url{https://arxiv.org/pdf/1911.02065.pdf}",
> abstract =
> "Traditional first-order logic (FOL) reasoning systems usually
> rely on manual heuristics for proof guidance. We propose TRAIL: a
> system that learns to perform proof guidance using reinforcement
> learning. A key design principle of our system is that it is
> general enough to allow transfer to problems in different domains
> that do not share the same vocabulary of the training set. To do
> so, we developed a novel representation of the internal state of a
> prover in terms of clauses and inference actions, and a novel
> neural-based attention mechanism to learn interactions between
> clauses. We demonstrate that this approach enables the system to
> generalize from training to test data across domains with
> different vocabularies, suggesting that the nerual architecture in
> TRAIL is well suited for representing and processing of logical
> formalisms.",
> paper = "Crou19.pdf"
> }
>
> @misc{Crou19a,
> author = "Crouse, Maxwell and Abdelaziz, Ibrahim and
> Cornelio, Cristina and Thost, Veronika and
> Wu, Lingfei and Forbus, Kenneth and Fokoue, Achille",
> title = {{Improving Graph Neural Network Representations of Logical
> Formulae with Subgraph Pooling}},
> year = "2019",
> linke = "\url{https://arxiv.org/pdf/1911.06904.pdf}",
> abstract =
> "Recent advances in the integration of deep learning with
> automated theorem proving have centered around the representation
> of graph-structured representations, in large part driven by the
> rapidly emerging body of research in geometric deep
> learning. Typically, structure-aware neural methods for embedding
> logical formulae have been variants of either Tree LSTMs or
> GNNs. While more effective than character and token-level
> approaches, such methods have often made representational
> trade-offs that limited their ability to effectively represent the
> global structure of their inputs. In this work, we introduce a
> novel approach for embedding logical formulae using DAG LSTMs that
> is designed to overome the limitations of both Tree LSTMs and
> GNNs. The effectiveness of the proposed framework is demonstrated
> on the tasks of premise selection and proof step classification
> where it achieves the state-of-the-art performance on two standard
> datasets.",
> paper = "Crou19a.pdf"
> }
>
> @misc{Gaut19,
> author = "Gauthier, Thibault",
> title = {{Deep Reinforcement Learning in HOL4}},
> year = "2019",
> link = "\url{https://arxiv.org/pdf/1910.11797.pdf}",
> abstract =
> "The paper describes an implementation of deep reinforcement
> learning through self-supervised learning within the proof
> assistant HOL4. A close interaction between the machine learning
> modules and the HOL4 library is achieved by the choice of tree
> neural networks (TNNs) as machine learning models and the internal
> use of HOL4 terms to represent tree structures of TNNs. Recursive
> improvement is possible when a given task is expressed as a search
> problem. In this case, a Monte Carlo Tree Search (MCTS) algorithm
> guided by a TNN can be used to explore the search space and
> produce better examples for training the next TNN. As an
> illustration, tasks over propositional and arithmetical terms,
> representative of fundamental theorem proving techniques, are
> specified and learned: truth estimation, end-to-end computation,
> term rewriting and term synthesis.",
> paper = "Gaut19.pdf"
> }
>
> @misc{Lamp19,
> author = "Lample, Guillaume and Charton, Francois",
> title = {{Deep Learning for Symbolic Mathematics}},
> year = "2019",
> link = "\url{https://arxiv.org/pdf/1912.01412.pdf}",
> link = "\url{https://www.youtube.com/watch?v=O_sHHG5_lr8}",
> abstract =
> "Neural networks have a reputation for being better at solving
> statistical or approximate problems than at performing
> calculations or working with symbolic data. In this paper, we show
> that they can be surprisingly good at more elaborated tasks in
> mathematics, such as symbolic integration and solving differential
> equations. We propose a syntax for representing mathematical
> problems, and methods for generating large datasets that can be
> used to train sequence-to-sequence models. We achieve results that
> outperform commercial Computer Algebra Systems such as Matlab or
> Mathematica.",
> paper = "Lamp19.pdf",
> keywords = "printed, DONE"
> }
>
> @misc{Olsa19,
> author = "Olsak, Miroslav and Kaliszyk, Cezary and Urban, Josef",
> title = {{Property Invariant Embedding for Automated Reasoning}},
> year = "2019",
> link = "\url{https://arxiv.org/pdf/1911.12073.pdf}",
> abstract =
> "Automated reasoning and theorem proving have recently become
> major challenges for machine learning. In other domains,
> representations that are able to abstract over unimportant
> transformations, such as abstraction over translations and
> rotations in vision, are becoming more common. Standard methods of
> embedding mathematical formulas for learning theorem proving are
> however yet unable to handle many important transformations. In
> particular, embedding previously unseen labels, that often arise
> in definitional encodings and in Skolemizatin, has been very weak
> so far. Similar problems appear when tranferring knowledge between
> known symbols.
>
> We propose a novel encoding of formulas that extends existing
> graph neural network models. This encoding represents symbols only
> by nodes in the graph, without giving the network any knowledge of
> the original labels. We provide additional links between such
> nodes that allow the network to recover the meaning and therefore
> correctly embed such nodes irrespective of the given labels. We
> test the proposed encoding in an automated theorem prover based on
> the tableaux connection calculus, and show that it improves on the
> best characterizations used so far. The encoding is further
> evaluated on the premise selection task and a newly introduced
> symbol guessing task, and shown to correctly predict 65\% of the
> symbol names.",
> paper = "Olsa19.pdf"
> }
>
> @misc{Piot19,
> author = "Piotrowski, Bartosz and Brown, Chad E. and
> Kaliszyk, Cezary",
> title = {{Can Neural Networks Learn Symbolic Rewriting?}},
> year = "2019",
> link = "\url{https://arxiv.org/pdf/1911.04783.pdf}",
> abstract =
> "This work investigates if the current neural architectures are
> adequate for learning symbolic rewriting. Two kinds of data sets
> are proposed for this research -- one based on automated proofs
> and the other being a synthetic set of polynomial terms. The
> experiments with use of the current neural machine translation
> models are performed and its results are discussed. Ideas for
> extending this line of research are proposed and its relevance is
> motivated.",
> paper = "Piot19.pdf"
> }
>
> @misc{Sanc19,
> author = "Sanchez-Stern, Alex and Alhessi, Yousef and Saul, Lawrence
> and Lerner, Sorin",
> title = {{Generating Correctness Proofs with Neural Networks}},
> year = "2019",
> link = "\url{https://arxiv.org/pdf/1907.07794.pdf}",
> abstract =
> "Foundational verification allows programmers to build software
> which has been empirically shown to have high levels of assurance
> in a variety of important domains. However, the cost of producing
> foundationally verified software remains prohibitively high for
> most projects, as it requires significant manual effort by highly
> trained experts. In this paper we present Proverbot9001 a proof
> search system using machine learning techniques to produce proofs
> of software correctness in interactive theorem provers. We
> deomonstrate Proverbot9001 on the proof obligations from a large
> practical proof project, the CompCert verified C compiler, and
> show that it can effectively automate what was previously manual
> proofs, automatically solving 15.77\% of proofs in our test
> dataset. This corresponds to an over 3X improvement over the prior
> state of the art machine learning technique for generating proofs
> in Coq.",
> paper = "Sanc19.pdf"
> }
>
> @misc{Wang19a,
> author = "Wang, Qingxiang and Brown, Chad and Kaliszyk, Cezary and
> Urban, Josef",
> title = {{Exploration of Neural Machine Translation in
> Autoformalization of Mathematics in Mizar}},
> year = "2019",
> link = "\url{https://arxiv.org/pdf/1912.02636.pdf}",
> abstract =
> "In this paper we share several experiments trying to
> automatically translate informal mathematics into formal
> mathematics. In our context informal mathematics refers to
> human-written mathematical sentences in the LaTeX format; and
> formal mathematics refers to statements in the Mizar language. We
> conducted our experiments against three established neural
> network-based machine translation models that are know to deliver
> competitive results on translating between natural languages. To
> train these models we also prepared four informal-to-formal
> datasets. We compare and analyze our results according to whether
> the model is supervised or unsupervised. In order to augment the
> data available for auto-formalization and improve the results, we
> develop a custom type-elaboration mechanism and integrate it into
> the supervised translation.",
> paper = "Wang19a.pdf"
> }
>
>
>
>
>
>
--000000000000456b4a05d52a4e53
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
at all clear how that could be possible using a Neural Net.

2) Can it be applied in programs like NuPRL / RedPRL?<=
/div>

--000000000000f134e205d4eb8a72--
From MAILER-DAEMON Sun Jan 09 13:22:54 2022
Received: from list by lists.gnu.org with archive (Exim 4.90_1)
id 1n6cqE-0005AH-BM
for mharc-axiom-developer@gnu.org; Sun, 09 Jan 2022 13:22:54 -0500
Received: from eggs.gnu.org ([209.51.188.92]:45866)
by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from (Innovations in Computational Type Theory using Nuprl

J=
ournal of Applied Logic 4 (2006) pp 428--469

3) Can the type of an object be inferred=
by casting it as a

question in mathematics? Is the generated pro=
gram correctly

typed?

4) Can this be lay=
ered on MetaMath (LEAN) or FDL (Nuprl)

to generate logically equi=
valent code?

5) Can this be applied to gradual typ=
ing?

In any case, this represents an interesti=
ng "interdisciplinary"

effort connecting the math depar=
tment and CS.

Tim

There are various connections to Neural Networks and=
Math:

@misc{Crou19,

=C2=A0 author =3D "Cr= ouse, Maxwell and Whitehead, Spencer and

=C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 Abdelaziz, Ibrahim and Makni, Bassem and

=C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 Cornelio, Cristina and Kapanipathi, Pavan and**=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Pell, Edwin and Srinivas, Kavit=
ha and**

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Thost, Veronika and Wit= brock, Michael and

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Fokoue, Ach= ille",

=C2=A0 title =3D {{A Deep Reinforcement Learning Base Approa= ch to Learning

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0Transferable Pro= of Guidance Strategies}},

=C2=A0 year =3D "2019",

=C2=A0 li= nke =3D "\url{https:/= /arxiv.org/pdf/1911.02065.pdf}",

=C2=A0 abstract =3D

=C2=A0= =C2=A0 "Traditional first-order logic (FOL) reasoning systems usually=

=C2=A0 =C2=A0 rely on manual heuristics for proof guidance. We propose = TRAIL: a

=C2=A0 =C2=A0 system that learns to perform proof guidance usin= g reinforcement

=C2=A0 =C2=A0 learning. A key design principle of our sy= stem is that it is

=C2=A0 =C2=A0 general enough to allow transfer to pro= blems in different domains

=C2=A0 =C2=A0 that do not share the same voca= bulary of the training set. To do

=C2=A0 =C2=A0 so, we developed a novel= representation of the internal state of a

=C2=A0 =C2=A0 prover in terms= of clauses and inference actions, and a novel

=C2=A0 =C2=A0 neural-base= d attention mechanism to learn interactions between

=C2=A0 =C2=A0 clause= s. We demonstrate that this approach enables the system to

=C2=A0 =C2=A0= generalize from training to test data across domains with

=C2=A0 =C2=A0= different vocabularies, suggesting that the nerual architecture in

=C2= =A0 =C2=A0 TRAIL is well suited for representing and processing of logical<= br>=C2=A0 =C2=A0 formalisms.",

=C2=A0 paper =3D "Crou19.pdf&qu= ot;

=C2=A0 author =3D "Cr= ouse, Maxwell and Whitehead, Spencer and

=C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 Abdelaziz, Ibrahim and Makni, Bassem and

=C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 Cornelio, Cristina and Kapanipathi, Pavan and

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Thost, Veronika and Wit= brock, Michael and

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Fokoue, Ach= ille",

=C2=A0 title =3D {{A Deep Reinforcement Learning Base Approa= ch to Learning

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0Transferable Pro= of Guidance Strategies}},

=C2=A0 year =3D "2019",

=C2=A0 li= nke =3D "\url{https:/= /arxiv.org/pdf/1911.02065.pdf}",

=C2=A0 abstract =3D

=C2=A0= =C2=A0 "Traditional first-order logic (FOL) reasoning systems usually=

=C2=A0 =C2=A0 rely on manual heuristics for proof guidance. We propose = TRAIL: a

=C2=A0 =C2=A0 system that learns to perform proof guidance usin= g reinforcement

=C2=A0 =C2=A0 learning. A key design principle of our sy= stem is that it is

=C2=A0 =C2=A0 general enough to allow transfer to pro= blems in different domains

=C2=A0 =C2=A0 that do not share the same voca= bulary of the training set. To do

=C2=A0 =C2=A0 so, we developed a novel= representation of the internal state of a

=C2=A0 =C2=A0 prover in terms= of clauses and inference actions, and a novel

=C2=A0 =C2=A0 neural-base= d attention mechanism to learn interactions between

=C2=A0 =C2=A0 clause= s. We demonstrate that this approach enables the system to

=C2=A0 =C2=A0= generalize from training to test data across domains with

=C2=A0 =C2=A0= different vocabularies, suggesting that the nerual architecture in

=C2= =A0 =C2=A0 TRAIL is well suited for representing and processing of logical<= br>=C2=A0 =C2=A0 formalisms.",

=C2=A0 paper =3D "Crou19.pdf&qu= ot;

}

@misc{Crou19a,

=C2=A0 autho= r =3D "Crouse, Maxwell and Abdelaziz, Ibrahim and

=C2=A0 =C2=A0 =C2= =A0 =C2=A0 =C2=A0 =C2=A0 Cornelio, Cristina and Thost, Veronika and

=C2= =A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Wu, Lingfei and Forbus, Kenneth and = Fokoue, Achille",

=C2=A0 title =3D {{Improving Graph Neural Network= Representations of Logical

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Fo= rmulae with Subgraph Pooling}},

=C2=A0 year =3D "2019",

=C2= =A0 linke =3D "\url{h= ttps://arxiv.org/pdf/1911.06904.pdf}",

=C2=A0 abstract =3D

= =C2=A0 =C2=A0 "Recent advances in the integration of deep learning wit= h

=C2=A0 =C2=A0 automated theorem proving have centered around the repre= sentation

=C2=A0 =C2=A0 of graph-structured representations, in large pa= rt driven by the

=C2=A0 =C2=A0 rapidly emerging body of research in geom= etric deep

=C2=A0 =C2=A0 learning. Typically, structure-aware neural met= hods for embedding

=C2=A0 =C2=A0 logical formulae have been variants of = either Tree LSTMs or

=C2=A0 =C2=A0 GNNs. While more effective than chara= cter and token-level

=C2=A0 =C2=A0 approaches, such methods have often m= ade representational

=C2=A0 =C2=A0 trade-offs that limited their ability= to effectively represent the

=C2=A0 =C2=A0 global structure of their in= puts. In this work, we introduce a

=C2=A0 =C2=A0 novel approach for embe= dding logical formulae using DAG LSTMs that

=C2=A0 =C2=A0 is designed to= overome the limitations of both Tree LSTMs and

=C2=A0 =C2=A0 GNNs. The = effectiveness of the proposed framework is demonstrated

=C2=A0 =C2=A0 on= the tasks of premise selection and proof step classification

=C2=A0 =C2= =A0 where it achieves the state-of-the-art performance on two standard

= =C2=A0 =C2=A0 datasets.",

=C2=A0 paper =3D "Crou19a.pdf"=

}

=C2=A0 autho= r =3D "Crouse, Maxwell and Abdelaziz, Ibrahim and

=C2=A0 =C2=A0 =C2= =A0 =C2=A0 =C2=A0 =C2=A0 Cornelio, Cristina and Thost, Veronika and

=C2= =A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Wu, Lingfei and Forbus, Kenneth and = Fokoue, Achille",

=C2=A0 title =3D {{Improving Graph Neural Network= Representations of Logical

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Fo= rmulae with Subgraph Pooling}},

=C2=A0 year =3D "2019",

=C2= =A0 linke =3D "\url{h= ttps://arxiv.org/pdf/1911.06904.pdf}",

=C2=A0 abstract =3D

= =C2=A0 =C2=A0 "Recent advances in the integration of deep learning wit= h

=C2=A0 =C2=A0 automated theorem proving have centered around the repre= sentation

=C2=A0 =C2=A0 of graph-structured representations, in large pa= rt driven by the

=C2=A0 =C2=A0 rapidly emerging body of research in geom= etric deep

=C2=A0 =C2=A0 learning. Typically, structure-aware neural met= hods for embedding

=C2=A0 =C2=A0 logical formulae have been variants of = either Tree LSTMs or

=C2=A0 =C2=A0 GNNs. While more effective than chara= cter and token-level

=C2=A0 =C2=A0 approaches, such methods have often m= ade representational

=C2=A0 =C2=A0 trade-offs that limited their ability= to effectively represent the

=C2=A0 =C2=A0 global structure of their in= puts. In this work, we introduce a

=C2=A0 =C2=A0 novel approach for embe= dding logical formulae using DAG LSTMs that

=C2=A0 =C2=A0 is designed to= overome the limitations of both Tree LSTMs and

=C2=A0 =C2=A0 GNNs. The = effectiveness of the proposed framework is demonstrated

=C2=A0 =C2=A0 on= the tasks of premise selection and proof step classification

=C2=A0 =C2= =A0 where it achieves the state-of-the-art performance on two standard

= =C2=A0 =C2=A0 datasets.",

=C2=A0 paper =3D "Crou19a.pdf"=

}

@misc{Gaut19,

=C2=A0 author =3D "Gau= thier, Thibault",

=C2=A0 title =3D {{Deep Reinforcement Learning in= HOL4}},

=C2=A0 year =3D "2019",

=C2=A0 link =3D "\url= {https://arxiv.org/pdf/191= 0.11797.pdf}",

=C2=A0 abstract =3D

=C2=A0 =C2=A0 "The p= aper describes an implementation of deep reinforcement

=C2=A0 =C2=A0 lea= rning through self-supervised learning within the proof

=C2=A0 =C2=A0 as= sistant HOL4. A close interaction between the machine learning

=C2=A0 = =C2=A0 modules and the HOL4 library is achieved by the choice of tree

= =C2=A0 =C2=A0 neural networks (TNNs) as machine learning models and the int= ernal

=C2=A0 =C2=A0 use of HOL4 terms to represent tree structures of TN= Ns. Recursive

=C2=A0 =C2=A0 improvement is possible when a given task is= expressed as a search

=C2=A0 =C2=A0 problem. In this case, a Monte Carl= o Tree Search (MCTS) algorithm

=C2=A0 =C2=A0 guided by a TNN can be used= to explore the search space and

=C2=A0 =C2=A0 produce better examples f= or training the next TNN. As an

=C2=A0 =C2=A0 illustration, tasks over p= ropositional and arithmetical terms,

=C2=A0 =C2=A0 representative of fun= damental theorem proving techniques, are

=C2=A0 =C2=A0 specified and lea= rned: truth estimation, end-to-end computation,

=C2=A0 =C2=A0 term rewri= ting and term synthesis.",

=C2=A0 paper =3D "Gaut19.pdf"<= br>}

=C2=A0 author =3D "Gau= thier, Thibault",

=C2=A0 title =3D {{Deep Reinforcement Learning in= HOL4}},

=C2=A0 year =3D "2019",

=C2=A0 link =3D "\url= {https://arxiv.org/pdf/191= 0.11797.pdf}",

=C2=A0 abstract =3D

=C2=A0 =C2=A0 "The p= aper describes an implementation of deep reinforcement

=C2=A0 =C2=A0 lea= rning through self-supervised learning within the proof

=C2=A0 =C2=A0 as= sistant HOL4. A close interaction between the machine learning

=C2=A0 = =C2=A0 modules and the HOL4 library is achieved by the choice of tree

= =C2=A0 =C2=A0 neural networks (TNNs) as machine learning models and the int= ernal

=C2=A0 =C2=A0 use of HOL4 terms to represent tree structures of TN= Ns. Recursive

=C2=A0 =C2=A0 improvement is possible when a given task is= expressed as a search

=C2=A0 =C2=A0 problem. In this case, a Monte Carl= o Tree Search (MCTS) algorithm

=C2=A0 =C2=A0 guided by a TNN can be used= to explore the search space and

=C2=A0 =C2=A0 produce better examples f= or training the next TNN. As an

=C2=A0 =C2=A0 illustration, tasks over p= ropositional and arithmetical terms,

=C2=A0 =C2=A0 representative of fun= damental theorem proving techniques, are

=C2=A0 =C2=A0 specified and lea= rned: truth estimation, end-to-end computation,

=C2=A0 =C2=A0 term rewri= ting and term synthesis.",

=C2=A0 paper =3D "Gaut19.pdf"<= br>}

@misc{Lamp19,

=C2=A0 author =3D "Lamp= le, Guillaume and Charton, Francois",

=C2=A0 title =3D {{Deep Learn= ing for Symbolic Mathematics}},

=C2=A0 year =3D "2019",

=C2= =A0 link =3D "\url{ht= tps://arxiv.org/pdf/1912.01412.pdf}",

=C2=A0 link =3D "\ur= l{https://www.you= tube.com/watch?v=3DO_sHHG5_lr8}",

=C2=A0 abstract =3D

=C2=A0= =C2=A0 "Neural networks have a reputation for being better at solving=

=C2=A0 =C2=A0 statistical or approximate problems than at performing

=C2=A0 =C2=A0 calculations or working with symbolic data. In this paper, w= e show

=C2=A0 =C2=A0 that they can be surprisingly good at more elaborat= ed tasks in

=C2=A0 =C2=A0 mathematics, such as symbolic integration and = solving differential

=C2=A0 =C2=A0 equations. We propose a syntax for re= presenting mathematical

=C2=A0 =C2=A0 problems, and methods for generati= ng large datasets that can be

=C2=A0 =C2=A0 used to train sequence-to-se= quence models. We achieve results that

=C2=A0 =C2=A0 outperform commerci= al Computer Algebra Systems such as Matlab or

=C2=A0 =C2=A0 Mathematica.= ",

=C2=A0 paper =3D "Lamp19.pdf",

=C2=A0 keywords =3D = "printed, DONE"

}

=C2=A0 author =3D "Lamp= le, Guillaume and Charton, Francois",

=C2=A0 title =3D {{Deep Learn= ing for Symbolic Mathematics}},

=C2=A0 year =3D "2019",

=C2= =A0 link =3D "\url{ht= tps://arxiv.org/pdf/1912.01412.pdf}",

=C2=A0 link =3D "\ur= l{https://www.you= tube.com/watch?v=3DO_sHHG5_lr8}",

=C2=A0 abstract =3D

=C2=A0= =C2=A0 "Neural networks have a reputation for being better at solving=

=C2=A0 =C2=A0 statistical or approximate problems than at performing

=C2=A0 =C2=A0 calculations or working with symbolic data. In this paper, w= e show

=C2=A0 =C2=A0 that they can be surprisingly good at more elaborat= ed tasks in

=C2=A0 =C2=A0 mathematics, such as symbolic integration and = solving differential

=C2=A0 =C2=A0 equations. We propose a syntax for re= presenting mathematical

=C2=A0 =C2=A0 problems, and methods for generati= ng large datasets that can be

=C2=A0 =C2=A0 used to train sequence-to-se= quence models. We achieve results that

=C2=A0 =C2=A0 outperform commerci= al Computer Algebra Systems such as Matlab or

=C2=A0 =C2=A0 Mathematica.= ",

=C2=A0 paper =3D "Lamp19.pdf",

=C2=A0 keywords =3D = "printed, DONE"

}

@misc{Olsa19,

= =C2=A0 author =3D "Olsak, Miroslav and Kaliszyk, Cezary and Urban, Jos= ef",

=C2=A0 title =3D {{Property Invariant Embedding for Automated = Reasoning}},

=C2=A0 year =3D "2019",

=C2=A0 link =3D "= \url{https://arxiv.org/pdf= /1911.12073.pdf}",

=C2=A0 abstract =3D

=C2=A0 =C2=A0 "A= utomated reasoning and theorem proving have recently become

=C2=A0 =C2= =A0 major challenges for machine learning. In other domains,

=C2=A0 =C2= =A0 representations that are able to abstract over unimportant

=C2=A0 = =C2=A0 transformations, such as abstraction over translations and

=C2=A0= =C2=A0 rotations in vision, are becoming more common. Standard methods of<= br>=C2=A0 =C2=A0 embedding mathematical formulas for learning theorem provi= ng are

=C2=A0 =C2=A0 however yet unable to handle many important transfo= rmations. In

=C2=A0 =C2=A0 particular, embedding previously unseen label= s, that often arise

=C2=A0 =C2=A0 in definitional encodings and in Skole= mizatin, has been very weak

=C2=A0 =C2=A0 so far. Similar problems appea= r when tranferring knowledge between

=C2=A0 =C2=A0 known symbols.

=C2=A0 =C2=A0 We propose a novel encoding of formulas that extends existin= g

=C2=A0 =C2=A0 graph neural network models. This encoding represents sy= mbols only

=C2=A0 =C2=A0 by nodes in the graph, without giving the netwo= rk any knowledge of

=C2=A0 =C2=A0 the original labels. We provide additi= onal links between such

=C2=A0 =C2=A0 nodes that allow the network to re= cover the meaning and therefore

=C2=A0 =C2=A0 correctly embed such nodes= irrespective of the given labels. We

=C2=A0 =C2=A0 test the proposed en= coding in an automated theorem prover based on

=C2=A0 =C2=A0 the tableau= x connection calculus, and show that it improves on the

=C2=A0 =C2=A0 be= st characterizations used so far. The encoding is further

=C2=A0 =C2=A0 = evaluated on the premise selection task and a newly introduced

=C2=A0 = =C2=A0 symbol guessing task, and shown to correctly predict 65\% of the

= =C2=A0 =C2=A0 symbol names.",

=C2=A0 paper =3D "Olsa19.pdf&quo= t;

}

= =C2=A0 author =3D "Olsak, Miroslav and Kaliszyk, Cezary and Urban, Jos= ef",

=C2=A0 title =3D {{Property Invariant Embedding for Automated = Reasoning}},

=C2=A0 year =3D "2019",

=C2=A0 link =3D "= \url{https://arxiv.org/pdf= /1911.12073.pdf}",

=C2=A0 abstract =3D

=C2=A0 =C2=A0 "A= utomated reasoning and theorem proving have recently become

=C2=A0 =C2= =A0 major challenges for machine learning. In other domains,

=C2=A0 =C2= =A0 representations that are able to abstract over unimportant

=C2=A0 = =C2=A0 transformations, such as abstraction over translations and

=C2=A0= =C2=A0 rotations in vision, are becoming more common. Standard methods of<= br>=C2=A0 =C2=A0 embedding mathematical formulas for learning theorem provi= ng are

=C2=A0 =C2=A0 however yet unable to handle many important transfo= rmations. In

=C2=A0 =C2=A0 particular, embedding previously unseen label= s, that often arise

=C2=A0 =C2=A0 in definitional encodings and in Skole= mizatin, has been very weak

=C2=A0 =C2=A0 so far. Similar problems appea= r when tranferring knowledge between

=C2=A0 =C2=A0 known symbols.

=C2=A0 =C2=A0 We propose a novel encoding of formulas that extends existin= g

=C2=A0 =C2=A0 graph neural network models. This encoding represents sy= mbols only

=C2=A0 =C2=A0 by nodes in the graph, without giving the netwo= rk any knowledge of

=C2=A0 =C2=A0 the original labels. We provide additi= onal links between such

=C2=A0 =C2=A0 nodes that allow the network to re= cover the meaning and therefore

=C2=A0 =C2=A0 correctly embed such nodes= irrespective of the given labels. We

=C2=A0 =C2=A0 test the proposed en= coding in an automated theorem prover based on

=C2=A0 =C2=A0 the tableau= x connection calculus, and show that it improves on the

=C2=A0 =C2=A0 be= st characterizations used so far. The encoding is further

=C2=A0 =C2=A0 = evaluated on the premise selection task and a newly introduced

=C2=A0 = =C2=A0 symbol guessing task, and shown to correctly predict 65\% of the

= =C2=A0 =C2=A0 symbol names.",

=C2=A0 paper =3D "Olsa19.pdf&quo= t;

}

@misc{Piot19,

=C2=A0 author =3D "Piotrows= ki, Bartosz and Brown, Chad E. and

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0 Kaliszyk, Cezary",

=C2=A0 title =3D {{Can Neural Networks Le= arn Symbolic Rewriting?}},

=C2=A0 year =3D "2019",

=C2=A0 l= ink =3D "\url{https:/= /arxiv.org/pdf/1911.04783.pdf}",

=C2=A0 abstract =3D

=C2=A0 = =C2=A0 "This work investigates if the current neural architectures are=

=C2=A0 =C2=A0 adequate for learning symbolic rewriting. Two kinds of da= ta sets

=C2=A0 =C2=A0 are proposed for this research -- one based on aut= omated proofs

=C2=A0 =C2=A0 and the other being a synthetic set of polyn= omial terms. The

=C2=A0 =C2=A0 experiments with use of the current neura= l machine translation

=C2=A0 =C2=A0 models are performed and its results= are discussed. Ideas for

=C2=A0 =C2=A0 extending this line of research = are proposed and its relevance is

=C2=A0 =C2=A0 motivated.",

= =C2=A0 paper =3D "Piot19.pdf"

}

@misc{Sanc19,

=C2=A0= author =3D "Sanchez-Stern, Alex and Alhessi, Yousef and Saul, Lawrenc= e

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 and Lerner, Sorin",

=C2=A0 title =3D {{Generating Correctness Proofs with Neural Networks}},**=C2=A0 year =3D "2019",**

=C2=A0 link =3D "\url{https://arxiv.org/pdf/1907.07794.= pdf}",

=C2=A0 abstract =3D

=C2=A0 =C2=A0 "Foundational = verification allows programmers to build software

=C2=A0 =C2=A0 which ha= s been empirically shown to have high levels of assurance

=C2=A0 =C2=A0 = in a variety of important domains. However, the cost of producing

=C2=A0= =C2=A0 foundationally verified software remains prohibitively high for

= =C2=A0 =C2=A0 most projects, as it requires significant manual effort by hi= ghly

=C2=A0 =C2=A0 trained experts. In this paper we present Proverbot90= 01 a proof

=C2=A0 =C2=A0 search system using machine learning techniques= to produce proofs

=C2=A0 =C2=A0 of software correctness in interactive = theorem provers. We

=C2=A0 =C2=A0 deomonstrate Proverbot9001 on the proo= f obligations from a large

=C2=A0 =C2=A0 practical proof project, the Co= mpCert verified C compiler, and

=C2=A0 =C2=A0 show that it can effective= ly automate what was previously manual

=C2=A0 =C2=A0 proofs, automatical= ly solving 15.77\% of proofs in our test

=C2=A0 =C2=A0 dataset. This cor= responds to an over 3X improvement over the prior

=C2=A0 =C2=A0 state of= the art machine learning technique for generating proofs

=C2=A0 =C2=A0 = in Coq.",

=C2=A0 paper =3D "Sanc19.pdf"

}

@misc= {Wang19a,

=C2=A0 author =3D "Wang, Qingxiang and Brown, Chad and Ka= liszyk, Cezary and

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Urban, Jose= f",

=C2=A0 title =3D {{Exploration of Neural Machine Translation i= n

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Autoformalization of Mathema= tics in Mizar}},

=C2=A0 year =3D "2019",

=C2=A0 link =3D &q= uot;\url{https://arxiv.org= /pdf/1912.02636.pdf}",

=C2=A0 abstract =3D

=C2=A0 =C2=A0 &qu= ot;In this paper we share several experiments trying to

=C2=A0 =C2=A0 au= tomatically translate informal mathematics into formal

=C2=A0 =C2=A0 mat= hematics. In our context informal mathematics refers to

=C2=A0 =C2=A0 hu= man-written mathematical sentences in the LaTeX format; and

=C2=A0 =C2= =A0 formal mathematics refers to statements in the Mizar language. We

= =C2=A0 =C2=A0 conducted our experiments against three established neural

=C2=A0 =C2=A0 network-based machine translation models that are know to de= liver

=C2=A0 =C2=A0 competitive results on translating between natural l= anguages. To

=C2=A0 =C2=A0 train these models we also prepared four info= rmal-to-formal

=C2=A0 =C2=A0 datasets. We compare and analyze our result= s according to whether

=C2=A0 =C2=A0 the model is supervised or unsuperv= ised. In order to augment the

=C2=A0 =C2=A0 data available for auto-form= alization and improve the results, we

=C2=A0 =C2=A0 develop a custom typ= e-elaboration mechanism and integrate it into

=C2=A0 =C2=A0 the supervis= ed translation.",

=C2=A0 paper =3D "Wang19a.pdf"

}

=

=C2=A0 author =3D "Piotrows= ki, Bartosz and Brown, Chad E. and

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0 Kaliszyk, Cezary",

=C2=A0 title =3D {{Can Neural Networks Le= arn Symbolic Rewriting?}},

=C2=A0 year =3D "2019",

=C2=A0 l= ink =3D "\url{https:/= /arxiv.org/pdf/1911.04783.pdf}",

=C2=A0 abstract =3D

=C2=A0 = =C2=A0 "This work investigates if the current neural architectures are=

=C2=A0 =C2=A0 adequate for learning symbolic rewriting. Two kinds of da= ta sets

=C2=A0 =C2=A0 are proposed for this research -- one based on aut= omated proofs

=C2=A0 =C2=A0 and the other being a synthetic set of polyn= omial terms. The

=C2=A0 =C2=A0 experiments with use of the current neura= l machine translation

=C2=A0 =C2=A0 models are performed and its results= are discussed. Ideas for

=C2=A0 =C2=A0 extending this line of research = are proposed and its relevance is

=C2=A0 =C2=A0 motivated.",

= =C2=A0 paper =3D "Piot19.pdf"

}

@misc{Sanc19,

=C2=A0= author =3D "Sanchez-Stern, Alex and Alhessi, Yousef and Saul, Lawrenc= e

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 and Lerner, Sorin",

=C2=A0 title =3D {{Generating Correctness Proofs with Neural Networks}},

=C2=A0 link =3D "\url{https://arxiv.org/pdf/1907.07794.= pdf}",

=C2=A0 abstract =3D

=C2=A0 =C2=A0 "Foundational = verification allows programmers to build software

=C2=A0 =C2=A0 which ha= s been empirically shown to have high levels of assurance

=C2=A0 =C2=A0 = in a variety of important domains. However, the cost of producing

=C2=A0= =C2=A0 foundationally verified software remains prohibitively high for

= =C2=A0 =C2=A0 most projects, as it requires significant manual effort by hi= ghly

=C2=A0 =C2=A0 trained experts. In this paper we present Proverbot90= 01 a proof

=C2=A0 =C2=A0 search system using machine learning techniques= to produce proofs

=C2=A0 =C2=A0 of software correctness in interactive = theorem provers. We

=C2=A0 =C2=A0 deomonstrate Proverbot9001 on the proo= f obligations from a large

=C2=A0 =C2=A0 practical proof project, the Co= mpCert verified C compiler, and

=C2=A0 =C2=A0 show that it can effective= ly automate what was previously manual

=C2=A0 =C2=A0 proofs, automatical= ly solving 15.77\% of proofs in our test

=C2=A0 =C2=A0 dataset. This cor= responds to an over 3X improvement over the prior

=C2=A0 =C2=A0 state of= the art machine learning technique for generating proofs

=C2=A0 =C2=A0 = in Coq.",

=C2=A0 paper =3D "Sanc19.pdf"

}

@misc= {Wang19a,

=C2=A0 author =3D "Wang, Qingxiang and Brown, Chad and Ka= liszyk, Cezary and

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Urban, Jose= f",

=C2=A0 title =3D {{Exploration of Neural Machine Translation i= n

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Autoformalization of Mathema= tics in Mizar}},

=C2=A0 year =3D "2019",

=C2=A0 link =3D &q= uot;\url{https://arxiv.org= /pdf/1912.02636.pdf}",

=C2=A0 abstract =3D

=C2=A0 =C2=A0 &qu= ot;In this paper we share several experiments trying to

=C2=A0 =C2=A0 au= tomatically translate informal mathematics into formal

=C2=A0 =C2=A0 mat= hematics. In our context informal mathematics refers to

=C2=A0 =C2=A0 hu= man-written mathematical sentences in the LaTeX format; and

=C2=A0 =C2= =A0 formal mathematics refers to statements in the Mizar language. We

= =C2=A0 =C2=A0 conducted our experiments against three established neural

=C2=A0 =C2=A0 network-based machine translation models that are know to de= liver

=C2=A0 =C2=A0 competitive results on translating between natural l= anguages. To

=C2=A0 =C2=A0 train these models we also prepared four info= rmal-to-formal

=C2=A0 =C2=A0 datasets. We compare and analyze our result= s according to whether

=C2=A0 =C2=A0 the model is supervised or unsuperv= ised. In order to augment the

=C2=A0 =C2=A0 data available for auto-form= alization and improve the results, we

=C2=A0 =C2=A0 develop a custom typ= e-elaboration mechanism and integrate it into

=C2=A0 =C2=A0 the supervis= ed translation.",

=C2=A0 paper =3D "Wang19a.pdf"

}

=

Thanks for this! It seems to speak to the success of the O=
penAI Codex more than anything else, but the results are impressive.

--000000000000456b4a05d52a4e53--
From MAILER-DAEMON Sun Jan 09 16:56:58 2022
Received: from list by lists.gnu.org with archive (Exim 4.90_1)
id 1n6gBO-0000fk-Cm
for mharc-axiom-developer@gnu.org; Sun, 09 Jan 2022 16:56:58 -0500
Received: from eggs.gnu.org ([209.51.188.92]:51162)
by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256)
(Exim 4.90_1) (envelope-from )
id 1n6gBN-0000fb-Bh
for axiom-developer@nongnu.org; Sun, 09 Jan 2022 16:56:57 -0500
Received: from [2607:f8b0:4864:20::834] (port=41549
helo=mail-qt1-x834.google.com)
by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128)
(Exim 4.90_1) (envelope-from )
id 1n6gBK-0003v9-28
for axiom-developer@nongnu.org; Sun, 09 Jan 2022 16:56:57 -0500
Received: by mail-qt1-x834.google.com with SMTP id f17so10002880qtf.8
for ; Sun, 09 Jan 2022 13:56:51 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112;
h=mime-version:references:in-reply-to:from:date:message-id:subject:to
:cc; bh=7XIX8bFw3UhFMKJPHm+ztOMwTtdj2nSsPcjQ4PcmAWw=;
b=Y8HcZvsrv1uYwKVskY39mr4nILesPxFguYzmnIdDXaKzpJI1oisA1wRn7DmwPVcEyl
oziN3aJr5CVxZV+yrGjd/fym9mQ2uvoqsE32Tq6XdTNjjl/og+UdLztAYsvXpzOTmLJk
chZAblQUeVcaMpZhxC+K8ib8IbsGlkUYLDVn62LR+b8dFL1X1wXOOWDny/JHWCTdX5LF
w8UdzACEt33dWfamfZSj6hi8RjL4elGHTrrLxVPRmynqix+J+DWDuA/XxkEOnEtimsII
YETQGWZplrnhI8SnXkG/BCTxrVnBfMOvkqo7epQmqBveM0MlhNfmIIJSLvZTrgCtiExi
T9DQ==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=1e100.net; s=20210112;
h=x-gm-message-state:mime-version:references:in-reply-to:from:date
:message-id:subject:to:cc;
bh=7XIX8bFw3UhFMKJPHm+ztOMwTtdj2nSsPcjQ4PcmAWw=;
b=X3OLsGMX6P1XOlxT3t4t462dosvR1/rDuvhdcfpQoL5GSnyQ7h/qwfftGHRUgV3v+h
lja3HJglzpc6vu6pPX4GqRnLdYVnMsxwbD6vQ5lt9PjyhZD1Qq44ymt4KyUoQtHJ5rU+
T/KUtnadcaGuMDTgyB8TuxUYG2hHSzUs37bduSt7Ju9gRHYwEfZmYxJROmmexsCKk/ir
biyyXINR9jgBHnYf0IcJTGDAbwnwixLWS0bUoqvkntPmCB+99EaAWHEmfAECCgAQ3tYH
3zXTXTNCUYb3yhjfVzwK1HDT15KSf2G45i0yVQAbwuYQCPon/4mCeFajtkp3UvrLeU5o
RVyg==
X-Gm-Message-State: AOAM531Vu+2QKcqusSqj0xnr5C9IG6dCxqabE2rnbosdncF+iJ/8fPGV
3L43Hjp3zWl1Wl2ud51Gj5HDMo/cgzAToQ/E69U=
X-Google-Smtp-Source: ABdhPJypqAIeAL3bfl13RAIxDhNHT1flPO8KZbYa/ER8RoHyWBJTO+YK6E9rPAgcu6V0SzR/kd6iqZu0eW6bd9vdbls=
X-Received: by 2002:ac8:5fc4:: with SMTP id k4mr2018091qta.28.1641765410958;
Sun, 09 Jan 2022 13:56:50 -0800 (PST)
MIME-Version: 1.0
References:
In-Reply-To:
From: Tim Daly
Date: Sun, 9 Jan 2022 16:56:37 -0500
Message-ID:
Subject: Re: A NN Solves and Generates Math Problems
To: Jeremy Avigad
Cc: Frank Pfenning , Prof Robert Harper ,
mcarneir , axiom-dev
Content-Type: multipart/alternative; boundary="0000000000001fed7e05d52d4c44"
X-Host-Lookup-Failed: Reverse DNS lookup failed for 2607:f8b0:4864:20::834
(failed)
Received-SPF: pass client-ip=2607:f8b0:4864:20::834;
envelope-from=axiomcas@gmail.com; helo=mail-qt1-x834.google.com
X-Spam_score_int: -12
X-Spam_score: -1.3
X-Spam_bar: -
X-Spam_report: (-1.3 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1,
DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, FREEMAIL_FROM=0.001,
HTML_MESSAGE=0.001, RCVD_IN_DNSWL_NONE=-0.0001, RDNS_NONE=0.793,
SPF_HELO_NONE=0.001, SPF_PASS=-0.001 autolearn=no autolearn_force=no
X-Spam_action: no action
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.29
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Sun, 09 Jan 2022 21:56:57 -0000
--0000000000001fed7e05d52d4c44
Content-Type: text/plain; charset="UTF-8"
In general, I'm pretty skeptical of Neural Net generation of math,
but I'm following the literature quite closely.
I recently spent time with an effort that tried to do integration.
It was interesting because they could "round trip" the solution by
differentiating the result. I worked with the authors, added some
of their results to Axiom, and suggested possible further work. But
the approach, while it looks impressive, has quite a few flaws.
I have yet to "deep dive" into this paper. It is really interesting to
me that it claims to generate code. I would like to see a "round
trip" where some LEAN math was used to generate code and
then the code was proven using LEAN. Especially interesting
would be the question of how the definitions and axioms of the
original LEAN proof were used, if at all, in the proof of the code.
(Of course, LEAN doesn't seem to focus on proving code.)
>From an Axiom point of view, "proven code generation" from a
proven theorem is my holy grail. If there was a way to form a
one-to-one, onto mapping between theorems and code I'd be
rewriting all of Axiom using it. I doubt that a Neural Net can
achieve such a mapping.
Given that Axiom is using first-class dependent types I'm not
at all clear how that could be possible using a Neural Net.
Can a Neural Net even infer the correct Types? I suppose,
for the simple case such as NAT, it could "learn" from the
definitions but cubical types might be a tad bit harder.
Nor is it clear to me how you would generate code that was
sound but not complete.
I just looked up Bartosz's body of work. It looks really interesting,
giving me much more to read.
Tim
On Sun, Jan 9, 2022 at 1:22 PM Jeremy Avigad wrote:
> Thanks for this! It seems to speak to the success of the OpenAI Codex more
> than anything else, but the results are impressive.
>
> Bartosz Piotrowski, a PhD student and author of one of the papers you
> cited, will be visiting Carnegie Mellon for a few months this spring.
>
> Best wishes,
>
> Jeremy
>
> On Thu, Jan 6, 2022 at 10:30 AM Tim Daly wrote:
>
>> This is an interesting paper (especially given that it
>> is work under Gilbert Strang):
>>
>> A Neural Network Solves and Generates Mathematics
>> Problems by Progam Synthesis: Calculus, Differential
>> Equations, Linear Algebra, and More.
>> https://arxiv.org/pdf/2112.15594.pdf
>>
>> "This work shows that a neural network that generates
>> programs (i.e. program synthesis) is the key to solving
>> math and STEM courses at scale, as it turns question
>> answering into a programming task."
>>
>> This seems interesting from several aspects:
>>
>> 1) Can this be applied to logic systems? Can it help
>> generate "proven code" from a proof system? (LEAN)
>>
>> 2) Can it be applied in programs like NuPRL / RedPRL?
>> (Innovations in Computational Type Theory using Nuprl
>> Journal of Applied Logic 4 (2006) pp 428--469
>>
>> https://reader.elsevier.com/reader/sd/pii/S1570868305000704?token=C11F82ADA94390097338EF7E421A4D9DFEF909336A451BF51D3099EDF1025177323CCD7B46510F77FFC4955D0AC6724F&originRegion=us-east-1&originCreation=20220106150458
>>
>> 3) Can the type of an object be inferred by casting it as a
>> question in mathematics? Is the generated program correctly
>> typed?
>>
>> 4) Can this be layered on MetaMath (LEAN) or FDL (Nuprl)
>> to generate logically equivalent code?
>>
>> 5) Can this be applied to gradual typing?
>>
>> In any case, this represents an interesting "interdisciplinary"
>> effort connecting the math department and CS.
>>
>> Tim
>>
>>
>>
>> There are various connections to Neural Networks and Math:
>>
>> @misc{Crou19,
>> author = "Crouse, Maxwell and Whitehead, Spencer and
>> Abdelaziz, Ibrahim and Makni, Bassem and
>> Cornelio, Cristina and Kapanipathi, Pavan and
>> Pell, Edwin and Srinivas, Kavitha and
>> Thost, Veronika and Witbrock, Michael and
>> Fokoue, Achille",
>> title = {{A Deep Reinforcement Learning Base Approach to Learning
>> Transferable Proof Guidance Strategies}},
>> year = "2019",
>> linke = "\url{https://arxiv.org/pdf/1911.02065.pdf}",
>> abstract =
>> "Traditional first-order logic (FOL) reasoning systems usually
>> rely on manual heuristics for proof guidance. We propose TRAIL: a
>> system that learns to perform proof guidance using reinforcement
>> learning. A key design principle of our system is that it is
>> general enough to allow transfer to problems in different domains
>> that do not share the same vocabulary of the training set. To do
>> so, we developed a novel representation of the internal state of a
>> prover in terms of clauses and inference actions, and a novel
>> neural-based attention mechanism to learn interactions between
>> clauses. We demonstrate that this approach enables the system to
>> generalize from training to test data across domains with
>> different vocabularies, suggesting that the nerual architecture in
>> TRAIL is well suited for representing and processing of logical
>> formalisms.",
>> paper = "Crou19.pdf"
>> }
>>
>> @misc{Crou19a,
>> author = "Crouse, Maxwell and Abdelaziz, Ibrahim and
>> Cornelio, Cristina and Thost, Veronika and
>> Wu, Lingfei and Forbus, Kenneth and Fokoue, Achille",
>> title = {{Improving Graph Neural Network Representations of Logical
>> Formulae with Subgraph Pooling}},
>> year = "2019",
>> linke = "\url{https://arxiv.org/pdf/1911.06904.pdf}",
>> abstract =
>> "Recent advances in the integration of deep learning with
>> automated theorem proving have centered around the representation
>> of graph-structured representations, in large part driven by the
>> rapidly emerging body of research in geometric deep
>> learning. Typically, structure-aware neural methods for embedding
>> logical formulae have been variants of either Tree LSTMs or
>> GNNs. While more effective than character and token-level
>> approaches, such methods have often made representational
>> trade-offs that limited their ability to effectively represent the
>> global structure of their inputs. In this work, we introduce a
>> novel approach for embedding logical formulae using DAG LSTMs that
>> is designed to overome the limitations of both Tree LSTMs and
>> GNNs. The effectiveness of the proposed framework is demonstrated
>> on the tasks of premise selection and proof step classification
>> where it achieves the state-of-the-art performance on two standard
>> datasets.",
>> paper = "Crou19a.pdf"
>> }
>>
>> @misc{Gaut19,
>> author = "Gauthier, Thibault",
>> title = {{Deep Reinforcement Learning in HOL4}},
>> year = "2019",
>> link = "\url{https://arxiv.org/pdf/1910.11797.pdf}",
>> abstract =
>> "The paper describes an implementation of deep reinforcement
>> learning through self-supervised learning within the proof
>> assistant HOL4. A close interaction between the machine learning
>> modules and the HOL4 library is achieved by the choice of tree
>> neural networks (TNNs) as machine learning models and the internal
>> use of HOL4 terms to represent tree structures of TNNs. Recursive
>> improvement is possible when a given task is expressed as a search
>> problem. In this case, a Monte Carlo Tree Search (MCTS) algorithm
>> guided by a TNN can be used to explore the search space and
>> produce better examples for training the next TNN. As an
>> illustration, tasks over propositional and arithmetical terms,
>> representative of fundamental theorem proving techniques, are
>> specified and learned: truth estimation, end-to-end computation,
>> term rewriting and term synthesis.",
>> paper = "Gaut19.pdf"
>> }
>>
>> @misc{Lamp19,
>> author = "Lample, Guillaume and Charton, Francois",
>> title = {{Deep Learning for Symbolic Mathematics}},
>> year = "2019",
>> link = "\url{https://arxiv.org/pdf/1912.01412.pdf}",
>> link = "\url{https://www.youtube.com/watch?v=O_sHHG5_lr8}",
>> abstract =
>> "Neural networks have a reputation for being better at solving
>> statistical or approximate problems than at performing
>> calculations or working with symbolic data. In this paper, we show
>> that they can be surprisingly good at more elaborated tasks in
>> mathematics, such as symbolic integration and solving differential
>> equations. We propose a syntax for representing mathematical
>> problems, and methods for generating large datasets that can be
>> used to train sequence-to-sequence models. We achieve results that
>> outperform commercial Computer Algebra Systems such as Matlab or
>> Mathematica.",
>> paper = "Lamp19.pdf",
>> keywords = "printed, DONE"
>> }
>>
>> @misc{Olsa19,
>> author = "Olsak, Miroslav and Kaliszyk, Cezary and Urban, Josef",
>> title = {{Property Invariant Embedding for Automated Reasoning}},
>> year = "2019",
>> link = "\url{https://arxiv.org/pdf/1911.12073.pdf}",
>> abstract =
>> "Automated reasoning and theorem proving have recently become
>> major challenges for machine learning. In other domains,
>> representations that are able to abstract over unimportant
>> transformations, such as abstraction over translations and
>> rotations in vision, are becoming more common. Standard methods of
>> embedding mathematical formulas for learning theorem proving are
>> however yet unable to handle many important transformations. In
>> particular, embedding previously unseen labels, that often arise
>> in definitional encodings and in Skolemizatin, has been very weak
>> so far. Similar problems appear when tranferring knowledge between
>> known symbols.
>>
>> We propose a novel encoding of formulas that extends existing
>> graph neural network models. This encoding represents symbols only
>> by nodes in the graph, without giving the network any knowledge of
>> the original labels. We provide additional links between such
>> nodes that allow the network to recover the meaning and therefore
>> correctly embed such nodes irrespective of the given labels. We
>> test the proposed encoding in an automated theorem prover based on
>> the tableaux connection calculus, and show that it improves on the
>> best characterizations used so far. The encoding is further
>> evaluated on the premise selection task and a newly introduced
>> symbol guessing task, and shown to correctly predict 65\% of the
>> symbol names.",
>> paper = "Olsa19.pdf"
>> }
>>
>> @misc{Piot19,
>> author = "Piotrowski, Bartosz and Brown, Chad E. and
>> Kaliszyk, Cezary",
>> title = {{Can Neural Networks Learn Symbolic Rewriting?}},
>> year = "2019",
>> link = "\url{https://arxiv.org/pdf/1911.04783.pdf}",
>> abstract =
>> "This work investigates if the current neural architectures are
>> adequate for learning symbolic rewriting. Two kinds of data sets
>> are proposed for this research -- one based on automated proofs
>> and the other being a synthetic set of polynomial terms. The
>> experiments with use of the current neural machine translation
>> models are performed and its results are discussed. Ideas for
>> extending this line of research are proposed and its relevance is
>> motivated.",
>> paper = "Piot19.pdf"
>> }
>>
>> @misc{Sanc19,
>> author = "Sanchez-Stern, Alex and Alhessi, Yousef and Saul, Lawrence
>> and Lerner, Sorin",
>> title = {{Generating Correctness Proofs with Neural Networks}},
>> year = "2019",
>> link = "\url{https://arxiv.org/pdf/1907.07794.pdf}",
>> abstract =
>> "Foundational verification allows programmers to build software
>> which has been empirically shown to have high levels of assurance
>> in a variety of important domains. However, the cost of producing
>> foundationally verified software remains prohibitively high for
>> most projects, as it requires significant manual effort by highly
>> trained experts. In this paper we present Proverbot9001 a proof
>> search system using machine learning techniques to produce proofs
>> of software correctness in interactive theorem provers. We
>> deomonstrate Proverbot9001 on the proof obligations from a large
>> practical proof project, the CompCert verified C compiler, and
>> show that it can effectively automate what was previously manual
>> proofs, automatically solving 15.77\% of proofs in our test
>> dataset. This corresponds to an over 3X improvement over the prior
>> state of the art machine learning technique for generating proofs
>> in Coq.",
>> paper = "Sanc19.pdf"
>> }
>>
>> @misc{Wang19a,
>> author = "Wang, Qingxiang and Brown, Chad and Kaliszyk, Cezary and
>> Urban, Josef",
>> title = {{Exploration of Neural Machine Translation in
>> Autoformalization of Mathematics in Mizar}},
>> year = "2019",
>> link = "\url{https://arxiv.org/pdf/1912.02636.pdf}",
>> abstract =
>> "In this paper we share several experiments trying to
>> automatically translate informal mathematics into formal
>> mathematics. In our context informal mathematics refers to
>> human-written mathematical sentences in the LaTeX format; and
>> formal mathematics refers to statements in the Mizar language. We
>> conducted our experiments against three established neural
>> network-based machine translation models that are know to deliver
>> competitive results on translating between natural languages. To
>> train these models we also prepared four informal-to-formal
>> datasets. We compare and analyze our results according to whether
>> the model is supervised or unsupervised. In order to augment the
>> data available for auto-formalization and improve the results, we
>> develop a custom type-elaboration mechanism and integrate it into
>> the supervised translation.",
>> paper = "Wang19a.pdf"
>> }
>>
>>
>>
>>
>>
>>
--0000000000001fed7e05d52d4c44
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

Given that Axiom is using first-class dependent types I'm not

Bartosz Piotrowski, a PhD student and author of one of the pap=
ers you cited, will be visiting Carnegie Mellon for a few months this sprin=
g.

Best wishes,

Jeremy

On Thu, Jan 6, 2022 at 10:30 AM Tim Daly <axiomcas@gmail.com> wrote:

This is an interesting p= aper (especially given that itis work under Gilbert Strang):A Neural Network Solves and Generates Mathematic= sProblems by Progam Synthesis: Calculus, Differential= Equations, Linear Algebra, and More."This work shows that a neural network t= hat generatesprograms (i.e. program synthesis) is the key to sol= vingmath and STEM courses at scale, as it turns questionanswering into a programming task." This s= eems interesting from several aspects:1) Can this= be applied to logic systems? Can it helpgenerate "pro= ven code" from a proof system? (LEAN)2) Can = it be applied in programs like NuPRL / RedPRL?(Innovations in Co= mputational Type Theory using NuprlJournal of Applied Logic 4 (2= 006) pp 428--469There are various connections to Neural Networks and Math:@misc{Crou19,

=C2=A0 author =3D "Crouse, Ma= xwell and Whitehead, Spencer and

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 Abdelaziz, Ibrahim and Makni, Bassem and

=C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 =C2=A0 Cornelio, Cristina and Kapanipathi, Pavan and

=C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Pell, Edwin and Srinivas, Kavitha and

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Thost, Veronika and Witbrock, Mi= chael and

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Fokoue, Achille"= ;,

=C2=A0 title =3D {{A Deep Reinforcement Learning Base Approach to Lea= rning

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0Transferable Proof Guidan= ce Strategies}},

=C2=A0 year =3D "2019",

=C2=A0 linke =3D &= quot;\url{https://arxiv.org/pdf/1911.02065.pdf}",

=C2=A0 abstract =3D <= br>=C2=A0 =C2=A0 "Traditional first-order logic (FOL) reasoning system= s usually

=C2=A0 =C2=A0 rely on manual heuristics for proof guidance. We= propose TRAIL: a

=C2=A0 =C2=A0 system that learns to perform proof guid= ance using reinforcement

=C2=A0 =C2=A0 learning. A key design principle = of our system is that it is

=C2=A0 =C2=A0 general enough to allow transf= er to problems in different domains

=C2=A0 =C2=A0 that do not share the = same vocabulary of the training set. To do

=C2=A0 =C2=A0 so, we develope= d a novel representation of the internal state of a

=C2=A0 =C2=A0 prover= in terms of clauses and inference actions, and a novel

=C2=A0 =C2=A0 ne= ural-based attention mechanism to learn interactions between

=C2=A0 =C2= =A0 clauses. We demonstrate that this approach enables the system to

=C2= =A0 =C2=A0 generalize from training to test data across domains with

=C2= =A0 =C2=A0 different vocabularies, suggesting that the nerual architecture = in

=C2=A0 =C2=A0 TRAIL is well suited for representing and processing of= logical

=C2=A0 =C2=A0 formalisms.",

=C2=A0 paper =3D "Crou= 19.pdf"}@misc{Crou19a,

=C2= =A0 author =3D "Crouse, Maxwell and Abdelaziz, Ibrahim and

=C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Cornelio, Cristina and Thost, Veronika a= nd

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Wu, Lingfei and Forbus, Ken= neth and Fokoue, Achille",

=C2=A0 title =3D {{Improving Graph Neura= l Network Representations of Logical

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0 Formulae with Subgraph Pooling}},

=C2=A0 year =3D "2019"= ;,

=C2=A0 linke =3D "\url{https://arxiv.org/pdf/1911.06904.pdf}",<= br>=C2=A0 abstract =3D

=C2=A0 =C2=A0 "Recent advances in the integ= ration of deep learning with

=C2=A0 =C2=A0 automated theorem proving hav= e centered around the representation

=C2=A0 =C2=A0 of graph-structured r= epresentations, in large part driven by the

=C2=A0 =C2=A0 rapidly emergi= ng body of research in geometric deep

=C2=A0 =C2=A0 learning. Typically,= structure-aware neural methods for embedding

=C2=A0 =C2=A0 logical form= ulae have been variants of either Tree LSTMs or

=C2=A0 =C2=A0 GNNs. Whil= e more effective than character and token-level

=C2=A0 =C2=A0 approaches= , such methods have often made representational

=C2=A0 =C2=A0 trade-offs= that limited their ability to effectively represent the

=C2=A0 =C2=A0 g= lobal structure of their inputs. In this work, we introduce a

=C2=A0 =C2= =A0 novel approach for embedding logical formulae using DAG LSTMs that

= =C2=A0 =C2=A0 is designed to overome the limitations of both Tree LSTMs and=

=C2=A0 =C2=A0 GNNs. The effectiveness of the proposed framework is demo= nstrated

=C2=A0 =C2=A0 on the tasks of premise selection and proof step = classification

=C2=A0 =C2=A0 where it achieves the state-of-the-art perf= ormance on two standard

=C2=A0 =C2=A0 datasets.",

=C2=A0 paper = =3D "Crou19a.pdf"

}@misc{Gaut19,

= =C2=A0 author =3D "Gauthier, Thibault",

=C2=A0 title =3D {{Dee= p Reinforcement Learning in HOL4}},

=C2=A0 year =3D "2019",

=C2=A0 link =3D "\url{https://arxiv.org/pdf/1910.11797.pdf}",

=C2= =A0 abstract =3D

=C2=A0 =C2=A0 "The paper describes an implementati= on of deep reinforcement

=C2=A0 =C2=A0 learning through self-supervised = learning within the proof

=C2=A0 =C2=A0 assistant HOL4. A close interact= ion between the machine learning

=C2=A0 =C2=A0 modules and the HOL4 libr= ary is achieved by the choice of tree

=C2=A0 =C2=A0 neural networks (TNN= s) as machine learning models and the internal

=C2=A0 =C2=A0 use of HOL4= terms to represent tree structures of TNNs. Recursive

=C2=A0 =C2=A0 imp= rovement is possible when a given task is expressed as a search

=C2=A0 = =C2=A0 problem. In this case, a Monte Carlo Tree Search (MCTS) algorithm

=C2=A0 =C2=A0 guided by a TNN can be used to explore the search space and<= br>=C2=A0 =C2=A0 produce better examples for training the next TNN. As an=C2=A0 =C2=A0 illustration, tasks over propositional and arithmetical ter= ms,

=C2=A0 =C2=A0 representative of fundamental theorem proving techniqu= es, are

=C2=A0 =C2=A0 specified and learned: truth estimation, end-to-en= d computation,

=C2=A0 =C2=A0 term rewriting and term synthesis.",=C2=A0 paper =3D "Gaut19.pdf"

}@mi= sc{Lamp19,

=C2=A0 author =3D "Lample, Guillaume and Charton, Franco= is",

=C2=A0 title =3D {{Deep Learning for Symbolic Mathematics}},=C2=A0 year =3D "2019",

=C2=A0 link =3D "\url{https://arxiv.o= rg/pdf/1912.01412.pdf}",

=C2=A0 link =3D "\url{https://ww= w.youtube.com/watch?v=3DO_sHHG5_lr8}",

=C2=A0 abstract =3D

= =C2=A0 =C2=A0 "Neural networks have a reputation for being better at s= olving

=C2=A0 =C2=A0 statistical or approximate problems than at perform= ing

=C2=A0 =C2=A0 calculations or working with symbolic data. In this pa= per, we show

=C2=A0 =C2=A0 that they can be surprisingly good at more el= aborated tasks in

=C2=A0 =C2=A0 mathematics, such as symbolic integratio= n and solving differential

=C2=A0 =C2=A0 equations. We propose a syntax = for representing mathematical

=C2=A0 =C2=A0 problems, and methods for ge= nerating large datasets that can be

=C2=A0 =C2=A0 used to train sequence= -to-sequence models. We achieve results that

=C2=A0 =C2=A0 outperform co= mmercial Computer Algebra Systems such as Matlab or

=C2=A0 =C2=A0 Mathem= atica.",

=C2=A0 paper =3D "Lamp19.pdf",

=C2=A0 keyword= s =3D "printed, DONE"

}@misc{Olsa19,=

=C2=A0 author =3D "Olsak, Miroslav and Kaliszyk, Cezary and Urban,= Josef",

=C2=A0 title =3D {{Property Invariant Embedding for Automa= ted Reasoning}},

=C2=A0 year =3D "2019",

=C2=A0 link =3D &q= uot;\url{https://arxiv.org/pdf/1911.12073.pdf}",

=C2=A0 abstract =3D

=C2=A0 =C2=A0 "Automated reasoning and theorem proving have recently = become

=C2=A0 =C2=A0 major challenges for machine learning. In other dom= ains,

=C2=A0 =C2=A0 representations that are able to abstract over unimp= ortant

=C2=A0 =C2=A0 transformations, such as abstraction over translati= ons and

=C2=A0 =C2=A0 rotations in vision, are becoming more common. Sta= ndard methods of

=C2=A0 =C2=A0 embedding mathematical formulas for learn= ing theorem proving are

=C2=A0 =C2=A0 however yet unable to handle many = important transformations. In

=C2=A0 =C2=A0 particular, embedding previo= usly unseen labels, that often arise

=C2=A0 =C2=A0 in definitional encod= ings and in Skolemizatin, has been very weak

=C2=A0 =C2=A0 so far. Simil= ar problems appear when tranferring knowledge between

=C2=A0 =C2=A0 know= n symbols.

=C2=A0 =C2=A0 We propose a novel encoding of formulas tha= t extends existing

=C2=A0 =C2=A0 graph neural network models. This encod= ing represents symbols only

=C2=A0 =C2=A0 by nodes in the graph, without= giving the network any knowledge of

=C2=A0 =C2=A0 the original labels. = We provide additional links between such

=C2=A0 =C2=A0 nodes that allow = the network to recover the meaning and therefore

=C2=A0 =C2=A0 correctly= embed such nodes irrespective of the given labels. We

=C2=A0 =C2=A0 tes= t the proposed encoding in an automated theorem prover based on

=C2=A0 = =C2=A0 the tableaux connection calculus, and show that it improves on the=C2=A0 =C2=A0 best characterizations used so far. The encoding is further=

=C2=A0 =C2=A0 evaluated on the premise selection task and a newly intro= duced

=C2=A0 =C2=A0 symbol guessing task, and shown to correctly predict= 65\% of the

=C2=A0 =C2=A0 symbol names.",

=C2=A0 paper =3D &quo= t;Olsa19.pdf"

}@misc{Piot19,

=C2=A0 author = =3D "Piotrowski, Bartosz and Brown, Chad E. and

=C2=A0 =C2=A0 =C2= =A0 =C2=A0 =C2=A0 =C2=A0 Kaliszyk, Cezary",

=C2=A0 title =3D {{Can = Neural Networks Learn Symbolic Rewriting?}},

=C2=A0 year =3D "2019&= quot;,

=C2=A0 link =3D "\url{https://arxiv.org/pdf/1911.04783.pdf}"= ;,

=C2=A0 abstract =3D

=C2=A0 =C2=A0 "This work investigates if = the current neural architectures are

=C2=A0 =C2=A0 adequate for learning= symbolic rewriting. Two kinds of data sets

=C2=A0 =C2=A0 are proposed f= or this research -- one based on automated proofs

=C2=A0 =C2=A0 and the = other being a synthetic set of polynomial terms. The

=C2=A0 =C2=A0 exper= iments with use of the current neural machine translation

=C2=A0 =C2=A0 = models are performed and its results are discussed. Ideas for

=C2=A0 =C2= =A0 extending this line of research are proposed and its relevance is

= =C2=A0 =C2=A0 motivated.",

=C2=A0 paper =3D "Piot19.pdf"=

}

@misc{Sanc19,

=C2=A0 author =3D "Sanchez-Stern, Alex a= nd Alhessi, Yousef and Saul, Lawrence

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 and Lerner, Sorin",

=C2=A0 title =3D {{Generating Correc= tness Proofs with Neural Networks}},

=C2=A0 year =3D "2019",=C2=A0 link =3D "\url{https://arxiv.org/pdf/1907.07794.pdf}",

= =C2=A0 abstract =3D

=C2=A0 =C2=A0 "Foundational verification allows= programmers to build software

=C2=A0 =C2=A0 which has been empirically = shown to have high levels of assurance

=C2=A0 =C2=A0 in a variety of imp= ortant domains. However, the cost of producing

=C2=A0 =C2=A0 foundationa= lly verified software remains prohibitively high for

=C2=A0 =C2=A0 most = projects, as it requires significant manual effort by highly

=C2=A0 =C2= =A0 trained experts. In this paper we present Proverbot9001 a proof

=C2= =A0 =C2=A0 search system using machine learning techniques to produce proof= s

=C2=A0 =C2=A0 of software correctness in interactive theorem provers. = We

=C2=A0 =C2=A0 deomonstrate Proverbot9001 on the proof obligations fro= m a large

=C2=A0 =C2=A0 practical proof project, the CompCert verified C= compiler, and

=C2=A0 =C2=A0 show that it can effectively automate what = was previously manual

=C2=A0 =C2=A0 proofs, automatically solving 15.77\= % of proofs in our test

=C2=A0 =C2=A0 dataset. This corresponds to an ov= er 3X improvement over the prior

=C2=A0 =C2=A0 state of the art machine = learning technique for generating proofs

=C2=A0 =C2=A0 in Coq.",

=C2=A0 paper =3D "Sanc19.pdf"

}

@misc{Wang19a,

=C2= =A0 author =3D "Wang, Qingxiang and Brown, Chad and Kaliszyk, Cezary a= nd

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Urban, Josef",

=C2= =A0 title =3D {{Exploration of Neural Machine Translation in

=C2=A0 =C2= =A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Autoformalization of Mathematics in Mizar}}= ,

=C2=A0 year =3D "2019",

=C2=A0 link =3D "\url{https://arxiv.= org/pdf/1912.02636.pdf}",

=C2=A0 abstract =3D

=C2=A0 =C2=A0 = "In this paper we share several experiments trying to

=C2=A0 =C2=A0= automatically translate informal mathematics into formal

=C2=A0 =C2=A0 = mathematics. In our context informal mathematics refers to

=C2=A0 =C2=A0= human-written mathematical sentences in the LaTeX format; and

=C2=A0 = =C2=A0 formal mathematics refers to statements in the Mizar language. We

=C2=A0 =C2=A0 conducted our experiments against three established neural=C2=A0 =C2=A0 network-based machine translation models that are know to d= eliver

=C2=A0 =C2=A0 competitive results on translating between natural = languages. To

=C2=A0 =C2=A0 train these models we also prepared four inf= ormal-to-formal

=C2=A0 =C2=A0 datasets. We compare and analyze our resul= ts according to whether

=C2=A0 =C2=A0 the model is supervised or unsuper= vised. In order to augment the

=C2=A0 =C2=A0 data available for auto-for= malization and improve the results, we

=C2=A0 =C2=A0 develop a custom ty= pe-elaboration mechanism and integrate it into

=C2=A0 =C2=A0 the supervi= sed translation.",

=C2=A0 paper =3D "Wang19a.pdf"

}

In general, I'm pretty skeptical of Neural Net ge=
neration of math,

but I'm following the literature quite clos=
ely.

I recently spent time with an effort that=
tried to do integration.

It was interesting because they could &=
quot;round trip" the solution by

differentiating the result.=
I worked with the authors, added some

of their results to A=
xiom, and suggested possible further work. But

the approach,=
while it looks impressive, has quite a few flaws.

I have yet to "deep dive" into this paper. It is really interest=
ing to

me that it claims to generate code. I would like to see a =
"round

trip" where some LEAN math was used to generate =
code and

then the code was proven using LEAN. Especially interest=
ing

would be the question of how the definitions and axioms of th=
e

original LEAN proof were used, if at all, in the proof of the c=
ode.

(Of course, LEAN doesn't seem to focus on proving code.)=

From an Axiom point of view, "proven cod=
e generation" from a

proven theorem is my holy grail. If the=
re was a way to form a

one-to-one, onto mapping between theorems =
and code I'd be

rewriting all of Axiom using it. I doubt that=
a Neural Net can

achieve such a mapping.

Ca=
n a Neural Net even infer the correct Types? I suppose,

for the s=
imple case such as NAT, it could "learn" from the

defin=
itions but cubical types might be a tad bit harder.

Nor is it clear to me how you would generate code that was

=
sound but not complete.

I just looked up Bartosz&#=
39;s body of work. It looks really interesting,

giving me much mo=
re to read.

Tim

On Sun, Jan 9, 2022 at 1:22 PM Jeremy Avigad <avigad@cmu.edu> wrote:

Thanks for this! It seems to speak = to the success of the OpenAI Codex more than anything else, but the results= are impressive.Bartosz Piotrowski, a PhD student and a= uthor of one of the papers you cited, will be visiting Carnegie Mellon for = a few months this spring.Best wishes,<= br>JeremyOn Thu, Jan 6, 2022 at 10:30 AM Tim Daly <axiomcas@gmail.com&= gt; wrote:This is an interesting paper (especially given that itis work under Gilbert Strang):A Neura= l Network Solves and Generates MathematicsProblems by Progam Syn= thesis: Calculus, DifferentialEquations, Linear Algebra, and Mor= e.&quo= t;This work shows that a neural network that generatesprograms (= i.e. program synthesis) is the key to solvingmath and STEM cours= es at scale, as it turns questionanswering into a programming ta= sk."This seems interesting from several aspe= cts:1) Can this be applied to logic systems? Can = it helpgenerate "proven code" from a proof system= ? (LEAN)2) Can it be applied in programs like NuP= RL / RedPRL?(Innovations in Computational Type Theory using Nupr= lJournal of Applied Logic 4 (2006) pp 428--4693) Can = the type of an object be inferred by casting it as aquestion in = mathematics? Is the generated program correctlytyped?=4) Can this be layered on MetaMath (LEAN) or FDL (Nuprl)to generate logically equivalent code?5) C= an this be applied to gradual typing?In any c= ase, this represents an interesting "interdisciplinary"effort connecting the math department and CS.Tim=There are various c= onnections to Neural Networks and Math:@misc{Crou= 19,

=C2=A0 author =3D "Crouse, Maxwell and Whitehead, Spencer and <= br>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Abdelaziz, Ibrahim and Makni, = Bassem and

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Cornelio, Cristina= and Kapanipathi, Pavan and

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Pe= ll, Edwin and Srinivas, Kavitha and

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0 Thost, Veronika and Witbrock, Michael and

=C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 Fokoue, Achille",

=C2=A0 title =3D {{A Deep Re= inforcement Learning Base Approach to Learning

=C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 =C2=A0Transferable Proof Guidance Strategies}},

=C2=A0 year = =3D "2019",

=C2=A0 linke =3D "\url{https://arxiv.org/pdf/1911.020= 65.pdf}",

=C2=A0 abstract =3D

=C2=A0 =C2=A0 "Tradition= al first-order logic (FOL) reasoning systems usually

=C2=A0 =C2=A0 rely = on manual heuristics for proof guidance. We propose TRAIL: a

=C2=A0 =C2= =A0 system that learns to perform proof guidance using reinforcement

=C2= =A0 =C2=A0 learning. A key design principle of our system is that it is

= =C2=A0 =C2=A0 general enough to allow transfer to problems in different dom= ains

=C2=A0 =C2=A0 that do not share the same vocabulary of the training= set. To do

=C2=A0 =C2=A0 so, we developed a novel representation of the= internal state of a

=C2=A0 =C2=A0 prover in terms of clauses and infere= nce actions, and a novel

=C2=A0 =C2=A0 neural-based attention mechanism = to learn interactions between

=C2=A0 =C2=A0 clauses. We demonstrate that= this approach enables the system to

=C2=A0 =C2=A0 generalize from train= ing to test data across domains with

=C2=A0 =C2=A0 different vocabularie= s, suggesting that the nerual architecture in

=C2=A0 =C2=A0 TRAIL is wel= l suited for representing and processing of logical

=C2=A0 =C2=A0 formal= isms.",

=C2=A0 paper =3D "Crou19.pdf"}@misc{Crou19a,

=C2=A0 author =3D "Crouse, Max= well and Abdelaziz, Ibrahim and

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 Cornelio, Cristina and Thost, Veronika and

=C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 =C2=A0 Wu, Lingfei and Forbus, Kenneth and Fokoue, Achille"= ,

=C2=A0 title =3D {{Improving Graph Neural Network Representations of L= ogical

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Formulae with Subgraph = Pooling}},

=C2=A0 year =3D "2019",

=C2=A0 linke =3D "\= url{http= s://arxiv.org/pdf/1911.06904.pdf}",

=C2=A0 abstract =3D

=C2= =A0 =C2=A0 "Recent advances in the integration of deep learning with=C2=A0 =C2=A0 automated theorem proving have centered around the represen= tation

=C2=A0 =C2=A0 of graph-structured representations, in large part = driven by the

=C2=A0 =C2=A0 rapidly emerging body of research in geometr= ic deep

=C2=A0 =C2=A0 learning. Typically, structure-aware neural method= s for embedding

=C2=A0 =C2=A0 logical formulae have been variants of eit= her Tree LSTMs or

=C2=A0 =C2=A0 GNNs. While more effective than characte= r and token-level

=C2=A0 =C2=A0 approaches, such methods have often made= representational

=C2=A0 =C2=A0 trade-offs that limited their ability to= effectively represent the

=C2=A0 =C2=A0 global structure of their input= s. In this work, we introduce a

=C2=A0 =C2=A0 novel approach for embeddi= ng logical formulae using DAG LSTMs that

=C2=A0 =C2=A0 is designed to ov= erome the limitations of both Tree LSTMs and

=C2=A0 =C2=A0 GNNs. The eff= ectiveness of the proposed framework is demonstrated

=C2=A0 =C2=A0 on th= e tasks of premise selection and proof step classification

=C2=A0 =C2=A0= where it achieves the state-of-the-art performance on two standard

=C2= =A0 =C2=A0 datasets.",

=C2=A0 paper =3D "Crou19a.pdf"

}@misc{Gaut19,

=C2=A0 author =3D "Gauthi= er, Thibault",

=C2=A0 title =3D {{Deep Reinforcement Learning in HO= L4}},

=C2=A0 year =3D "2019",

=C2=A0 link =3D "\url{https://ar= xiv.org/pdf/1910.11797.pdf}",

=C2=A0 abstract =3D

=C2=A0 =C2= =A0 "The paper describes an implementation of deep reinforcement

= =C2=A0 =C2=A0 learning through self-supervised learning within the proof

=C2=A0 =C2=A0 assistant HOL4. A close interaction between the machine lear= ning

=C2=A0 =C2=A0 modules and the HOL4 library is achieved by the choic= e of tree

=C2=A0 =C2=A0 neural networks (TNNs) as machine learning model= s and the internal

=C2=A0 =C2=A0 use of HOL4 terms to represent tree str= uctures of TNNs. Recursive

=C2=A0 =C2=A0 improvement is possible when a = given task is expressed as a search

=C2=A0 =C2=A0 problem. In this case,= a Monte Carlo Tree Search (MCTS) algorithm

=C2=A0 =C2=A0 guided by a TN= N can be used to explore the search space and

=C2=A0 =C2=A0 produce bett= er examples for training the next TNN. As an

=C2=A0 =C2=A0 illustration,= tasks over propositional and arithmetical terms,

=C2=A0 =C2=A0 represen= tative of fundamental theorem proving techniques, are

=C2=A0 =C2=A0 spec= ified and learned: truth estimation, end-to-end computation,

=C2=A0 =C2= =A0 term rewriting and term synthesis.",

=C2=A0 paper =3D "Gau= t19.pdf"

}@misc{Lamp19,

=C2=A0 author = =3D "Lample, Guillaume and Charton, Francois",

=C2=A0 title = =3D {{Deep Learning for Symbolic Mathematics}},

=C2=A0 year =3D "20= 19",

=C2=A0 link =3D "\url{https://arxiv.org/pdf/1912.01412.pdf}&q= uot;,

=C2=A0 link =3D "\url{https://www.youtube.com/watch?v=3DO_sH= HG5_lr8}",

=C2=A0 abstract =3D

=C2=A0 =C2=A0 "Neural ne= tworks have a reputation for being better at solving

=C2=A0 =C2=A0 stati= stical or approximate problems than at performing

=C2=A0 =C2=A0 calculat= ions or working with symbolic data. In this paper, we show

=C2=A0 =C2=A0= that they can be surprisingly good at more elaborated tasks in

=C2=A0 = =C2=A0 mathematics, such as symbolic integration and solving differential=C2=A0 =C2=A0 equations. We propose a syntax for representing mathematica= l

=C2=A0 =C2=A0 problems, and methods for generating large datasets that= can be

=C2=A0 =C2=A0 used to train sequence-to-sequence models. We achi= eve results that

=C2=A0 =C2=A0 outperform commercial Computer Algebra Sy= stems such as Matlab or

=C2=A0 =C2=A0 Mathematica.",

=C2=A0 pape= r =3D "Lamp19.pdf",

=C2=A0 keywords =3D "printed, DONE&qu= ot;

}@misc{Olsa19,

=C2=A0 author =3D "= Olsak, Miroslav and Kaliszyk, Cezary and Urban, Josef",

=C2=A0 titl= e =3D {{Property Invariant Embedding for Automated Reasoning}},

=C2=A0 y= ear =3D "2019",

=C2=A0 link =3D "\url{https://arxiv.org/pdf/1911.= 12073.pdf}",

=C2=A0 abstract =3D

=C2=A0 =C2=A0 "Automat= ed reasoning and theorem proving have recently become

=C2=A0 =C2=A0 majo= r challenges for machine learning. In other domains,

=C2=A0 =C2=A0 repre= sentations that are able to abstract over unimportant

=C2=A0 =C2=A0 tran= sformations, such as abstraction over translations and

=C2=A0 =C2=A0 rot= ations in vision, are becoming more common. Standard methods of

=C2=A0 = =C2=A0 embedding mathematical formulas for learning theorem proving are

= =C2=A0 =C2=A0 however yet unable to handle many important transformations. = In

=C2=A0 =C2=A0 particular, embedding previously unseen labels, that of= ten arise

=C2=A0 =C2=A0 in definitional encodings and in Skolemizatin, h= as been very weak

=C2=A0 =C2=A0 so far. Similar problems appear when tra= nferring knowledge between

=C2=A0 =C2=A0 known symbols.

=C2=A0 = =C2=A0 We propose a novel encoding of formulas that extends existing

=C2= =A0 =C2=A0 graph neural network models. This encoding represents symbols on= ly

=C2=A0 =C2=A0 by nodes in the graph, without giving the network any k= nowledge of

=C2=A0 =C2=A0 the original labels. We provide additional lin= ks between such

=C2=A0 =C2=A0 nodes that allow the network to recover th= e meaning and therefore

=C2=A0 =C2=A0 correctly embed such nodes irrespe= ctive of the given labels. We

=C2=A0 =C2=A0 test the proposed encoding i= n an automated theorem prover based on

=C2=A0 =C2=A0 the tableaux connec= tion calculus, and show that it improves on the

=C2=A0 =C2=A0 best chara= cterizations used so far. The encoding is further

=C2=A0 =C2=A0 evaluate= d on the premise selection task and a newly introduced

=C2=A0 =C2=A0 sym= bol guessing task, and shown to correctly predict 65\% of the

=C2=A0 =C2= =A0 symbol names.",

=C2=A0 paper =3D "Olsa19.pdf"

}@misc{Piot19,

=C2=A0 author =3D "Piotrowski, Bartos= z and Brown, Chad E. and

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Kali= szyk, Cezary",

=C2=A0 title =3D {{Can Neural Networks Learn Symboli= c Rewriting?}},

=C2=A0 year =3D "2019",

=C2=A0 link =3D &qu= ot;\url{= https://arxiv.org/pdf/1911.04783.pdf}",

=C2=A0 abstract =3D

= =C2=A0 =C2=A0 "This work investigates if the current neural architectu= res are

=C2=A0 =C2=A0 adequate for learning symbolic rewriting. Two kind= s of data sets

=C2=A0 =C2=A0 are proposed for this research -- one based= on automated proofs

=C2=A0 =C2=A0 and the other being a synthetic set o= f polynomial terms. The

=C2=A0 =C2=A0 experiments with use of the curren= t neural machine translation

=C2=A0 =C2=A0 models are performed and its = results are discussed. Ideas for

=C2=A0 =C2=A0 extending this line of re= search are proposed and its relevance is

=C2=A0 =C2=A0 motivated.",=

=C2=A0 paper =3D "Piot19.pdf"

}

@misc{Sanc19,

= =C2=A0 author =3D "Sanchez-Stern, Alex and Alhessi, Yousef and Saul, L= awrence

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 and Lerner, Sorin&quo= t;,

=C2=A0 title =3D {{Generating Correctness Proofs with Neural Network= s}},

=C2=A0 year =3D "2019",

=C2=A0 link =3D "\url{https://arx= iv.org/pdf/1907.07794.pdf}",

=C2=A0 abstract =3D

=C2=A0 =C2= =A0 "Foundational verification allows programmers to build software

=C2=A0 =C2=A0 which has been empirically shown to have high levels of assu= rance

=C2=A0 =C2=A0 in a variety of important domains. However, the cost= of producing

=C2=A0 =C2=A0 foundationally verified software remains pro= hibitively high for

=C2=A0 =C2=A0 most projects, as it requires signific= ant manual effort by highly

=C2=A0 =C2=A0 trained experts. In this paper= we present Proverbot9001 a proof

=C2=A0 =C2=A0 search system using mach= ine learning techniques to produce proofs

=C2=A0 =C2=A0 of software corr= ectness in interactive theorem provers. We

=C2=A0 =C2=A0 deomonstrate Pr= overbot9001 on the proof obligations from a large

=C2=A0 =C2=A0 practica= l proof project, the CompCert verified C compiler, and

=C2=A0 =C2=A0 sho= w that it can effectively automate what was previously manual

=C2=A0 =C2= =A0 proofs, automatically solving 15.77\% of proofs in our test

=C2=A0 = =C2=A0 dataset. This corresponds to an over 3X improvement over the prior=C2=A0 =C2=A0 state of the art machine learning technique for generating = proofs

=C2=A0 =C2=A0 in Coq.",

=C2=A0 paper =3D "Sanc19.pdf= "

}

@misc{Wang19a,

=C2=A0 author =3D "Wang, Qingxian= g and Brown, Chad and Kaliszyk, Cezary and

=C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 Urban, Josef",

=C2=A0 title =3D {{Exploration of Neu= ral Machine Translation in

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Aut= oformalization of Mathematics in Mizar}},

=C2=A0 year =3D "2019&quo= t;,

=C2=A0 link =3D "\url{https://arxiv.org/pdf/1912.02636.pdf}",<= br>=C2=A0 abstract =3D

=C2=A0 =C2=A0 "In this paper we share severa= l experiments trying to

=C2=A0 =C2=A0 automatically translate informal m= athematics into formal

=C2=A0 =C2=A0 mathematics. In our context informa= l mathematics refers to

=C2=A0 =C2=A0 human-written mathematical sentenc= es in the LaTeX format; and

=C2=A0 =C2=A0 formal mathematics refers to s= tatements in the Mizar language. We

=C2=A0 =C2=A0 conducted our experime= nts against three established neural

=C2=A0 =C2=A0 network-based machine= translation models that are know to deliver

=C2=A0 =C2=A0 competitive r= esults on translating between natural languages. To

=C2=A0 =C2=A0 train = these models we also prepared four informal-to-formal

=C2=A0 =C2=A0 data= sets. We compare and analyze our results according to whether

=C2=A0 =C2= =A0 the model is supervised or unsupervised. In order to augment the

=C2= =A0 =C2=A0 data available for auto-formalization and improve the results, w= e

=C2=A0 =C2=A0 develop a custom type-elaboration mechanism and integrat= e it into

=C2=A0 =C2=A0 the supervised translation.",

=C2=A0 pap= er =3D "Wang19a.pdf"

}

Suppose the goal was to generate code from proofs.

<=
div>The definition of an axiom could include the text for the

Suppose that certain tactics have "code-like" equivalents=
.

Can we define such a restricted set of tactics?

This =
would eliminate Coq's hammer tactic, for example.

equ=
ivalent program, making them "effective theorems",

or &=
quot;fully constructive theorems".

Given =
a proof of a theorem from this restricted set

it should be (=
somewhat) easier to create equivalent programs.

Th=
is amounts to "proving the theorem" by "writing the program&=
quot;,

albeit in a tactic language.

For =
example, a "reduce" tactic would apply a function to a

=
set of numbers (symbolically), with the proof condition that

the =
set is finite and the generated index decreases so we

can know th=
at "reduce" terminates. That would then be

equivalent t=
o the Lisp map operation.

Tim

On Sun, Jan 9, 2022 at 4:56 PM Tim Daly <axiomcas@gmail.com> wrote:

In general, =
I'm pretty skeptical of Neural Net generation of math,

but I&=
#39;m following the literature quite closely.

=
I recently spent time with an effort that tried to do integration.

differentiating the result. I worked with the authors, added =
some

of their results to Axiom, and suggested possible furth=
er work. But

the approach, while it looks impressive, has qu=
ite a few flaws.

I have yet to "deep dive&quo=
t; into this paper. It is really interesting to

me that it claims=
to generate code. I would like to see a "round

trip" w=
here some LEAN math was used to generate code and

then the code w=
as proven using LEAN. Especially interesting

would be the questio=
n of how the definitions and axioms of the

original LEAN proof we=
re used, if at all, in the proof of the code.

(Of course, LEAN do=
esn't seem to focus on proving code.)

From=
an Axiom point of view, "proven code generation" from a

o=
ne-to-one, onto mapping between theorems and code I'd be

rewr=
iting all of Axiom using it. I doubt that a Neural Net can

achiev=
e such a mapping.

Given that Axiom is using first-=
class dependent types I'm not

at all clear how that could be =
possible using a Neural Net.

Can a Neural Net even infer the corr=
ect Types? I suppose,

for the simple case such as NAT, it could &=
quot;learn" from the

definitions but cubical types might be =
a tad bit harder.

Nor is it clear to me how yo=
u would generate code that was

sound but not complete.

=

I just looked up Bartosz's body of work. It looks really=
interesting,

giving me much more to read.

On Sun, Jan 9, 2022 at 1:22 PM Je=
remy Avigad <avigad@=
cmu.edu> wrote:

Thanks for this! It seems to speak to the success o= f the OpenAI Codex more than anything else, but the results are impressive.=Bartosz Piotrowski, a PhD student and author of one of = the papers you cited, will be visiting Carnegie Mellon for a few months thi= s spring.Best wishes,Je= remyOn Thu, Jan 6, 2022 at 10:30 AM Tim Daly <axiomcas@gmail.com> wrote:This is an interesting paper (especially given that itis work u= nder Gilbert Strang):A Neural Network Solves= and Generates MathematicsProblems by Progam Synthesis: Calculus= , DifferentialEquations, Linear Algebra, and More."This work show= s that a neural network that generatesprograms (i.e. program syn= thesis) is the key to solvingmath and STEM courses at scale, as = it turns questionanswering into a programming task."<= div>This seems interesting from several aspects:<= br>1) Can this be applied to logic systems? Can it helpgenerate "proven code" from a proof system? (LEAN) 2) Can it be applied in programs like NuPRL / RedPRL?(Innovations in Computational Type Theory using NuprlJour= nal of Applied Logic 4 (2006) pp 428--4693) Can the type of an obj= ect be inferred by casting it as aquestion in mathematics? Is th= e generated program correctlytyped?4) = Can this be layered on MetaMath (LEAN) or FDL (Nuprl)to generate= logically equivalent code?5) Can this be applied= to gradual typing?In any case, this represen= ts an interesting "interdisciplinary"effort connecting= the math department and CS.TimThere are various connections to Neur= al Networks and Math:@misc{Crou19,

=C2=A0 auth= or =3D "Crouse, Maxwell and Whitehead, Spencer and

=C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 Abdelaziz, Ibrahim and Makni, Bassem and

= =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Cornelio, Cristina and Kapanipath= i, Pavan and

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Pell, Edwin and S= rinivas, Kavitha and

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Thost, Ve= ronika and Witbrock, Michael and

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 Fokoue, Achille",

=C2=A0 title =3D {{A Deep Reinforcement Learn= ing Base Approach to Learning

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0T= ransferable Proof Guidance Strategies}},

=C2=A0 year =3D "2019"= ;,

=C2=A0 linke =3D "\url{https://arxiv.org/pdf/1911.02065.pdf}",<= br>=C2=A0 abstract =3D

=C2=A0 =C2=A0 "Traditional first-order logi= c (FOL) reasoning systems usually

=C2=A0 =C2=A0 rely on manual heuristic= s for proof guidance. We propose TRAIL: a

=C2=A0 =C2=A0 system that lear= ns to perform proof guidance using reinforcement

=C2=A0 =C2=A0 learning.= A key design principle of our system is that it is

=C2=A0 =C2=A0 genera= l enough to allow transfer to problems in different domains

=C2=A0 =C2= =A0 that do not share the same vocabulary of the training set. To do

=C2= =A0 =C2=A0 so, we developed a novel representation of the internal state of= a

=C2=A0 =C2=A0 prover in terms of clauses and inference actions, and a= novel

=C2=A0 =C2=A0 neural-based attention mechanism to learn interacti= ons between

=C2=A0 =C2=A0 clauses. We demonstrate that this approach ena= bles the system to

=C2=A0 =C2=A0 generalize from training to test data a= cross domains with

=C2=A0 =C2=A0 different vocabularies, suggesting that= the nerual architecture in

=C2=A0 =C2=A0 TRAIL is well suited for repre= senting and processing of logical

=C2=A0 =C2=A0 formalisms.",

= =C2=A0 paper =3D "Crou19.pdf"}@misc{Crou19a,

=C2=A0 author =3D "Crouse, Maxwell and Abdelaz= iz, Ibrahim and

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Cornelio, Cris= tina and Thost, Veronika and

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 W= u, Lingfei and Forbus, Kenneth and Fokoue, Achille",

=C2=A0 title = =3D {{Improving Graph Neural Network Representations of Logical

=C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Formulae with Subgraph Pooling}},

=C2= =A0 year =3D "2019",

=C2=A0 linke =3D "\url{https://arxiv.org/pdf= /1911.06904.pdf}",

=C2=A0 abstract =3D

=C2=A0 =C2=A0 "= Recent advances in the integration of deep learning with

=C2=A0 =C2=A0 a= utomated theorem proving have centered around the representation

=C2=A0 = =C2=A0 of graph-structured representations, in large part driven by the

= =C2=A0 =C2=A0 rapidly emerging body of research in geometric deep

=C2=A0= =C2=A0 learning. Typically, structure-aware neural methods for embedding=C2=A0 =C2=A0 logical formulae have been variants of either Tree LSTMs or=

=C2=A0 =C2=A0 GNNs. While more effective than character and token-level=

=C2=A0 =C2=A0 approaches, such methods have often made representational=

=C2=A0 =C2=A0 trade-offs that limited their ability to effectively repr= esent the

=C2=A0 =C2=A0 global structure of their inputs. In this work, = we introduce a

=C2=A0 =C2=A0 novel approach for embedding logical formul= ae using DAG LSTMs that

=C2=A0 =C2=A0 is designed to overome the limitat= ions of both Tree LSTMs and

=C2=A0 =C2=A0 GNNs. The effectiveness of the= proposed framework is demonstrated

=C2=A0 =C2=A0 on the tasks of premis= e selection and proof step classification

=C2=A0 =C2=A0 where it achieve= s the state-of-the-art performance on two standard

=C2=A0 =C2=A0 dataset= s.",

=C2=A0 paper =3D "Crou19a.pdf"

}

<= /div>@misc{Gaut19,

=C2=A0 author =3D "Gauthier, Thibault"= ,

=C2=A0 title =3D {{Deep Reinforcement Learning in HOL4}},

=C2=A0 ye= ar =3D "2019",

=C2=A0 link =3D "\url{https://arxiv.org/pdf/1910.1= 1797.pdf}",

=C2=A0 abstract =3D

=C2=A0 =C2=A0 "The pape= r describes an implementation of deep reinforcement

=C2=A0 =C2=A0 learni= ng through self-supervised learning within the proof

=C2=A0 =C2=A0 assis= tant HOL4. A close interaction between the machine learning

=C2=A0 =C2= =A0 modules and the HOL4 library is achieved by the choice of tree

=C2= =A0 =C2=A0 neural networks (TNNs) as machine learning models and the intern= al

=C2=A0 =C2=A0 use of HOL4 terms to represent tree structures of TNNs.= Recursive

=C2=A0 =C2=A0 improvement is possible when a given task is ex= pressed as a search

=C2=A0 =C2=A0 problem. In this case, a Monte Carlo T= ree Search (MCTS) algorithm

=C2=A0 =C2=A0 guided by a TNN can be used to= explore the search space and

=C2=A0 =C2=A0 produce better examples for = training the next TNN. As an

=C2=A0 =C2=A0 illustration, tasks over prop= ositional and arithmetical terms,

=C2=A0 =C2=A0 representative of fundam= ental theorem proving techniques, are

=C2=A0 =C2=A0 specified and learne= d: truth estimation, end-to-end computation,

=C2=A0 =C2=A0 term rewritin= g and term synthesis.",

=C2=A0 paper =3D "Gaut19.pdf"

= }@misc{Lamp19,

=C2=A0 author =3D "Lample,= Guillaume and Charton, Francois",

=C2=A0 title =3D {{Deep Learning= for Symbolic Mathematics}},

=C2=A0 year =3D "2019",

=C2=A0= link =3D "\url{https://arxiv.org/pdf/1912.01412.pdf}",

=C2=A0 lin= k =3D "\url{https://www.youtube.com/watch?v=3DO_sHHG5_lr8}",=

=C2=A0 abstract =3D

=C2=A0 =C2=A0 "Neural networks have a reput= ation for being better at solving

=C2=A0 =C2=A0 statistical or approxima= te problems than at performing

=C2=A0 =C2=A0 calculations or working wit= h symbolic data. In this paper, we show

=C2=A0 =C2=A0 that they can be s= urprisingly good at more elaborated tasks in

=C2=A0 =C2=A0 mathematics, = such as symbolic integration and solving differential

=C2=A0 =C2=A0 equa= tions. We propose a syntax for representing mathematical

=C2=A0 =C2=A0 p= roblems, and methods for generating large datasets that can be

=C2=A0 = =C2=A0 used to train sequence-to-sequence models. We achieve results that=C2=A0 =C2=A0 outperform commercial Computer Algebra Systems such as Matl= ab or

=C2=A0 =C2=A0 Mathematica.",

=C2=A0 paper =3D "Lamp19= .pdf",

=C2=A0 keywords =3D "printed, DONE"

}@misc{Olsa19,

=C2=A0 author =3D "Olsak, Miroslav an= d Kaliszyk, Cezary and Urban, Josef",

=C2=A0 title =3D {{Property I= nvariant Embedding for Automated Reasoning}},

=C2=A0 year =3D "2019= ",

=C2=A0 link =3D "\url{https://arxiv.org/pdf/1911.12073.pdf}&quo= t;,

=C2=A0 abstract =3D

=C2=A0 =C2=A0 "Automated reasoning and t= heorem proving have recently become

=C2=A0 =C2=A0 major challenges for m= achine learning. In other domains,

=C2=A0 =C2=A0 representations that ar= e able to abstract over unimportant

=C2=A0 =C2=A0 transformations, such = as abstraction over translations and

=C2=A0 =C2=A0 rotations in vision, = are becoming more common. Standard methods of

=C2=A0 =C2=A0 embedding ma= thematical formulas for learning theorem proving are

=C2=A0 =C2=A0 howev= er yet unable to handle many important transformations. In

=C2=A0 =C2=A0= particular, embedding previously unseen labels, that often arise

=C2=A0= =C2=A0 in definitional encodings and in Skolemizatin, has been very weak=C2=A0 =C2=A0 so far. Similar problems appear when tranferring knowledge = between

=C2=A0 =C2=A0 known symbols.

=C2=A0 =C2=A0 We propose a n= ovel encoding of formulas that extends existing

=C2=A0 =C2=A0 graph neur= al network models. This encoding represents symbols only

=C2=A0 =C2=A0 b= y nodes in the graph, without giving the network any knowledge of

=C2=A0= =C2=A0 the original labels. We provide additional links between such

= =C2=A0 =C2=A0 nodes that allow the network to recover the meaning and there= fore

=C2=A0 =C2=A0 correctly embed such nodes irrespective of the given = labels. We

=C2=A0 =C2=A0 test the proposed encoding in an automated theo= rem prover based on

=C2=A0 =C2=A0 the tableaux connection calculus, and = show that it improves on the

=C2=A0 =C2=A0 best characterizations used s= o far. The encoding is further

=C2=A0 =C2=A0 evaluated on the premise se= lection task and a newly introduced

=C2=A0 =C2=A0 symbol guessing task, = and shown to correctly predict 65\% of the

=C2=A0 =C2=A0 symbol names.&q= uot;,

=C2=A0 paper =3D "Olsa19.pdf"

}@mi= sc{Piot19,

=C2=A0 author =3D "Piotrowski, Bartosz and Brown, Chad E= . and

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Kaliszyk, Cezary",=

=C2=A0 title =3D {{Can Neural Networks Learn Symbolic Rewriting?}},

= =C2=A0 year =3D "2019",

=C2=A0 link =3D "\url{https://arxiv.org/p= df/1911.04783.pdf}",

=C2=A0 abstract =3D

=C2=A0 =C2=A0 "= ;This work investigates if the current neural architectures are

=C2=A0 = =C2=A0 adequate for learning symbolic rewriting. Two kinds of data sets

= =C2=A0 =C2=A0 are proposed for this research -- one based on automated proo= fs

=C2=A0 =C2=A0 and the other being a synthetic set of polynomial terms= . The

=C2=A0 =C2=A0 experiments with use of the current neural machine t= ranslation

=C2=A0 =C2=A0 models are performed and its results are discus= sed. Ideas for

=C2=A0 =C2=A0 extending this line of research are propose= d and its relevance is

=C2=A0 =C2=A0 motivated.",

=C2=A0 paper = =3D "Piot19.pdf"

}

@misc{Sanc19,

=C2=A0 author =3D &= quot;Sanchez-Stern, Alex and Alhessi, Yousef and Saul, Lawrence

=C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 and Lerner, Sorin",

=C2=A0 title= =3D {{Generating Correctness Proofs with Neural Networks}},

=C2=A0 year= =3D "2019",

=C2=A0 link =3D "\url{https://arxiv.org/pdf/1907.077= 94.pdf}",

=C2=A0 abstract =3D

=C2=A0 =C2=A0 "Foundation= al verification allows programmers to build software

=C2=A0 =C2=A0 which= has been empirically shown to have high levels of assurance

=C2=A0 =C2= =A0 in a variety of important domains. However, the cost of producing

= =C2=A0 =C2=A0 foundationally verified software remains prohibitively high f= or

=C2=A0 =C2=A0 most projects, as it requires significant manual effort= by highly

=C2=A0 =C2=A0 trained experts. In this paper we present Prove= rbot9001 a proof

=C2=A0 =C2=A0 search system using machine learning tech= niques to produce proofs

=C2=A0 =C2=A0 of software correctness in intera= ctive theorem provers. We

=C2=A0 =C2=A0 deomonstrate Proverbot9001 on th= e proof obligations from a large

=C2=A0 =C2=A0 practical proof project, = the CompCert verified C compiler, and

=C2=A0 =C2=A0 show that it can eff= ectively automate what was previously manual

=C2=A0 =C2=A0 proofs, autom= atically solving 15.77\% of proofs in our test

=C2=A0 =C2=A0 dataset. Th= is corresponds to an over 3X improvement over the prior

=C2=A0 =C2=A0 st= ate of the art machine learning technique for generating proofs

=C2=A0 = =C2=A0 in Coq.",

=C2=A0 paper =3D "Sanc19.pdf"

}@misc{Wang19a,

=C2=A0 author =3D "Wang, Qingxiang and Brown, Chad= and Kaliszyk, Cezary and

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Urba= n, Josef",

=C2=A0 title =3D {{Exploration of Neural Machine Transl= ation in

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Autoformalization of = Mathematics in Mizar}},

=C2=A0 year =3D "2019",

=C2=A0 link= =3D "\url{https://arxiv.org/pdf/1912.02636.pdf}",

=C2=A0 abstract= =3D

=C2=A0 =C2=A0 "In this paper we share several experiments tryi= ng to

=C2=A0 =C2=A0 automatically translate informal mathematics into fo= rmal

=C2=A0 =C2=A0 mathematics. In our context informal mathematics refe= rs to

=C2=A0 =C2=A0 human-written mathematical sentences in the LaTeX fo= rmat; and

=C2=A0 =C2=A0 formal mathematics refers to statements in the M= izar language. We

=C2=A0 =C2=A0 conducted our experiments against three = established neural

=C2=A0 =C2=A0 network-based machine translation model= s that are know to deliver

=C2=A0 =C2=A0 competitive results on translat= ing between natural languages. To

=C2=A0 =C2=A0 train these models we al= so prepared four informal-to-formal

=C2=A0 =C2=A0 datasets. We compare a= nd analyze our results according to whether

=C2=A0 =C2=A0 the model is s= upervised or unsupervised. In order to augment the

=C2=A0 =C2=A0 data av= ailable for auto-formalization and improve the results, we

=C2=A0 =C2=A0= develop a custom type-elaboration mechanism and integrate it into

=C2= =A0 =C2=A0 the supervised translation.",

=C2=A0 paper =3D "Wan= g19a.pdf"

}

I can't stress enough how important it is to list=
en to Hamming's talk

Axiom will begin to die the day I stop working on it.

However, proving Axiom correct "down to the meta=
l", is fundamental.

It will merge computer algebra and logic=
, spawning years of new

research.

Work o=
n fundamental problems.

Tim

On=
Thu, Dec 30, 2021 at 6:46 PM Tim Daly <axiomcas@gmail.com> wrote:

One of the interesting questi= ons when obtaining a resultis "what functions were called a= nd what was their return value?"Otherwise known as the &quo= t;show your work" idea.There is an idea call= ed the "writer monad" [0], usuallyimplemented to = facilitate logging. We can exploit thisidea to provide "sho= w your work" capability. Each functioncan provide this info= rmation inside the monad enabling thequestion to be answered at = any time.For those unfamiliar with the monad idea= , the best explanationI've found is this video [1]. Tim[0] Deriving the writer m= onad from first principles

=[1] The Absolute Best Intro to Monads for Software Engineers On Mon, Dec = 13, 2021 at 12:30 AM Tim Daly <axiomcas@gmail.com> wrote:...(snip)...Common Lisp has an "open compiler". That al= lows the abilityto deeply modify compiler behavior using compile= r macrosand macros in general. CLOS takes advantage of this to a= ddtyped behavior into the compiler in a way that ALLOWS stricttyping such as found in constructive type theory and ML.Judgments, ala Crary, are front-and-center.W= hether you USE the discipline afforded is the real question.

=Indeed, the Axiom research struggle is essentially one of howto have a disciplined use of first-class dependent types. The=struggle raises issues of, for example, compiling a dependenttype whose argument is recursive in the compiled type. Since th= e new type is first-class it can be constructed at what youimpro= perly call "run-time". However, it appears that the recursivetype may have to call the compiler at each recursion to generatethe next step since in some cases it cannot generate "closed co= de".I am embedding proofs (in LEAN langu= age) into the typehierarchy so that theorems, which depend on th= e type hierarchy,are correctly inherited. The compiler has t= o check the proofs of functionsat compile time using these. Hack= ing up nonsense just won't cut it. Thinkof the problem of em= bedding LEAN proofs in ML or ML in LEAN.(Actually, Jeremy Avigad= might find that research interesting.)So Matrix(= 3,3,Float) has inverses (assuming Float is afield (cough)). The = type inherits this theorem and proofs offunctions can use this. = But Matrix(3,4,Integer) does not haveinverses so the proofs cann= ot use this. The type hierarchy hasto ensure that the proper the= orems get inherited.Making proof technology w= ork at compile time is hard.(Worse yet, LEAN is a moving target.= Sigh.)On Thu, Nov 25, 2021 at 9:43 AM Tim Dal= y <axiomcas@gmai= l.com> wrote: As you know I've been re-architecting Axiom to use first classdependent types and proving the algorithms correct. For example, the GCD of natural numbers or the GCD of polynomials. The idea involves "boxing up" the proof with the algorithm= (akaproof carrying code) in the ELF file (under a crypto hash s= o itcan't be changed).Once the cod= e is running on the CPU, the proof is run in parallelon the fiel= d programmable gate array (FPGA). Intel data centerservers have = CPUs with built-in FPGAs these days.There is a bi= t of a disconnect, though. The GCD code is compiledmachine code = but the proof is LEAN-level.What would be ideal i= s if the compiler not only compiled the GCDcode to machine code,= it also compiled the proof to "machine code".That is,= for each machine instruction, the FPGA proof checkerwould ensur= e that the proof was not violated at the individualinstruction l= evel.What does it mean to "compile a pro= of to the machine code level"?The Milawa eff= ort (Myre14.pdf) does incremental proofs in layers.To quote from= the article [0]:=C2=A0=C2=A0 We begin with a= simple proof checker, call it A, which is short=C2=A0=C2=A0 eno= ugh to verify by the ``social process'' of mathematics -- and==C2=A0 more recently with a theorem prover for a more expressive logic= .=C2=A0=C2=A0 We then develop a series of increas= ingly powerful proof checkers,=C2=A0 call the B, C, D, and so on= . We show each of these programs only=C2=A0=C2=A0 accepts the sa= me formulas as A, using A to verify B, and B to verify=C2=A0=C2= =A0 C, and so on. Then, since we trust A, and A says B is trustworthy, we=C2=A0=C2=A0 can trust B. Then, since we trust B, and B says C is = trustworthy, we=C2=A0=C2=A0 can trust C.This gives a technique for "compiling the proof" down the = the machinecode level. Ideally, the compiler would have judgment= s for each step ofthe compilation so that each compile step has = a justification. I don'tknow of any compiler that does this = yet. (References welcome).At the machine= code level, there are techniques that would allowthe FPGA proof= to "step in sequence" with the executing code.Som= e work has been done on using "Hoare Logic for RealisticallyModelled Machine Code" (paper attached, Myre07a.pdf),"= ;Decompilation into Logic -- Improved (Myre12a.pdf).So the game is to construct a GCD over some type (Nats, Polys, etc. Axiom has 22), compile the dependent type GCD to machine code.<= div>In parallel, the proof of the code is compiled to machine code. Thepair is sent to the CPU/FPGA and, while the algorithm runs, the FPGA=ensures the proof is not violated, instruction by instruction.(I'm ignoring machine architecture issues such = pipelining, out-of-order,branch prediction, and other machine-le= vel things to ponder. I'm lookingat the RISC-V Verilog detai= ls by various people to understand better butit is still a "= ;misty fog" for me.)The result is proven= code "down to the metal".TimOn = Thu, Nov 25, 2021 at 6:05 AM Tim Daly <axiomcas@gmail.com> wrote: As you know I've been re-architecting Axiom to use first class=dependent types and proving the algorithms correct. For example,=the GCD of natural numbers or the GCD of polynomials.=The idea involves "boxing up" the proof with the a= lgorithm (akaproof carrying code) in the ELF file (under a crypt= o hash so itcan't be changed).Once= the code is running on the CPU, the proof is run in parallelon = the field programmable gate array (FPGA). Intel data centerserve= rs have CPUs with built-in FPGAs these days.There= is a bit of a disconnect, though. The GCD code is compiledmachi= ne code but the proof is LEAN-level.What would be= ideal is if the compiler not only compiled the GCDcode to machi= ne code, it also compiled the proof to "machine code".= That is, for each machine instruction, the FPGA proof checkerwou= ld ensure that the proof was not violated at the individualinstr= uction level.What does it mean to "compi= le a proof to the machine code level"?The Mi= lawa effort (Myre14.pdf) does incremental proofs in layers.To qu= ote from the article [0]:=C2=A0=C2=A0 We begi= n with a simple proof checker, call it A, which is short=C2=A0= =C2=A0 enough to verify by the ``social process'' of mathematics --= and=C2=A0 more recently with a theorem prover for a more expres= sive logic.=C2=A0=C2=A0 We then develop a series = of increasingly powerful proof checkers,=C2=A0 call the B, C, D,= and so on. We show each of these programs only=C2=A0=C2=A0 acce= pts the same formulas as A, using A to verify B, and B to verify= =C2=A0=C2=A0 C, and so on. Then, since we trust A, and A says B is trustwor= thy, we=C2=A0=C2=A0 can trust B. Then, since we trust B, and B s= ays C is trustworthy, we=C2=A0=C2=A0 can trust C.This gives a technique for "compiling the proof" = down the the machinecode level. Ideally, the compiler would have= judgments for each step ofthe compilation so that each compile = step has a justification. I don'tknow of any compiler that d= oes this yet. (References welcome).At th= e machine code level, there are techniques that would allowthe F= PGA proof to "step in sequence" with the executing code.=Some work has been done on using "Hoare Logic for Realistically<= /div>Modelled Machine Code" (paper attached, Myre07a.pdf),<= div>"Decompilation into Logic -- Improved (Myre12a.pdf).So the game is to construct a GCD over some type (Nats, Polys, = etc.Axiom has 22), compile the dependent type GCD to machine cod= e.In parallel, the proof of the code is compiled to machine code= . Thepair is sent to the CPU/FPGA and, while the algorithm runs,= the FPGAensures the proof is not violated, instruction by instr= uction.(I'm ignoring machine architecture iss= ues such pipelining, out-of-order,branch prediction, and other m= achine-level things to ponder. I'm lookingat the RISC-V Veri= log details by various people to understand better butit is stil= l a "misty fog" for me.)The result = is proven code "down to the metal".= On Sat, Nov 13, 2021 at 5:28 PM Tim Daly <axiomcas@gmail.com> wrote: Full supp= ort for general, first-class dependent types requiressome change= s to the Axiom design. That implies some languagedesign question= s.Given that mathematics is such a general subjec= t with a lot of"local" notation and ideas (witness log= ical judgment notation)careful thought is needed to design a lan= guage that is able tohandle a wide range.Normally language design is a two-level process. The language = designer creates a language and then an implementation. Variousd= esign choices affect the final language.There= is "The Metaobject Protocol" (MOP)which encourages a three-level process. Th= e language designerworks at a Metalevel to design a family = of languages, then thelanguage specializations, then the impleme= ntation. A MOP designallows the language user to optimize the la= nguage to their problem.A simple paper on the sub= ject is "Metaobject Protocols"Tim<= /div>O= n Mon, Oct 25, 2021 at 7:42 PM Tim Daly <axiomcas@gmail.com> wrote: I have a s= eparate thread of research on Self-Replicating Systems(ref: Kine= matics of Self Reproducing Machineswhich led to watching "S= trange Dreams of Stranger Loops" by Will ByrdWill referenc= ed a PhD Thesis by Jon Doyle"A Model for Deliberation, Acti= on, and Introspection"I also read the thesis= by J.C.G. Sturdy"A Lisp through the Looking Glass"Self-replication requires the ability to manipulate = your ownrepresentation in such a way that changes to that repres= entationwill change behavior.This lead= s to two thoughts in the SANE research.First, &qu= ot;Declarative Representation". That is, most of the things= about the representation should be declarative rather thanproced= ural. Applying this idea as much as possible makes iteasier to u= nderstand and manipulate.Second, "Explic= it Call Stack". Function calls form an implicitcall stack. = This can usually be displayed in a running lisp system.However, = having the call stack explicitly available would meanthat a syst= em could "introspect" at the first-class level.These two ideas would make it easy, for example, to let thesystem "show the work". One of the normal complaints is that a system presents an answer but there is no way to know how<= div>that answer was derived. These two ideas make it possible to= understand, display, and even post-answer manipulatethe intermed= iate steps.Having the intermediate steps also all= ows proofs to beinserted in a step-by-step fashion. This aids th= e effort tohave proofs run in parallel with computation at the h= ardwarelevel.Tim

<= div class=3D"gmail_quote">On Thu, Oct= 21, 2021 at 9:50 AM Tim Daly <axiomcas@gmail.com> wrote:So the current strug= gle involves the categories in Axiom.The categori= es and domains constructed using categoriesare dependent types. = When are dependent types "equal"?Well, hummmm, that de= pends on the arguments to theconstructor.But in order to decide(?) equality we have to evaluate the arg= uments (which themselves can be dependent types).Indeed, we may,= and in general, we must evaluate thearguments at compile t= ime (well, "construction time" asthere isn't reall= y a compiler / interpreter separation anymore.)That raises the question of what "equality" means. This is not simply a "set equality" relation. It falls into the infinite-groupoid of homotopy type theory. In generalit a= ppears that deciding category / domain equivalencemight force us= to climb the type hierarchy.Beyond that, there i= s the question of "which proof"applies to the resultin= g object. Proofs depend on theirassumptions which might be diffe= rent for differentconstructions. As yet I have no clue how to &q= uot;index"proofs based on their assumptions, nor how toconnect these assumptions to the groupoid structure.=My brain hurts.Tim

<= /div>On Mon, Oct 18, 2021 at 2:00 AM Tim Daly <axiomcas@gmail.com> wrote:<= blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-l= eft:1px solid rgb(204,204,204);padding-left:1ex">&quo= t;Birthing Computational Mathematics"The Axi= om SANE project is difficult at a very fundamentallevel. The tit= le "SANE" was chosen due to the variouswords found in = a thesuarus... "rational", "coherent","= judicious" and "sound".These are v= ery high level, amorphous ideas. But so isthe design of SANE. Br= eaking away from tradition incomputer algebra, type theory, and = proof assistantsis very difficult. Ideas tend to fall into stand= ard jargonwhich limits both the frame of thinking (e.g. dependen= ttypes) and the content (e.g. notation).Questioning both frame and content is very difficult. It is har= d to even recognize when they are accepted"by default"= rather than "by choice". What does the idea"= power tools" mean in a primitive, hand labor culture?Christopher Alexander [0] addresses this problem in= a lot of his writing. Specifically, in his book "Notes onth= e Synthesis of Form", in his chapter 5 "The SelfconsiousProcess", he addresses this problem directly. This is a &q= uot;must read" book.Unlike building desi= gn and contruction, however, thereare almost no constraints to u= se as guides. Alexanderquotes Plato's Phaedrus:=C2=A0 "First, the taking in of scattered particulars und= er=C2=A0=C2=A0 one Idea, so that everyone understands what is be= ing=C2=A0=C2=A0 talked about ... Second, the separation of the I= dea=C2=A0=C2=A0 into parts, by dividing it at the joints, as nat= ure=C2=A0=C2=A0 directs, not breaking any limb in half as a bad ==C2=A0=C2=A0 carver might."Lisp, which has been called "clay for the mind" can b= uild virtually anything that can be thought. The"joint= s" are also "of one's choosing" so one isboth= carver and "nature".Clearly the pr= oblem is no longer "the tools".*I* am the problem cons= training the solution.Birthing this "new thing" is slo= w, difficult, anduncertain at best.Tim=[0] Alexander, Christopher "Notes on the Syn= thesisof Form" Harvard University Press 1964ISBN 0-674-62751-2On Sun, Oct 10, 2021 at 4:40 PM Tim= Daly <axiomcas@= gmail.com> wrote:Re: writing a paper... I'm not connected to Academia

so anything I'd write would never make it into print.

"Language level parsing" is still a long way off. The talk

by Guy Steele [2] highlights some of the problems we

currently face using mathematical metanotation.

For example, a professor I know at CCNY (City College

of New York) didn't understand Platzer's "funny

fraction notation" (proof judgements) despite being

an expert in Platzer's differential equations area.

Notation matters and is not widely common.

I spoke to Professor Black (in LTI) about using natural

language in the limited task of a human-robot cooperation

in changing a car tire.=C2=A0 I looked at the current machine

learning efforts. They are no where near anything but

toy systems, taking too long to train and are too fragile.

Instead I ended up using a combination of AIML [3]

(Artificial Intelligence Markup Language), the ALICE

Chatbot [4], Forgy's OPS5 rule based program [5],

and Fahlman's SCONE [6] knowledge base. It was

much less fragile in my limited domain problem.

I have no idea how to extend any system to deal with

even undergraduate mathematics parsing.

Nor do I have any idea how I would embed LEAN

knowledge into a SCONE database, although I

think the combination would be useful and interesting.

I do believe that, in the limited area of computational

mathematics, we are capable of building robust, proven

systems that are quite general and extensible. As you

might have guessed I've given it a lot of thought over

the years :-)

A mathematical language seems to need >6 components

1) We need some sort of a specification language, possibly

somewhat 'propositional' that introduces the assumptions

you mentioned (ref. your discussion of numbers being

abstract and ref. your discussion of relevant choice of

assumptions related to a problem).

This is starting to show up in the hardware area (e.g.

Lamport's TLC[0])

Of course, specifications relate to proving programs

and, as you recall, I got a cold reception from the

LEAN community about using LEAN for program proofs.

2) We need "scaffolding". That is, we need a theory

that can be reduced to some implementable form

that provides concept-level structure.

Axiom uses group theory for this. Axiom's "category"

structure has "Category" things like Ring. Claiming

to be a Ring brings in a lot of "Signatures" of functions

you have to implement to properly be a Ring.

Scaffolding provides a firm mathematical basis for

design. It provides a link between the concept of a

Ring and the expectations you can assume when

you claim your "Domain" "is a Ring". Category

theory might provide similar structural scaffolding

(eventually... I'm still working on that thought garden)

LEAN ought to have a textbook(s?) that structures

the world around some form of mathematics. It isn't

sufficient to say "undergraduate math" is the goal.

There needs to be some coherent organization so

people can bring ideas like Group Theory to the

organization. Which brings me to ...

3) We need "spreading". That is, we need to take

the various definitions and theorems in LEAN and

place them in their proper place in the scaffold.

For example, the Ring category needs the definitions

and theorems for a Ring included in the code for the

Ring category. Similarly, the Commutative category

needs the definitions and theorems that underlie

"commutative" included in the code.

That way, when you claim to be a "Commutative Ring"

you get both sets of definitions and theorems. That is,

the inheritance mechanism will collect up all of the

definitions and theorems and make them available

for proofs.

I am looking at LEAN's definitions and theorems with

an eye to "spreading" them into the group scaffold of

Axiom.

4) We need "carriers" (Axiom calls them representations,

aka "REP"). REPs allow data structures to be defined

independent of the implementation.

For example, Axiom can construct Polynomials that

have their coefficients in various forms of representation.

You can define "dense" (all coefficients in a list),

"sparse" (only non-zero coefficients), "recursive", etc= .

A "dense polynomial" and a "sparse polynomial" work

exactly the same way as far as the user is concerned.

They both implement the same set of functions. There

is only a difference of representation for efficiency and

this only affects the implementation of the functions,

not their use.

Axiom "got this wrong" because it didn't sufficiently

separate the REP from the "Domain". I plan to fix this.

LEAN ought to have a "data structures" subtree that

has all of the definitions and axioms for all of the

existing data structures (e.g. Red-Black trees). This

would be a good undergraduate project.

5) We need "Domains" (in Axiom speak). That is, we

need a box that holds all of the functions that implement

a "Domain". For example, a "Polynomial Domain" would

hold all of the functions for manipulating polynomials

(e.g polynomial multiplication). The "Domain" box

is a dependent type that:

=C2=A0 A) has an argument list of "Categories" that this "Do= main"

=C2=A0 =C2=A0 =C2=A0 box inherits. Thus, the "Integer Domain" inh= erits

=C2=A0 =C2=A0 =C2=A0 the definitions and axioms from "Commutative"= ;

=C2=A0 =C2=A0 =C2=A0Functions in the "Domain" box can now assume<= br> =C2=A0 =C2=A0 =C2=A0and use the properties of being commutative. Proofs

=C2=A0 =C2=A0 =C2=A0of functions in this domain can use the definitions

=C2=A0 =C2=A0 =C2=A0and proofs about being commutative.

=C2=A0 B) contains an argument that specifies the "REP"

=C2=A0 =C2=A0 =C2=A0 =C2=A0(aka, the carrier). That way you get all of the<= br> =C2=A0 =C2=A0 =C2=A0 =C2=A0functions associated with the data structure

=C2=A0 =C2=A0 =C2=A0 available for use in the implementation.

=C2=A0 =C2=A0 =C2=A0 Functions in the Domain box can use all of

=C2=A0 =C2=A0 =C2=A0 the definitions and axioms about the representation

=C2=A0 =C2=A0 =C2=A0 (e.g. NonNegativeIntegers are always positive)

=C2=A0 C) contains local "spread" definitions and axioms

=C2=A0 =C2=A0 =C2=A0 =C2=A0that can be used in function proofs.

=C2=A0 =C2=A0 =C2=A0 For example, a "Square Matrix" domain would<= br> =C2=A0 =C2=A0 =C2=A0 have local axioms that state that the matrix is

=C2=A0 =C2=A0 =C2=A0 always square. Thus, functions in that box could

=C2=A0 =C2=A0 =C2=A0 use these additional definitions and axioms in

=C2=A0 =C2=A0 =C2=A0 function proofs.

=C2=A0 D) contains local state. A "Square Matrix" domain

=C2=A0 =C2=A0 =C2=A0 =C2=A0would be constructed as a dependent type that

=C2=A0 =C2=A0 =C2=A0 =C2=A0specified the size of the square (e.g. a 2x2

=C2=A0 =C2=A0 =C2=A0 =C2=A0matrix would have '2' as a dependent par= ameter.

=C2=A0 E) contains implementations of inherited functions.

=C2=A0 =C2=A0 =C2=A0 =C2=A0A "Category" could have a signature fo= r a GCD

=C2=A0 =C2=A0 =C2=A0 =C2=A0function and the "Category" could have= a default

=C2=A0 =C2=A0 =C2=A0 =C2=A0implementation. However, the "Domain" = could

=C2=A0 =C2=A0 =C2=A0 =C2=A0have a locally more efficient implementation whi= ch

=C2=A0 =C2=A0 =C2=A0 =C2=A0overrides the inherited implementation.

=C2=A0 =C2=A0 =C2=A0 Axiom has about 20 GCD implementations that

=C2=A0 =C2=A0 =C2=A0 differ locally from the default in the category. They<= br> =C2=A0 =C2=A0 =C2=A0 use properties known locally to be more efficient.

=C2=A0 F) contains local function signatures.

=C2=A0 =C2=A0 =C2=A0 A "Domain" gives the user more and more uniq= ue

=C2=A0 =C2=A0 =C2=A0 functions. The signature have associated

=C2=A0 =C2=A0 =C2=A0 "pre- and post- conditions" that can be used=

=C2=A0 =C2=A0 =C2=A0 as assumptions in the function proofs.

=C2=A0 =C2=A0 =C2=A0 Some of the user-available functions are only

=C2=A0 =C2=A0 =C2=A0 visible if the dependent type would allow them

=C2=A0 =C2=A0 =C2=A0 to exist. For example, a general Matrix domain

=C2=A0 =C2=A0 =C2=A0 would have fewer user functions that a Square

=C2=A0 =C2=A0 =C2=A0 Matrix domain.

=C2=A0 =C2=A0 =C2=A0 In addition, local "helper" functions need t= heir

=C2=A0 =C2=A0 =C2=A0 own signatures that are not user visible.

=C2=A0 G) the function implementation for each signature.

=C2=A0 =C2=A0 =C2=A0 =C2=A0This is obviously where all the magic happens

=C2=A0 H) the proof of each function.

=C2=A0 =C2=A0 =C2=A0 =C2=A0This is where I'm using LEAN.

=C2=A0 =C2=A0 =C2=A0 =C2=A0Every function has a proof. That proof can use=C2=A0 =C2=A0 =C2=A0 =C2=A0all of the definitions and axioms inherited from=

=C2=A0 =C2=A0 =C2=A0 =C2=A0the "Category", "Representation&q= uot;, the "Domain

=C2=A0 =C2=A0 =C2=A0 =C2=A0Local", and the signature pre- and post-

=C2=A0 =C2=A0 =C2=A0 =C2=A0conditions.

=C2=A0 =C2=A0I) literature links. Algorithms must contain a link

=C2=A0 =C2=A0 =C2=A0 to at least one literature reference. Of course,

=C2=A0 =C2=A0 =C2=A0 since everything I do is a Literate Program

=C2=A0 =C2=A0 =C2=A0 this is obviously required. Knuth said so :-)

LEAN ought to have "books" or "pamphlets" that

bring together all of this information for a domain

such as Square Matrices. That way a user can

find all of the related ideas, available functions,

and their corresponding proofs in one place.

6) User level presentation.

=C2=A0 =C2=A0 This is where the systems can differ significantly.

=C2=A0 =C2=A0 Axiom and LEAN both have GCD but they use

=C2=A0 =C2=A0 that for different purposes.

=C2=A0 =C2=A0 I'm trying to connect LEAN's GCD and Axiom's GCD<= br> =C2=A0 =C2=A0 so there is a "computational mathematics" idea that=

=C2=A0 =C2=A0 allows the user to connect proofs and implementations.

7) Trust

Unlike everything else, computational mathematics

can have proven code that gives various guarantees.

I have been working on this aspect for a while.

I refer to it as trust "down to the metal" The idea is

that a proof of the GCD function and the implementation

of the GCD function get packaged into the ELF format.

(proof carrying code). When the GCD algorithm executes

on the CPU, the GCD proof is run through the LEAN

proof checker on an FPGA in parallel.

(I just recently got a PYNQ Xilinx board [1] with a CPU

and FPGA together. I'm trying to implement the LEAN

proof checker on the FPGA).

We are on the cusp of a revolution in computational

mathematics. But the two pillars (proof and computer

algebra) need to get know each other.

Tim

[0] Lamport, Leslie "Chapter on TLA+"

in "Software Specification Methods"

https://www.springer.com/gp/book/9781852333539

(I no longer have CMU library access or I'd send you

the book PDF)

[1] https://www.tul.com.tw/productspynq-z2.html

[2] https://www.youtube.com/watch?v=3DdCuZkaaou0Q

[3] "ARTIFICIAL INTELLIGENCE MARKUP LANGUAGE"

https://arxiv.org/pdf/1307.3091.pdf

[4] ALICE Chatbot

http://www.scielo.org.mx/pdf/cys= /v19n4/1405-5546-cys-19-04-00625.pdf

[5] OPS5 User Manual

https://kilthub.cm= u.edu/articles/journal_contribution/OPS5_user_s_manual/6608090/1

[6] Scott Fahlman "SCONE"

http://www.cs.cmu.edu/~sef/scone/

On 9/27/21, Tim Daly <axiomcas@gmail.com> wrote:

> I have tried to maintain a list of names of people who have

> helped Axiom, going all the way back to the pre-Scratchpad

> days. The names are listed at the beginning of each book.

> I also maintain a bibliography of publications I've read or

> that have had an indirect influence on Axiom.

>

> Credit is "the coin of the realm". It is easy to share and w= rong

> to ignore. It is especially damaging to those in Academia who

> are affected by credit and citations in publications.

>

> Apparently I'm not the only person who feels that way. The ACM

> Turing award seems to have ignored a lot of work:

>

> Scientific Integrity, the 2021 Turing Lecture, and the 2018 Turing

> Award for Deep Learning

> https://pe= ople.idsia.ch/~juergen/scientific-integrity-turing-award-deep-learning.html=

>

> I worked on an AI problem at IBM Research called Ketazolam.

> (https://en.wikipedia.org/wiki/Ketazolam). The idea = was to recognize

> and associated 3D chemical drawings with their drug counterparts.

> I used Rumelhart, and McClelland's books. These books contained

> quite a few ideas that seem to be "new and innovative" among= the

> machine learning crowd... but the books are from 1987. I don't bel= ieve

> I've seen these books mentioned in any recent bibliography.

> https://mitpress.mit.edu= /books/parallel-distributed-processing-volume-1

>

>

>

>

> On 9/27/21, Tim Daly <axiomcas@gmail.com> wrote:

>> Greg Wilson asked "How Reliable is Scientific Software?"=

>> https://ne= verworkintheory.org/2021/09/25/how-reliable-is-scientific-software.html=

>>

>> which is a really interesting read. For example"

>>

>>=C2=A0 [Hatton1994], is now a quarter of a century old, but its con= clusions

>> are still fresh. The authors fed the same data into nine commercia= l

>> geophysical software packages and compared the results; they found=

>> that, "numerical disagreement grows at around the rate of 1% = in

>> average absolute difference per 4000 fines of implemented code, an= d,

>> even worse, the nature of the disagreement is nonrandom" (i.e= ., the

>> authors of different packages make similar mistakes).

>>

>>

>> On 9/26/21, Tim Daly <axiomcas@gmail.com> wrote:

>>> I should note that the lastest board I've just unboxed

>>> (a PYNQ-Z2) is a Zynq Z-7020 chip from Xilinx (AMD).

>>>

>>> What makes it interesting is that it contains 2 hard

>>> core processors and an FPGA, connected by 9 paths

>>> for communication. The processors can be run

>>> independently so there is the possibility of a parallel

>>> version of some Axiom algorithms (assuming I had

>>> the time, which I don't).

>>>

>>> Previously either the hard (physical) processor was

>>> separate from the FPGA with minimal communication

>>> or the soft core processor had to be created in the FPGA

>>> and was much slower.

>>>

>>> Now the two have been combined in a single chip.

>>> That means that my effort to run a proof checker on

>>> the FPGA and the algorithm on the CPU just got to

>>> the point where coordination is much easier.

>>>

>>> Now all I have to do is figure out how to program this

>>> beast.

>>>

>>> There is no such thing as a simple job.

>>>

>>> Tim

>>>

>>>

>>> On 9/26/21, Tim Daly <axiomcas@gmail.com> wrote:

>>>> I'm familiar with most of the traditional approaches>>>> like Theorema. The bibliography contains most of the

>>>> more interesting sources. [0]

>>>>

>>>> There is a difference between traditional approaches to

>>>> connecting computer algebra and proofs and my approach.

>>>>

>>>> Proving an algorithm, like the GCD, in Axiom is hard.

>>>> There are many GCDs (e.g. NNI vs POLY) and there

>>>> are theorems and proofs passed at runtime in the

>>>> arguments of the newly constructed domains. This

>>>> involves a lot of dependent type theory and issues of

>>>> compile time / runtime argument evaluation. The issues

>>>> that arise are difficult and still being debated in the ty= pe

>>>> theory community.

>>>>

>>>> I am putting the definitions, theorems, and proofs (DTP)>>>> directly into the category/domain hierarchy. Each category=

>>>> will have the DTP specific to it. That way a commutative>>>> domain will inherit a commutative theorem and a

>>>> non-commutative domain will not.

>>>>

>>>> Each domain will have additional DTPs associated with

>>>> the domain (e.g. NNI vs Integer) as well as any DTPs

>>>> it inherits from the category hierarchy. Functions in the<= br> >>>> domain will have associated DTPs.

>>>>

>>>> A function to be proven will then inherit all of the relev= ant

>>>> DTPs. The proof will be attached to the function and

>>>> both will be sent to the hardware (proof-carrying code).>>>>

>>>> The proof checker, running on a field programmable

>>>> gate array (FPGA), will be checked at runtime in

>>>> parallel with the algorithm running on the CPU

>>>> (aka "trust down to the metal"). (Note that Inte= l

>>>> and AMD have built CPU/FPGA combined chips,

>>>> currently only available in the cloud.)

>>>>

>>>>

>>>>

>>>> I am (slowly) making progress on the research.

>>>>

>>>> I have the hardware and nearly have the proof

>>>> checker from LEAN running on my FPGA.

>>>>

>>>> I'm in the process of spreading the DTPs from

>>>> LEAN across the category/domain hierarchy.

>>>>

>>>> The current Axiom build extracts all of the functions

>>>> but does not yet have the DTPs.

>>>>

>>>> I have to restructure the system, including the compiler>>>> and interpreter to parse and inherit the DTPs. I

>>>> have some of that code but only some of the code

>>>> has been pushed to the repository (volume 15) but

>>>> that is rather trivial, out of date, and incomplete.

>>>>

>>>> I'm clearly not smart enough to prove the Risch

>>>> algorithm and its associated machinery but the needed

>>>> definitions and theorems will be available to someone

>>>> who wants to try.

>>>>

>>>> [0] https://github.com/daly/= PDFS/blob/master/bookvolbib.pdf

>>>>

>>>>

>>>> On 8/19/21, Tim Daly <axiomcas@gmail.com> wrote:

>>>>> =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D

>>>>>

>>>>> REVIEW (Axiom on WSL2 Windows)

>>>>>

>>>>>

>>>>> So the steps to run Axiom from a Windows desktop

>>>>>

>>>>> 1 Windows) install XMing on Windows for X11 server

>>>>>

>>>>> http://www.straightrunning.com/XmingN= otes/

>>>>>

>>>>> 2 WSL2) Install Axiom in WSL2

>>>>>

>>>>> sudo apt install axiom

>>>>>

>>>>> 3 WSL2) modify /usr/bin/axiom to fix the bug:

>>>>> (someone changed the axiom startup script.

>>>>> It won't work on WSL2. I don't know who or

>>>>> how to get it fixed).

>>>>>

>>>>> sudo emacs /usr/bin/axiom

>>>>>

>>>>> (split the line into 3 and add quote marks)

>>>>>

>>>>> export SPADDEFAULT=3D/usr/local/axiom/mnt/linux

>>>>> export AXIOM=3D/usr/lib/axiom-20170501

>>>>> export "PATH=3D/usr/lib/axiom-20170501/bin:$PATH&= quot;

>>>>>

>>>>> 4 WSL2) create a .axiom.input file to include startup = cmds:

>>>>>

>>>>> emacs .axiom.input

>>>>>

>>>>> )cd "/mnt/c/yourpath"

>>>>> )sys pwd

>>>>>

>>>>> 5 WSL2) create a "myaxiom" command that sets= the

>>>>>=C2=A0 =C2=A0 =C2=A0DISPLAY variable and starts axiom>>>>>

>>>>> emacs myaxiom

>>>>>

>>>>> #! /bin/bash

>>>>> export DISPLAY=3D:0.0

>>>>> axiom

>>>>>

>>>>> 6 WSL2) put it in the /usr/bin directory

>>>>>

>>>>> chmod +x myaxiom

>>>>> sudo cp myaxiom /usr/bin/myaxiom

>>>>>

>>>>> 7 WINDOWS) start the X11 server

>>>>>

>>>>> (XMing XLaunch Icon on your desktop)

>>>>>

>>>>> 8 WINDOWS) run myaxiom from PowerShell

>>>>> (this should start axiom with graphics available)

>>>>>

>>>>> wsl myaxiom

>>>>>

>>>>> 8 WINDOWS) make a PowerShell desktop

>>>>>

>>>>> https://superuser.com/questions/886951/run-powershell-script-when-you= -open-powershell

>>>>>

>>>>> Tim

>>>>>

>>>>> On 8/13/21, Tim Daly <axiomcas@gmail.com> wrote:

>>>>>> A great deal of thought is directed toward making = the SANE version

>>>>>> of Axiom as flexible as possible, decoupling mecha= nism from theory.

>>>>>>

>>>>>> An interesting publication by Brian Cantwell Smith= [0], "Reflection

>>>>>> and Semantics in LISP" seems to contain inter= esting ideas related

>>>>>> to our goal. Of particular interest is the ability= to reason about

>>>>>> and

>>>>>> perform self-referential manipulations. In a depen= dently-typed

>>>>>> system it seems interesting to be able "adapt= " code to handle

>>>>>> run-time computed arguments to dependent functions= . The abstract:

>>>>>>

>>>>>>=C2=A0 =C2=A0 "We show how a computational sys= tem can be constructed to

>>>>>> "reason",

>>>>>> effectively

>>>>>>=C2=A0 =C2=A0 and consequentially, about its own in= ferential processes. The

>>>>>> analysis proceeds in two

>>>>>>=C2=A0 =C2=A0 parts. First, we consider the general= question of computational

>>>>>> semantics, rejecting

>>>>>>=C2=A0 =C2=A0 traditional approaches, and arguing t= hat the declarative and

>>>>>> procedural aspects of

>>>>>>=C2=A0 =C2=A0 computational symbols (what they stan= d for, and what behaviour

>>>>>> they

>>>>>> engender) should be

>>>>>>=C2=A0 =C2=A0 analysed independently, in order that= they may be coherently

>>>>>> related. Second, we

>>>>>>=C2=A0 =C2=A0 investigate self-referential behavior= in computational processes,

>>>>>> and show how to embed an

>>>>>>=C2=A0 =C2=A0 effective procedural model of a compu= tational calculus within that

>>>>>> calculus (a model not

>>>>>>=C2=A0 =C2=A0 unlike a meta-circular interpreter, b= ut connected to the

>>>>>> fundamental operations of the

>>>>>>=C2=A0 =C2=A0 machine in such a way as to provide, = at any point in a

>>>>>> computation,

>>>>>> fully articulated

>>>>>>=C2=A0 =C2=A0 descriptions of the state of that com= putation, for inspection and

>>>>>> possible modification). In

>>>>>>=C2=A0 =C2=A0 terms of the theories that result fro= m these investigations, we

>>>>>> present a general architecture

>>>>>>=C2=A0 =C2=A0 for procedurally reflective processes= , able to shift smoothly

>>>>>> between dealing with a given

>>>>>>=C2=A0 =C2=A0 subject domain, and dealing with thei= r own reasoning processes

>>>>>> over

>>>>>> that domain.

>>>>>>

>>>>>>=C2=A0 =C2=A0 An instance of the general solution i= s worked out in the context

>>>>>> of

>>>>>> an applicative

>>>>>>=C2=A0 =C2=A0 language. Specifically, we present th= ree successive dialects of

>>>>>> LISP: 1-LISP, a distillation of

>>>>>>=C2=A0 =C2=A0 current practice, for comparison purp= oses; 2-LISP, a dialect

>>>>>> constructed in terms of our

>>>>>>=C2=A0 =C2=A0 rationalised semantics, in which the = concept of evaluation is

>>>>>> rejected in favour of

>>>>>>=C2=A0 =C2=A0 independent notions of simplification= and reference, and in which

>>>>>> the respective categories

>>>>>>=C2=A0 =C2=A0 of notation, structure, semantics, an= d behaviour are strictly

>>>>>> aligned; and 3-LISP, an

>>>>>>=C2=A0 =C2=A0 extension of 2-LISP endowed with refl= ective powers."

>>>>>>

>>>>>> Axiom SANE builds dependent types on the fly. The = ability to access

>>>>>> both the refection

>>>>>> of the tower of algebra and the reflection of the = tower of proofs at

>>>>>> the time of construction

>>>>>> makes the construction of a new domain or specific= algorithm easier

>>>>>> and more general.

>>>>>>

>>>>>> This is of particular interest because one of the = efforts is to build

>>>>>> "all the way down to the

>>>>>> metal". If each layer is constructed on top o= f previous proven layers

>>>>>> and the new layer

>>>>>> can "reach below" to lower layers then t= he tower of layers can be

>>>>>> built without duplication.

>>>>>>

>>>>>> Tim

>>>>>>

>>>>>> [0], Smith, Brian Cantwell "Reflection and Se= mantics in LISP"

>>>>>> POPL '84: Proceedings of the 11th ACM SIGACT-S= IGPLAN

>>>>>> ymposium on Principles of programming languagesJan= uary 1

>>>>>> 984 Pages 23=E2=80=9335https://doi.org= /10.1145/800017.800513

>>>>>>

>>>>>> On 6/29/21, Tim Daly <axiomcas@gmail.com> wrote:

>>>>>>> Having spent time playing with hardware it is = perfectly clear that

>>>>>>> future computational mathematics efforts need = to adapt to using

>>>>>>> parallel processing.

>>>>>>>

>>>>>>> I've spent a fair bit of time thinking abo= ut structuring Axiom to

>>>>>>> be parallel. Most past efforts have tried to f= ocus on making a

>>>>>>> particular algorithm parallel, such as a matri= x multiply.

>>>>>>>

>>>>>>> But I think that it might be more effective to= make each domain

>>>>>>> run in parallel. A computation crosses multipl= e domains so a

>>>>>>> particular computation could involve multiple = parallel copies.

>>>>>>>

>>>>>>> For example, computing the Cylindrical Algebra= ic Decomposition

>>>>>>> could recursively decompose the plane. Indeed,= any tree-recursive

>>>>>>> algorithm could be run in parallel "in th= e large" by creating new

>>>>>>> running copies of the domain for each sub-prob= lem.

>>>>>>>

>>>>>>> So the question becomes, how does one manage t= his?

>>>>>>>

>>>>>>> A similar problem occurs in robotics where one= could have multiple

>>>>>>> wheels, arms, propellers, etc. that need to ac= t independently but

>>>>>>> in coordination.

>>>>>>>

>>>>>>> The robot solution uses ROS2. The three ideas = are ROSCORE,

>>>>>>> TOPICS with publish/subscribe, and SERVICES wi= th request/response.

>>>>>>> These are communication paths defined between = processes.

>>>>>>>

>>>>>>> ROS2 has a "roscore" which is basica= lly a phonebook of "topics".

>>>>>>> Any process can create or look up the current = active topics. eq:

>>>>>>>

>>>>>>>=C2=A0 =C2=A0 rosnode list

>>>>>>>

>>>>>>> TOPICS:

>>>>>>>

>>>>>>> Any process can PUBLISH a topic (which is basi= cally a typed data

>>>>>>> structure), e.g the topic /hw with the String = data "Hello World".

>>>>>>> eg:

>>>>>>>

>>>>>>>=C2=A0 =C2=A0 rostopic pub /hw std_msgs/String = "Hello, World"

>>>>>>>

>>>>>>> Any process can SUBSCRIBE to a topic, such as = /hw, and get a

>>>>>>> copy of the data.=C2=A0 eg:

>>>>>>>

>>>>>>>=C2=A0 =C2=A0 rostopic echo /hw=C2=A0 =C2=A0=3D= =3D> "Hello, World"

>>>>>>>

>>>>>>> Publishers talk, subscribers listen.

>>>>>>>

>>>>>>>

>>>>>>> SERVICES:

>>>>>>>

>>>>>>> Any process can make a REQUEST of a SERVICE an= d get a RESPONSE.

>>>>>>> This is basically a remote function call.

>>>>>>>

>>>>>>>

>>>>>>>

>>>>>>> Axiom in parallel?

>>>>>>>

>>>>>>> So domains could run, each in its own process.= It could provide

>>>>>>> services, one for each function. Any other pro= cess could request

>>>>>>> a computation and get the result as a response= . Domains could

>>>>>>> request services from other domains, either wa= iting for responses

>>>>>>> or continuing while the response is being comp= uted.

>>>>>>>

>>>>>>> The output could be sent anywhere, to a termin= al, to a browser,

>>>>>>> to a network, or to another process using the = publish/subscribe

>>>>>>> protocol, potentially all at the same time sin= ce there can be many

>>>>>>> subscribers to a topic.

>>>>>>>

>>>>>>> Available domains could be dynamically added b= y announcing

>>>>>>> themselves as new "topics" and could= be dynamically looked-up

>>>>>>> at runtime.

>>>>>>>

>>>>>>> This structure allows function-level / domain-= level parallelism.

>>>>>>> It is very effective in the robot world and I = think it might be a

>>>>>>> good structuring mechanism to allow computatio= nal mathematics

>>>>>>> to take advantage of multiple processors in a = disciplined fashion.

>>>>>>>

>>>>>>> Axiom has a thousand domains and each could ru= n on its own core.

>>>>>>>

>>>>>>> In addition. notice that each domain is indepe= ndent of the others.

>>>>>>> So if we want to use BLAS Fortran code, it cou= ld just be another

>>>>>>> service node. In fact, any "foreign funct= ion" could transparently

>>>>>>> cooperate in a distributed Axiom.

>>>>>>>

>>>>>>> Another key feature is that proofs can be &quo= t;by node".

>>>>>>>

>>>>>>> Tim

>>>>>>>

>>>>>>>

>>>>>>>

>>>>>>>

>>>>>>> On 6/5/21, Tim Daly <axiomcas@gmail.com> wrote:

>>>>>>>> Axiom is based on first-class dependent ty= pes. Deciding when

>>>>>>>> two types are equivalent may involve compu= tation. See

>>>>>>>> Christiansen, David Thrane "Checking = Dependent Types with

>>>>>>>> Normalization by Evaluation" (2019)>>>>>>>>

>>>>>>>> This puts an interesting constraint on bui= lding types. The

>>>>>>>> constructed types has to export a function= to decide if a

>>>>>>>> given type is "equivalent" to it= self.

>>>>>>>>

>>>>>>>> The notion of "equivalence" migh= t involve category ideas

>>>>>>>> of natural transformation and univalence. = Sigh.

>>>>>>>>

>>>>>>>> That's an interesting design point.

>>>>>>>>

>>>>>>>> Tim

>>>>>>>>

>>>>>>>>

>>>>>>>> On 5/5/21, Tim Daly <axiomcas@gmail.com> wrote:

>>>>>>>>> It is interesting that programmer'= s eyes and expectations adapt

>>>>>>>>> to the tools they use. For instance, I= use emacs and expect to

>>>>>>>>> work directly in files and multiple bu= ffers. When I try to use one

>>>>>>>>> of the many IDE tools I find they tend= to "get in the way". I

>>>>>>>>> already

>>>>>>>>> know or can quickly find whatever they= try to tell me. If you use

>>>>>>>>> an

>>>>>>>>> IDE you probably find emacs "too = sparse" for programming.

>>>>>>>>>

>>>>>>>>> Recently I've been working in a sp= arse programming environment.

>>>>>>>>> I'm exploring the question of runn= ing a proof checker in an FPGA.

>>>>>>>>> The FPGA development tools are painful= at best and not intuitive

>>>>>>>>> since you SEEM to be programming but y= ou're actually describing

>>>>>>>>> hardware gates, connections, and timin= g. This is an environment

>>>>>>>>> where everything happens all-at-once a= nd all-the-time (like the

>>>>>>>>> circuits in your computer). It is the = "assembly language of

>>>>>>>>> circuits".

>>>>>>>>> Naturally, my eyes have adapted to thi= s rather raw level.

>>>>>>>>>

>>>>>>>>> That said, I'm normally doing lite= rate programming all the time.

>>>>>>>>> My typical file is a document which is= a mixture of latex and

>>>>>>>>> lisp.

>>>>>>>>> It is something of a shock to return t= o that world. It is clear

>>>>>>>>> why

>>>>>>>>> people who program in Python find lisp= to be a "sea of parens".

>>>>>>>>> Yet as a lisp programmer, I don't = even see the parens, just code.

>>>>>>>>>

>>>>>>>>> It takes a few minutes in a literate d= ocument to adapt vision to

>>>>>>>>> see the latex / lisp combination as na= tural. The latex markup,

>>>>>>>>> like the lisp parens, eventually just = disappears. What remains

>>>>>>>>> is just lisp and natural language text= .

>>>>>>>>>

>>>>>>>>> This seems painful at first but eyes q= uickly adapt. The upside

>>>>>>>>> is that there is always a "finish= ed" document that describes the

>>>>>>>>> state of the code. The overhead of wri= ting a paragraph to

>>>>>>>>> describe a new function or change a pa= ragraph to describe the

>>>>>>>>> changed function is very small.

>>>>>>>>>

>>>>>>>>> Using a Makefile I latex the document = to generate a current PDF

>>>>>>>>> and then I extract, load, and execute = the code. This loop catches

>>>>>>>>> errors in both the latex and the sourc= e code. Keeping an open file

>>>>>>>>> in

>>>>>>>>> my pdf viewer shows all of the changes= in the document after every

>>>>>>>>> run of make. That way I can edit the b= ook as easily as the code.

>>>>>>>>>

>>>>>>>>> Ultimately I find that writing the boo= k while writing the code is

>>>>>>>>> more productive. I don't have to r= emember why I wrote something

>>>>>>>>> since the explanation is already there= .

>>>>>>>>>

>>>>>>>>> We all have our own way of programming= and our own tools.

>>>>>>>>> But I find literate programming to be = a real advance over IDE

>>>>>>>>> style programming and "raw code&q= uot; programming.

>>>>>>>>>

>>>>>>>>> Tim

>>>>>>>>>

>>>>>>>>>

>>>>>>>>> On 2/27/21, Tim Daly <axiomcas@gmail.com> wrote= :

>>>>>>>>>> The systems I use have the interes= ting property of

>>>>>>>>>> "Living within the compiler&q= uot;.

>>>>>>>>>>

>>>>>>>>>> Lisp, Forth, Emacs, and other syst= ems that present themselves

>>>>>>>>>> through the Read-Eval-Print-Loop (= REPL) allow the

>>>>>>>>>> ability to deeply interact with th= e system, shaping it to your

>>>>>>>>>> need.

>>>>>>>>>>

>>>>>>>>>> My current thread of study is soft= ware architecture. See

>>>>>>>>>> https://www.youtube.com/watch?v=3DW2hagw1VhhI&feature=3Dyoutu.= be

>>>>>>>>>> and https://www.geor= gefairbanks.com/videos/

>>>>>>>>>>

>>>>>>>>>> My current thinking on SANE involv= es the ability to

>>>>>>>>>> dynamically define categories, rep= resentations, and functions

>>>>>>>>>> along with "composition funct= ions" that permits choosing a

>>>>>>>>>> combination at the time of use.

>>>>>>>>>>

>>>>>>>>>> You might want a domain for handli= ng polynomials. There are

>>>>>>>>>> a lot of choices, depending on you= r use case. You might want

>>>>>>>>>> different representations. For exa= mple, you might want dense,

>>>>>>>>>> sparse, recursive, or "machin= e compatible fixnums" (e.g. to

>>>>>>>>>> interface with C code). If these d= on't exist it ought to be

>>>>>>>>>> possible

>>>>>>>>>> to create them. Such "lego-li= ke" building blocks require careful

>>>>>>>>>> thought about creating "fully= factored" objects.

>>>>>>>>>>

>>>>>>>>>> Given that goal, the traditional b= arrier of "compiler" vs

>>>>>>>>>> "interpreter"

>>>>>>>>>> does not seem useful. It is better= to "live within the compiler"

>>>>>>>>>> which

>>>>>>>>>> gives the ability to define new th= ings "on the fly".

>>>>>>>>>>

>>>>>>>>>> Of course, the SANE compiler is go= ing to want an associated

>>>>>>>>>> proof of the functions you create = along with the other parts

>>>>>>>>>> such as its category hierarchy and= representation properties.

>>>>>>>>>>

>>>>>>>>>> There is no such thing as a simple= job. :-)

>>>>>>>>>>

>>>>>>>>>> Tim

>>>>>>>>>>

>>>>>>>>>>

>>>>>>>>>> On 2/18/21, Tim Daly <axiomcas@gmail.com>= wrote:

>>>>>>>>>>> The Axiom SANE compiler / inte= rpreter has a few design points.

>>>>>>>>>>>

>>>>>>>>>>> 1) It needs to mix interpreted= and compiled code in the same

>>>>>>>>>>> function.

>>>>>>>>>>> SANE allows dynamic constructi= on of code as well as dynamic type

>>>>>>>>>>> construction at runtime. Both = of these can occur in a runtime

>>>>>>>>>>> object.

>>>>>>>>>>> So there is potentially a mixt= ure of interpreted and compiled

>>>>>>>>>>> code.

>>>>>>>>>>>

>>>>>>>>>>> 2) It needs to perform type re= solution at compile time without

>>>>>>>>>>> overhead

>>>>>>>>>>> where possible. Since this is = not always possible there needs to

>>>>>>>>>>> be

>>>>>>>>>>> a "prefix thunk" tha= t will perform the resolution. Trivially,

>>>>>>>>>>> for

>>>>>>>>>>> example,

>>>>>>>>>>> if we have a + function we nee= d to type-resolve the arguments.

>>>>>>>>>>>

>>>>>>>>>>> However, if we can prove at co= mpile time that the types are both

>>>>>>>>>>> bounded-NNI and the result is = bounded-NNI (i.e. fixnum in lisp)

>>>>>>>>>>> then we can inline a call to += at runtime. If not, we might have

>>>>>>>>>>> + applied to NNI and POLY(FLOA= T), which requires a thunk to

>>>>>>>>>>> resolve types. The thunk could= even "specialize and compile"

>>>>>>>>>>> the code before executing it.<= br> >>>>>>>>>>>

>>>>>>>>>>> It turns out that the Forth im= plementation of

>>>>>>>>>>> "threaded-interpreted&quo= t;

>>>>>>>>>>> languages model provides an ef= ficient and effective way to do

>>>>>>>>>>> this.[0]

>>>>>>>>>>> Type resolution can be "i= nserted" in intermediate thunks.

>>>>>>>>>>> The model also supports dynami= c overloading and tail recursion.

>>>>>>>>>>>

>>>>>>>>>>> Combining high-level CLOS code= with low-level threading gives an

>>>>>>>>>>> easy to understand and robust = design.

>>>>>>>>>>>

>>>>>>>>>>> Tim

>>>>>>>>>>>

>>>>>>>>>>> [0] Loeliger, R.G. "Threa= ded Interpretive Languages" (1981)

>>>>>>>>>>> ISBN 0-07-038360-X

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>> On 2/5/21, Tim Daly <axiomcas@gmail.com>= ; wrote:

>>>>>>>>>>>> I've worked hard to ma= ke Axiom depend on almost no other

>>>>>>>>>>>> tools so that it would not= get caught by "code rot" of

>>>>>>>>>>>> libraries.

>>>>>>>>>>>>

>>>>>>>>>>>> However, I'm also tryi= ng to make the new SANE version much

>>>>>>>>>>>> easier to understand and d= ebug.To that end I've been

>>>>>>>>>>>> experimenting

>>>>>>>>>>>> with some ideas.

>>>>>>>>>>>>

>>>>>>>>>>>> It should be possible to v= iew source code, of course. But the

>>>>>>>>>>>> source

>>>>>>>>>>>> code is not the only, nor = possibly the best, representation of

>>>>>>>>>>>> the

>>>>>>>>>>>> ideas.

>>>>>>>>>>>> In particular, source code= gets compiled into data structures.

>>>>>>>>>>>> In

>>>>>>>>>>>> Axiom

>>>>>>>>>>>> these data structures real= ly are a graph of related structures.

>>>>>>>>>>>>

>>>>>>>>>>>> For example, looking at th= e gcd function from NNI, there is the

>>>>>>>>>>>> representation of the gcd = function itself. But there is also a

>>>>>>>>>>>> structure

>>>>>>>>>>>> that is the REP (and, in t= he new system, is separate from the

>>>>>>>>>>>> domain).

>>>>>>>>>>>>

>>>>>>>>>>>> Further, there are associa= ted specification and proof

>>>>>>>>>>>> structures.

>>>>>>>>>>>> Even

>>>>>>>>>>>> further, the domain inheri= ts the category structures, and from

>>>>>>>>>>>> those

>>>>>>>>>>>> it

>>>>>>>>>>>> inherits logical axioms an= d definitions through the proof

>>>>>>>>>>>> structure.

>>>>>>>>>>>>

>>>>>>>>>>>> Clearly the gcd function i= s a node in a much larger graph

>>>>>>>>>>>> structure.

>>>>>>>>>>>>

>>>>>>>>>>>> When trying to decide why = code won't compile it would be useful

>>>>>>>>>>>> to

>>>>>>>>>>>> be able to see and walk th= ese structures. I've thought about

>>>>>>>>>>>> using

>>>>>>>>>>>> the

>>>>>>>>>>>> browser but browsers are t= oo weak. Either everything has to be

>>>>>>>>>>>> "in

>>>>>>>>>>>> a

>>>>>>>>>>>> single tab to show the gra= ph" or "the nodes of the graph are in

>>>>>>>>>>>> different

>>>>>>>>>>>> tabs". Plus, construc= ting dynamic graphs that change as the

>>>>>>>>>>>> software

>>>>>>>>>>>> changes (e.g. by loading a= new spad file or creating a new

>>>>>>>>>>>> function)

>>>>>>>>>>>> represents the huge proble= m of keeping the browser "in sync

>>>>>>>>>>>> with

>>>>>>>>>>>> the

>>>>>>>>>>>> Axiom workspace". So = something more dynamic and embedded is

>>>>>>>>>>>> needed.

>>>>>>>>>>>>

>>>>>>>>>>>> Axiom source gets compiled= into CLOS data structures. Each of

>>>>>>>>>>>> these

>>>>>>>>>>>> new SANE structures has an= associated surface representation,

>>>>>>>>>>>> so

>>>>>>>>>>>> they

>>>>>>>>>>>> can be presented in user-f= riendly form.

>>>>>>>>>>>>

>>>>>>>>>>>> Also, since Axiom is liter= ate software, it should be possible

>>>>>>>>>>>> to

>>>>>>>>>>>> look

>>>>>>>>>>>> at

>>>>>>>>>>>> the code in its literate f= orm with the surrounding explanation.

>>>>>>>>>>>>

>>>>>>>>>>>> Essentially we'd like = to have the ability to "deep dive" into

>>>>>>>>>>>> the

>>>>>>>>>>>> Axiom

>>>>>>>>>>>> workspace, not only for de= bugging, but also for understanding

>>>>>>>>>>>> what

>>>>>>>>>>>> functions are used, where = they come from, what they inherit,

>>>>>>>>>>>> and

>>>>>>>>>>>> how they are used in a com= putation.

>>>>>>>>>>>>

>>>>>>>>>>>> To that end I'm lookin= g at using McClim, a lisp windowing

>>>>>>>>>>>> system.

>>>>>>>>>>>> Since the McClim windows w= ould be part of the lisp image, they

>>>>>>>>>>>> have

>>>>>>>>>>>> access to display (and mod= ify) the Axiom workspace at all

>>>>>>>>>>>> times.

>>>>>>>>>>>>

>>>>>>>>>>>> The only hesitation is tha= t McClim uses quicklisp and drags in

>>>>>>>>>>>> a

>>>>>>>>>>>> lot

>>>>>>>>>>>> of other subsystems. It= 9;s all lisp, of course.

>>>>>>>>>>>>

>>>>>>>>>>>> These ideas aren't new= . They were available on Symbolics

>>>>>>>>>>>> machines,

>>>>>>>>>>>> a truly productive platfor= m and one I sorely miss.

>>>>>>>>>>>>

>>>>>>>>>>>> Tim

>>>>>>>>>>>>

>>>>>>>>>>>>

>>>>>>>>>>>>

>>>>>>>>>>>> On 1/19/21, Tim Daly <<= a href=3D"mailto:axiomcas@gmail.com" target=3D"_blank">axiomcas@gmail.com> wrote:

>>>>>>>>>>>>> Also of interest is th= e talk

>>>>>>>>>>>>> "The Unreasonable= Effectiveness of Dynamic Typing for

>>>>>>>>>>>>> Practical

>>>>>>>>>>>>> Programs"

>>>>>>>>>>>>> https://vimeo.com/743= 54480

>>>>>>>>>>>>> which questions whethe= r static typing really has any benefit.

>>>>>>>>>>>>>

>>>>>>>>>>>>> Tim

>>>>>>>>>>>>>

>>>>>>>>>>>>>

>>>>>>>>>>>>> On 1/19/21, Tim Daly &= lt;axiomcas@gmail.c= om> wrote:

>>>>>>>>>>>>>> Peter Naur wrote a= n article of interest:

>>>>>>>>>>>>>> htt= p://pages.cs.wisc.edu/~remzi/Naur.pdf

>>>>>>>>>>>>>>

>>>>>>>>>>>>>> In particular, it = mirrors my notion that Axiom needs

>>>>>>>>>>>>>> to embrace literat= e programming so that the "theory

>>>>>>>>>>>>>> of the problem&quo= t; is presented as well as the "theory

>>>>>>>>>>>>>> of the solution&qu= ot;. I quote the introduction:

>>>>>>>>>>>>>>

>>>>>>>>>>>>>>

>>>>>>>>>>>>>>

>>>>>>>>>>>>>> This article is, t= o my mind, the most accurate account

>>>>>>>>>>>>>> of what goes on in= designing and coding a program.

>>>>>>>>>>>>>> I refer to it regu= larly when discussing how much

>>>>>>>>>>>>>> documentation to c= reate, how to pass along tacit

>>>>>>>>>>>>>> knowledge, and the= value of the XP's metaphor-setting

>>>>>>>>>>>>>> exercise. It also = provides a way to examine a methodolgy's

>>>>>>>>>>>>>> economic structure= .

>>>>>>>>>>>>>>

>>>>>>>>>>>>>> In the article, wh= ich follows, note that the quality of the

>>>>>>>>>>>>>> designing programm= er's work is related to the quality of

>>>>>>>>>>>>>> the match between = his theory of the problem and his theory

>>>>>>>>>>>>>> of the solution. N= ote that the quality of a later

>>>>>>>>>>>>>> programmer's>>>>>>>>>>>>>> work is related to= the match between his theories and the

>>>>>>>>>>>>>> previous programme= r's theories.

>>>>>>>>>>>>>>

>>>>>>>>>>>>>> Using Naur's i= deas, the designer's job is not to pass along

>>>>>>>>>>>>>> "the design&q= uot; but to pass along "the theories" driving the

>>>>>>>>>>>>>> design.

>>>>>>>>>>>>>> The latter goal is= more useful and more appropriate. It also

>>>>>>>>>>>>>> highlights that kn= owledge of the theory is tacit in the

>>>>>>>>>>>>>> owning,

>>>>>>>>>>>>>> and

>>>>>>>>>>>>>> so passing along t= he thoery requires passing along both

>>>>>>>>>>>>>> explicit

>>>>>>>>>>>>>> and tacit knowledg= e.

>>>>>>>>>>>>>>

>>>>>>>>>>>>>> Tim

>>>>>>>>>>>>>>

>>>>>>>>>>>>>

>>>>>>>>>>>>

>>>>>>>>>>>

>>>>>>>>>>

>>>>>>>>>

>>>>>>>>

>>>>>>>

>>>>>>

>>>>>

>>>>

>>>

>>

>