Buckets:
| import torch | |
| import torch.nn as nn | |
| import torch.nn.functional as F | |
| from typing import List, Dict, Tuple, Any, Optional | |
| class ProofStepPredictor(nn.Module): | |
| def __init__( | |
| self, problem_dim=512, step_vocab_size=100, hidden_dim=512, num_layers=3 | |
| ): | |
| super().__init__() | |
| self.step_vocab_size = step_vocab_size | |
| self.step_vocab = [ | |
| "apply_pythagorean", | |
| "apply_angle_sum", | |
| "apply_sas_similarity", | |
| "apply_inscribed_angle", | |
| "construct_perpendicular", | |
| "construct_parallel", | |
| "construct_circumcenter", | |
| "construct_incenter", | |
| "use_symmetry", | |
| "use_congruence", | |
| "use_similarity", | |
| "compute_area", | |
| "compute_angle", | |
| "identify_right_triangle", | |
| "identify_isosceles", | |
| "conclude_proof", | |
| ] | |
| self.state_encoder = nn.LSTM( | |
| problem_dim, hidden_dim, num_layers=num_layers, batch_first=True | |
| ) | |
| self.step_predictor = nn.Sequential( | |
| nn.Linear(hidden_dim, hidden_dim), | |
| nn.ReLU(), | |
| nn.Dropout(0.1), | |
| nn.Linear(hidden_dim, len(self.step_vocab)), | |
| ) | |
| self.confidence_scorer = nn.Sequential( | |
| nn.Linear(hidden_dim, 64), nn.ReLU(), nn.Linear(64, 1), nn.Sigmoid() | |
| ) | |
| def forward(self, problem_encoding, proof_history=None): | |
| batch_size = problem_encoding.size(0) | |
| if proof_history is None: | |
| input_seq = problem_encoding.unsqueeze(1) | |
| else: | |
| input_seq = torch.cat([problem_encoding.unsqueeze(1), proof_history], dim=1) | |
| output, (hidden, _) = self.state_encoder(input_seq) | |
| final_state = hidden[-1] | |
| step_logits = self.step_predictor(final_state) | |
| step_probs = F.softmax(step_logits, dim=-1) | |
| confidence = self.confidence_scorer(final_state) | |
| return { | |
| "step_logits": step_logits, | |
| "step_probs": step_probs, | |
| "confidence": confidence, | |
| "hidden_state": final_state, | |
| } | |
| def beam_search_proof(self, problem_encoding, max_steps=10, beam_width=3): | |
| beam = [(0.0, [], None)] | |
| for step in range(max_steps): | |
| candidates = [] | |
| for score, steps, hidden_state in beam: | |
| if steps: | |
| step_tensors = [] | |
| for step_name in steps: | |
| if step_name in self.step_vocab: | |
| step_idx = self.step_vocab.index(step_name) | |
| step_tensor = torch.zeros(1, len(self.step_vocab)) | |
| step_tensor[0, step_idx] = 1.0 | |
| step_tensors.append(step_tensor) | |
| if step_tensors: | |
| proof_history = torch.stack(step_tensors, dim=1) | |
| else: | |
| proof_history = None | |
| else: | |
| proof_history = None | |
| with torch.no_grad(): | |
| prediction = self.forward(problem_encoding, proof_history) | |
| step_probs = prediction["step_probs"][0] | |
| confidence = prediction["confidence"][0].item() | |
| top_k_probs, top_k_indices = torch.topk(step_probs, beam_width) | |
| for prob, idx in zip(top_k_probs, top_k_indices): | |
| step_name = self.step_vocab[idx.item()] | |
| new_score = score + torch.log(prob).item() * confidence | |
| new_steps = steps + [step_name] | |
| candidates.append((new_score, new_steps, None)) | |
| if step_name == "conclude_proof": | |
| return new_steps, new_score | |
| candidates.sort(key=lambda x: x[0], reverse=True) | |
| beam = candidates[:beam_width] | |
| if beam: | |
| return beam[0][1], beam[0][0] | |
| return [], float("-inf") | |
Xet Storage Details
- Size:
- 4.02 kB
- Xet hash:
- 3c5ae009e63a1a3c86ba02e2138d23f1d9f0be74af9d6e027697be296295dbbd
·
Xet efficiently stores files, intelligently splitting them into unique chunks and accelerating uploads and downloads. More info.