Hi Dan,
So, in a nutshell, you've got N proof scripts in HOL Light that you want
to fit together as one coherent proof in a single session, but that
would take far too much processing to do so in practice. So you want to
execute these in N parallel HOL Light sessions, recording the
kernel-level steps as they happen, and export these, and replay them all
in a single HOL Light session.
This is basically known as "proof recording", and an exported proof is
known as a "proof object". There have been various attempts at proof
recording in HOL Systems over the years, including Wong (1990s),
Skalberg & Obua (2000s), Kaliszyk & Krauss (2010s), Hurd's Open Theory
project (2010s) and my Common HOL project (2010s). Section 4.5 of my
paper on proof auditing includes a brief overview of these. As you say,
most recording systems are designed for either porting proofs between
two specific proof systems (either two proof assistants or a proof
assistant and its sister proof checker), but Open Theory and Common HOL
were designed for porting between any two HOL systems (including back
into the same system).
You're absolutely right that the replay has potential to be much faster
than executing the original proof scripts, given that search does not
need to be replicated during replay. But there are numerous challenges
to overcome to make it tractable. Even though a basic proof recording
system can be written in a few hundred lines of ML, recording a large
proof would probably use up huge amounts of RAM/diskspace, and probably
not result in that much of a speed up during replay. However, some
recording systems do much better than that. I'm not sure about the
latest developments for other systems, but back in 2015 my recording
system for Common HOL recorded the "text formalisation" part of Flyspeck
in HOL Light (1.3bn primitive proof steps) using modest RAM/CPU, and
managed to get replay in HOL Light down by a factor of 7, and I think
that this could go down by another factor of 2 (so perhaps 15 in total)
with a bit of extra work, but this is nowhere near the 100x speedup you
envisage. Would that meet your requirements? May I ask what the
application is?
Mark.
On 25/01/2021 13:40, D. J. Bernstein wrote:
I have another newbie question regarding HOL Light; again happy to hear
about other HOL variants if those have easier answers.
I'm in the typical post-human-proof situation where a program found a
"proof" that's too tedious for a human to verify (in the conventional
sense, not PCPs). For verification, I'm converting the "proof" into a
HOL Light proof: auto-generating the whole chain of intermediate steps
as definitions, and auto-generating all the theorems linking the
definitions. This works fine on scaled-down examples, and extrapolation
suggests that the CPU time for HOL Light will still be affordable when
scaled up to the full theorem, in the ballpark of 10000 core-hours.
It's no problem to farm the separate proof steps out to separate cores,
each using its own subset of the relevant definitions, at which point I
have one instance of HOL Light printing out a theorem saying A implies
B, and a separate instance of HOL Light printing out a theorem saying B
implies C, and so on. This brings me to the question: how can I have
HOL
Light printing out the combined theorem saying that A implies Z,
without
waiting 10000 hours for HOL Light on one core to serially run through
proving all the lemmas?
I'd guess that >99% of the CPU time I'm seeing comes from HOL Light
searching for proofs (e.g., the computation in REAL_LINEAR_PROVER), and
that far less is spent by the HOL Light kernel verifying the proofs. Is
there a generic mechanism to record merely what the kernel is doing---
i.e., to automatically write down a proof in the conventional sense---
and then replay this proof in another HOL Light instance that has the
same definitions?
The papers I've found on the problem of exporting libraries of theorems
from one system to another sound like that's only partially solved, but
that's also a conceptually more difficult problem than simply replaying
the lowest level of proof within a single system. I did various other
searches for answers and didn't find anything---sorry if I missed
something obvious. In general the small kernel makes me think that
tracing proofs wouldn't be touching many lines of code, but I haven't
studied the kernel closely enough to be confident about this.
In case this (1) doesn't exist and (2) is hard to build, my backup plan
is to modify the program printing out the proof tactics to do its own
searches for lower-level proof steps. Conceptually this would be
copying
the searches implemented in HOL Light, so presumably the speed will end
up similar, but the searches would then be easily distributable
precomputation, which is the objective---I'd just like to reach this
without the waste of time of reimplementing something that HOL Light
already knows how to do!
---Dan
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
