currently we report the posterior probability of the solution, and the prior probability of each axiom
we should report the posterior of each axiom. We do this by taking the sum of all solutions that include that axiom, and dividing that by the sum of probabilities of solutions that have a different interpretation.
If not all solutions are explored this will be an estimate. The estimate will be biased in favor of those with higher probabilities, as lower priorities may never be explored. We can account for this with a prior probability that the solution is biased
Pr(Axiom) = IsBiasedPrior * AxiomPrior + (1-IsBiasedPrior) * AxiomEstimatedPosterior
We can estimate IsBiasedPrior based on how many times the axiom or its alternatives were explored in the overall search tree.
We can also have strategies to minimize bias. E.g for each potential axiom we start at least one search with that as our initial choice.
currently we report the posterior probability of the solution, and the prior probability of each axiom
we should report the posterior of each axiom. We do this by taking the sum of all solutions that include that axiom, and dividing that by the sum of probabilities of solutions that have a different interpretation.
If not all solutions are explored this will be an estimate. The estimate will be biased in favor of those with higher probabilities, as lower priorities may never be explored. We can account for this with a prior probability that the solution is biased
Pr(Axiom) = IsBiasedPrior * AxiomPrior + (1-IsBiasedPrior) * AxiomEstimatedPosteriorWe can estimate IsBiasedPrior based on how many times the axiom or its alternatives were explored in the overall search tree.
We can also have strategies to minimize bias. E.g for each potential axiom we start at least one search with that as our initial choice.