TheoryLearner.pl (Script trying to solve multiple problems in large theory by learning from successes)
TheoryLearner.pl [options] filestem
time ./TheoryLearner.pl --fileprefix='chainy_lemma1/' --filepostfix='.ren' chainy1 | tee chainy1.log
Options:
--commonfile=<arg>, -c<arg>
--problemsfile=<arg> -o<arg>
--uniquify=<arg>, -F<arg>
--fileprefix=<arg>, -e<arg>
--filepostfix=<arg>, -s<arg>
--tmpdir=<arg>, -T<arg>
--maxcpulimit=<arg>, -C<arg>
--mincpulimit=<arg>, -U<arg>
--maxaxiomlimit=<arg>, -A<arg>
--permutetimelimit=<arg>, -P<arg>
--dofull=<arg>, -f<arg>
--iterrecover=<arg>, -I<arg>
--loadprovedby=<arg>, -B<arg>
--runeprover=<arg>, -E<arg>
--runspass=<arg>, -S<arg>
--runvampire=<arg>, -V<arg>
--runparadox=<arg>, -p<arg>
--runmace=<arg>, -M<arg>
--maceemul=<arg>, -l<arg>
--usemodels=<arg>, -D<arg>
--incrmodels=<arg>, -N<arg>
--srassemul=<arg>, -R<arg>
--countersatcheck=<arg>, -k<arg>
--similarity=<arg>, -i<arg>
--generalize=<arg>, -g<arg>
--parallelize=<arg>, -j<arg>
--iterpolicy=<arg>, -y<arg>
--learnpolicy=<arg>, -O<arg>
--iterlimit=<arg>, -t<arg>
--recadvice=<arg>, -a<arg>
--snowserver=<arg>, -W<arg>
--reuseeval=<arg>, -u<arg>
--limittargets=<arg>, -L<arg>
--boostlimit=<arg>, -b<arg>
--boostweight=<arg>, -w<arg>
--refsbgcheat=<arg>, -r<arg>
--alwaysmizrefs=<arg>, -m<arg>
--tptpproofs=<arg>, -z<arg>
--help, -h
--man
- --commonfile=<arg, -c<arg> >>>
-
One common file containing all axioms and conjectures that should be proved
from them. If an extra axiom is needed in this input scenario for a conjecture,
it has to be added as an antecedent of an implication. The --fileprefix
option is mandatory in this case, specifying the directory for autogenerated
problem files.
- --problemsfile=<arg, -o<arg> >>>
-
One file containing pairs of absolute problem file names and
absolute output file names for solutions. This is the setup
used in CASC LTB division.
The --fileprefix option is mandatory in this case, specifying the working
directory. The --uniquify option is likely to be needed too, at least for
renaming file names and conjectures.
- --uniquify=<arg, -F<arg> >>>
-
If > 0, the formula names in problems are not assumed to be consistent, and
the naming of conjectures does not have to correspond to the problem names.
This means that problem names will be changed, so that conjecture names
could be derived from them, different formulas with the same name will be
disjointly renamed, and same formulas with different names will be jointly
renamed in all problems (with the exception of the same conjecture shared
by two different problems).
The name mappings are remembered, i.e., a mapping of problem names is kept,
and for each problem, the original names of its formulas are kept.
This can be used to observe the CASC solution format (see also --problemsfile).
The default is 0 (experimental so far).
See uniquify.pl in the script directory for implementation.
- --fileprefix=<arg, -e<arg> >>>
-
Prefix saying how to create problem file names from conjecture names.
It is prepended to the conjecture name (and can contain directory part ended with /).
If the --commonfile option was used, this tells the directory used for
autogenerated problem files (the directory must not exist).
- --filepostfix=<arg, -s<arg> >>>
-
Postfix saying how to create problem file names from conjecture names.
It is appended to the conjecture name (typically a file extension).
- --tmpdir=<arg, -T<arg> >>>
-
Directory (slash-ended) for temporary problem and result files.
Defaults to ``'', which means no usage of any special directory.
Otherwise, the tmpdir/fileprefix directory must not previously exist.
The /tmp/ is usable, however /dev/shm/ or similar memory-based
(tmpfs) location is strongly recommended, because the number of
these files is large. After each pass, these files are tgz-ed
into a .pass_nr file, and deleted.
- --maxcpulimit=<arg, -C<arg> >>>
-
Upper limit to which the CPU time for one ATP attempt is grown
exponentially (multiplied by 4 and starting from 1 second base).
The default is 16 seconds (should be power of 4)
- --mincpulimit=<arg, -U<arg> >>>
-
Lower limit for the CPU time for one ATP attempt.
The default is 1 second (should be power of 4).
- --maxaxiomlimit=<arg, -A<arg> >>>
-
Upper limit to which the number of axioms used for one ATP attempt is grown
exponentially (multiplied by 2 and starting from 4 axioms).
The default is 128 axioms (should be power of 2).
- --permutetimelimit=<arg, -P<arg> >>>
-
Upper time limit upto which fixing of subsumed specifications is done.
I.e. if a specification suggested by the adviser is subsumed, and
the suggested timelimit is less or equal to permutetimelimit, then
the specification will be fixed by adding additional axioms
in order of their relevance. The fixing method is influnced
by --countersatcheck.
Default is equal to mincpulimit. If 0, no fixing is done.
- --dofull=<arg, -f<arg> >>>
-
If 1, the first pass is a max-timelimit run on full problems.
If 2, the first pass is a min-timelimit run on full problems.
If 0, that pass is omitted, and the symbol-only pass is the first run.
Default is 1.
- --iterrecover=<arg, -I<arg> >>>
-
Instead of starting fresh, assume that iteration passed as arg
was already done. Load the result table and all other needed
tables, and continue with the next iteration.
- --loadprovedby=<arg, -B<arg> >>>
-
Load the initial proved_by table from the given file.
Otherwise, the default initial proved_by table contains for each formulas
the info that it can be proved by itself (this initializes the learning).
If an entry for some formula is missing in the given file,
the default info will be added for it.
- --runeprover=<arg, -E<arg> >>>
-
If >= 1, run E. Default is 1.
If greater than 1, run only in passes where the number
of refs is not greater than this.
- --runspass=<arg, -S<arg> >>>
-
If >= 1, run SPASS. Default is 1.
If greater than 1, run only in passes where the number
of refs is not greater than this.
- --runvampire=<arg, -V<arg> >>>
-
If >= 1, run Vampire. Default is 0.
If greater than 1, run only in passes where the number
of refs is not greater than this.
- --runparadox=<arg, -p<arg> >>>
-
If >= 1, run Paradox. Default is 0.
If greater than 1, run only in passes where the number
of refs is not greater than this. Good nonzero default
is then 128.
- --runmace=<arg, -M<arg> >>>
-
If >= 1, and running Paradox, run also Mace to construct a model.
If greater than 1, run only in passes where the number
of refs is not greater than this.
The model is then used for evaluation of formulas. Default is 64,
because this is constraint by --runparadox anyway.
- --maceemul=<arg, -l<arg> >>>
-
If >= 1, and running Paradox, try to forge a Mace4 model
using the prdxprep.pl and prdx2p9.pl programs on Pradaox output. This
replaces running Mace to create the model, which sometimes fails
(Mace avoids models of cardinality 1).
Default is 0 - is experimental.
- --usemodels=<arg, -D<arg> >>>
-
Use models for learning relevance of formulas. If 1, only negative
models are used, if 2, only positive models are used, if 3,
both positive and negative models are used, if 0, none are used.
Default is 1. This asssumes --runmace=1 or --maceemul=1.
- --incrmodels=<arg, -N<arg> >>>
-
If 1, printing and learning of models is done incrementally,
i.e. a new example is printed for each fla that has a new model
found in the last iteration. If 0, the nonincremental (older)
implementation is used, printing the whole models info
for all iterations as one example for each fla with a model.
Default is 0 (more tested). This assumes --usemodels>0.
- --srassemul=<arg, -R<arg> >>>
-
If 1, and running Mace (i.e. models are used), try to extend problem
specifications using the SRASS algorithm. That is: axioms that were
evaluated as false in some model of the negated conjecture are
greedily added (in order of their relevance) until all such models
are covered (or we run out of falsifying axioms).
Default is 1, because this is constraint by --runmace=1 or --maceemul=1 anyway.
- --countersatcheck=<arg, -k<arg> >>>
-
Default is 1, which means that if a suggested specification is
a subset of a specification that is already known to be countersatisfiable,
axioms will be greedily added (by relevance) until it is no longer
known to be countersatisfiable.
If 2, and --runmace=1 or --maceemul=1 (i.e. models are used), the
model info will be used to fix countersatisfiable specifications. That is,
if a model was found for a previous countersatisfiable specification S, all formulas
will be evaluated in the model, and usually many more will be known to be true
in the model than just the axioms of the specification S. So instead of extending
just the countersatisfiable specifications, the whole set of true axioms has to be
extended for each model. This is a bit related to --srassemul.
Use --permutetimelimit=0 to switch off fixing of countersatisfiable specs completely.
- --similarity=<arg, -i<arg> >>>
-
The similarity measure for formulas. If 1, only vector of symbols
is used, if 2, only codes of shared terms are used, if 4, the shared terms
are first normalized by renaming all variables to just one generic variable.
Combinations of these basic methods can be done by summing their codes
(i.e., value 7 would tell to use all of them).
Default is 1 (symbols only).
- --generalize=<arg, -g<arg> >>>
-
The generalization method for formulas. If 0, no generalization is done.
If 1, new generalized formulas are created by replacing all local constants
in formulas with a new special symbol. The generalized formulas
become learning targets exactly as the original ones, and they are included
into training whenever some corresponding original formula is. Accordingly,
when a generalized fla is recommended by the trained system as an axiom,
the corresponding original flas become recommended.
Default is 0.
- --parallelize=<arg, -j<arg> >>>
-
If greater than 1, runs problems in parallel, using Makefile with
the -j<arg> option. Currently works only with E.
Default is 1 - no parallelization.
- --iterpolicy=<arg, -y<arg> >>>
-
Policy for iterations. Default is 0 - the standard learning greedy,
minimal axioms loop. Another implemented option is 1: prefers
to grow the axiomlimit to the maximum regardless of previous
success, and only when it is maximal, it drops to the lowest value.
- --learnpolicy=<arg, -O<arg> >>>
-
Policy for learning. Default is 0 - learning is always done.
If > 1, and --iterpolicy is 1, learning only occurs when the maximum
values of the axiomlimit is reached. This can speed things up
when learning is slow, the price is that the new info is not available
immediatelly.
- --iterlimit=<arg, -t<arg> >>>
-
Depending on the iterpolicy, this is the maximal/minimal number of
iterations. If iterpolicy is 0, it is maximum, otherwise minimum.
One particular use is to set maxcpulimit to 1, iterpolicy to 1,
and this to e.g. 200. It ensures that 200 iterations with
timilimit 1 will be done repetitively through all axiom thresholds,
even if nothing new was learned (so setting permutetimelimit
to a reasonable value is recommended, as it is the only source of
possible new results). Defaults to 10000 with the standard iterpolicy,
and to 50 with the axiomlimit growth policy.
- --recadvice=<arg, -a<arg> >>>
-
If nonzero, the axiom advising phase is repeated this many times,
recursively using the recommended axioms to enlarge the set of symbols
for the next advising phase. Default is 0 (no recursion).
- --snowserver=<arg, -W<arg> >>>
-
If nonzero, snow is running as server for iterations > 3,
learning only the new info and not re-learning all things again.
If --usemodels>0, it will set --incrmodels to 1, so that
only the new model info could be used. This should speed things
up with large numbers of targets, however it is not clear if
snow really can learn in the server mode, so the default is 0.
- --reuseeval=<arg, -u<arg> >>>
-
If nonzero, the evaluation of the learner is stored after each pass
(can be a huge file), and if nothing new was proved in the previous
pass, it is re-used (instead of running the same evaluation).
The current implementation will conflict with the modelinfo features,
so don't use it if usemodels is on.
Default is 0 (no re-use, still experimental).
- --limittargets=<arg, -L<arg> >>>
-
If nonzero, it is the maximum number of targets that the
machine learner prints for further consideration. This can
be a useful speed-up when the number of targets is very high
(say 100000), but we only need a small number of them that
are very likely to be recommended within a much smaller initial
segment. Default is 0 - no limit. A useful limit is 1000.
- --boostlimit=<arg, -b<arg> >>>
-
If nonzero, the axioms in small specifications are slightly
boosted in learning by exp( -boostweight). A specification is
small, if it has less axioms than (boostlimit/100) * number-of-all-axioms.
Default is 0 (no boosting). A reasonable boosting default is 1,
i.e. with 70000 total axioms in all specs, axioms in those
with less than 700 will be boosted. The idea is that this will
help to focus in the much larger specifications, in the same way
as the info about proof helps.
- --boostweight=<arg, -w<arg> >>>
-
The weight used for boosting if boostlimit > 0. This
is negated and exponentiated to get the boost factor. The default
is 7 (so the boost factor is exp -7 = ca. 0.01), because this is
constraint by boostlimit anyway.
- --refsbgcheat=<arg, -r<arg> >>>
-
Tells to cheat by limiting background for problems
whose subproblems (specified in .refspec) are solved.
Useful for reproving. Default is 0 - no cheating.
- --alwaysmizrefs=<arg, -m<arg> >>>
-
If 1, tells to always include the explicit Mizar references. This
is useful for the bushy problems, where we are reasonably sure
that the explicit Mizar references should be used in the proof,
while we are uncertain about the background formulas.
The explicit references are now recongized by matching the regexp
``^[tldes][0-9]+'' (for theorems, top-level lemmas, definitions,
sublemmas, and scheme instances).
If 2, references containing Mizar local constants are always
included. These references are recognized by grepping
for ``\bc[0-9]+'' in the formula symbols.
- --tptpproofs, -z<arg >>>
-
If > 0, try to get the TPTP format of all found proofs. This
is now done by rerunning EP on the set of needed references found
by other provers. This is mainly used for CASC LTB*, where the
condition is a TPTP proof with adequate FOF->CNF documentation.
The default is 0.
- --help, -h >>
-
Print a brief help message and exit.
- --man >>
-
Print the manual page and exit.
Josef Urban: MaLARea: a Metasystem for Automated Reasoning in Large Theories.
Proceedings of the CADE-21 Workshop on
Empirically Successful Automated Reasoning in Large Theories
Bremen, Germany, 17th July 2007.
http://ftp.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-257/05_Urban.pdf .
Urban J., Sutcliffe G., Pudlak P., Vyskocil J. (2007),
MaLARea SG1: Machine Learner for Automated Reasoning with Semantic Guidance,
In Baumgartner P., Armando A., Gilles D.,
Proceedings of the 4th International Joint Conference on Automated Reasoning (Sydney, Australia),
Lecture Notes in Artificial Intelligence (To appear).
http://kti.mff.cuni.cz/~urban/MaLAReaSG1.pdf .
Josef Urban urban@kti.ms.mff.cuni.cz
This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.