Python API Specification

This page documents the htps module, which is implemented as a CPython extension in C++ (from htps.cpp).

HyperTreeProofSearch

class htps.Context

Bases: object

The underlying context for HyperTreeProofSearch

namespaces: Namespaces set

class htps.EnvEffect

Bases: object

A single EnvEffect, i.e. a tactic applied on a goal, for HyperTreeProofSearch

children: Children theorems

goal: Goal theorem

tactic: Tactic

class htps.EnvExpansion

Bases: object

A full EnvExpansion for HyperTreeProofSearch

children_for_tactic: Children for each tactic

effects: EnvEffects

env_durations: Environment durations

error: Error string (optional)

expander_duration: Expander duration

from_json_str(): Create from JSON string

generation_duration: Generation duration

get_json_str(): Get JSON string representation

is_error: Returns True if error is set

log_critic: Log critic value

priors: Priors

tactics: Tactics

thm: Theorem for expansion

class htps.HTPS

Bases: object

The HyperTreeProofSearch

expand_and_backup(): Expands and backups using the provided list of EnvExpansion objects

expansions: Number of expansions

from_json_str(): Creates a HTPS object from a JSON string

get_json_str(): Returns a JSON string representation of the HTPS object

get_result(): Returns the result of the HTPS run

is_done(): Whether the HTPS run is done or not

is_expanding(): Whether the HTPS run is still awaiting EnvExpansions or not (in which case new theorems can be requested)

proven(): Whether the start theorem is proven or not

theorems_to_expand(): Returns a list of subsequent theorems to expand

class htps.Hypothesis

Bases: object

A single hypothesis for HyperTreeProofSearch

identifier: Identifier for a hypothesis

value: Type of the hypothesis

class htps.InProof(value)

Bases: Enum

An enumeration.

InMinimalProof = 2

InProof = 1

NotInProof = 0

class htps.Metric(value)

Bases: Enum

An enumeration.

Depth = 0

Size = 1

Time = 2

class htps.NodeMask(value)

Bases: Enum

An enumeration.

MinimalProof = 3

MinimalProofSolving = 4

NoMask = 0

Proof = 2

Solving = 1

class htps.PolicyType(value)

Bases: Enum

An enumeration.

AlphaZero = 0

RPO = 1

class htps.Proof

Bases: object

Proof object, holding a proof subtree

children: Child proof objects

tactic: Tactic used in the proof

theorem: Theorem used in the proof

class htps.QValueSolved(value)

Bases: Enum

An enumeration.

CountOverCounts = 1

CountOverCountsNoFPU = 5

One = 2

OneOverCounts = 0

OneOverCountsNoFPU = 4

OneOverVirtualCounts = 3

class htps.Result

Bases: object

Result for a full HTPS run

critic_samples: Critic samples

effect_samples: Effect samples

goal: Goal theorem

metric: Metric

proof: Proof

proof_samples_tactics: Proof samples

tactic_samples: Tactic samples

class htps.SampleCritic

Bases: object

SampleCritic object, holding critic training samples

bad: Bad

critic: Critic value

goal: Goal theorem

q_estimate: Q estimate

solved: Solved

visit_count: Visit count

class htps.SampleEffect

Bases: object

SampleEffect object, holding effect training samples

children: Children theorems

goal: Goal theorem

tactic: Tactic

class htps.SampleTactics

Bases: object

SampleTactics object, holding tactic generation training samples

goal: theorem that was used to generate new tactics

inproof: InProof enum

q_estimates: q estimates

tactics: List of tactics

target_pi: Target probabilities

visit_count: Visit count

class htps.SearchParams

Bases: object

Parameters for HyperTreeProofSearch

backup_once: backup once flag

backup_one_for_solved: backup one for solved flag

count_threshold: count threshold

critic_subsampling_rate: critic subsampling rate

depth_penalty: depth penalty

early_stopping: early stopping flag

early_stopping_solved_if_root_not_proven: early stopping solved flag

effect_subsampling_rate: effect subsampling rate

exploration: exploration parameter

metric: Metric enum

no_critic: no critic flag

node_mask: NodeMask enum

num_expansions: max number of expansions

only_learn_best_tactics: only learn best tactics flag

policy_temperature: policy temperature

policy_type: PolicyType enum

q_value_solved: QValueSolved enum

succ_expansions: expansions per batch

tactic_init_value: tactic initial value

tactic_p_threshold: tactic p threshold flag

tactic_sample_q_conditioning: tactic sample q conditioning flag

virtual_loss: virtual loss

class htps.Tactic

Bases: object

A single tactic for HyperTreeProofSearch

duration: Duration of tactic in the environment

is_valid: Whether the tactic is valid or not

unique_string: Unique identifier for a tactic

class htps.Theorem

Bases: object

A single theorem for HyperTreeProofSearch

conclusion: Conclusion of the theorem

context: Context of the theorem

hypotheses: Hypotheses of theorem

metadata: Metadata dictionary

past_tactics: Past tactics of theorem

unique_string: Unique string of the theorem

exception htps.error: Bases: Exception