On optimal heuristic randomized semidecision procedures, with application to proof complexity