Buckets:
| import time | |
| from typing import List, Dict, Tuple, Any, Optional | |
| from ..core.geometry import OlympiadProblem | |
| from ..neural.prover import NeuralTheoremProver | |
| from ..core.knowledge import GeometricKnowledgeGraph | |
| from ..core.reasoning import TheoremDatabase | |
| from ..symbolic.coordinate import CoordinateGeometrySolver | |
| from ..symbolic.synthetic import SyntheticGeometrySolver | |
| from ..symbolic.verifier import ProofVerifier | |
| from .strategy import StrategySelector | |
| from .explanation import ExplanationGenerator | |
| class OlympiadGeometrySolver: | |
| def __init__(self): | |
| self.neural_prover = NeuralTheoremProver() | |
| self.knowledge_graph = GeometricKnowledgeGraph() | |
| self.theorem_db = TheoremDatabase() | |
| self.coordinate_solver = CoordinateGeometrySolver() | |
| self.synthetic_solver = SyntheticGeometrySolver() | |
| self.strategy_selector = StrategySelector() | |
| self.proof_verifier = ProofVerifier() | |
| self.explanation_generator = ExplanationGenerator() | |
| def solve_problem( | |
| self, problem: OlympiadProblem, timeout: int = 300 | |
| ) -> Dict[str, Any]: | |
| solution = { | |
| "problem": problem.name, | |
| "strategies_attempted": [], | |
| "proofs_found": [], | |
| "best_proof": None, | |
| "confidence": 0.0, | |
| "reasoning_trace": [], | |
| "time_taken": 0.0, | |
| } | |
| start_time = time.time() | |
| try: | |
| strategies = self.strategy_selector.select_strategies(problem) | |
| solution["strategies_attempted"] = strategies | |
| proof_candidates = [] | |
| for strategy in strategies: | |
| if time.time() - start_time > timeout: | |
| break | |
| solution["reasoning_trace"].append(f"Trying strategy: {strategy}") | |
| if strategy == "neural": | |
| proof = self._solve_with_neural(problem) | |
| elif strategy == "coordinate": | |
| proof = self._solve_with_coordinates(problem) | |
| elif strategy == "synthetic": | |
| proof = self._solve_with_synthetic(problem) | |
| elif strategy == "hybrid": | |
| proof = self._solve_with_hybrid(problem) | |
| else: | |
| continue | |
| if proof["success"]: | |
| proof_candidates.append(proof) | |
| solution["proofs_found"].append(proof) | |
| solution["reasoning_trace"].append( | |
| f"Success with {strategy} strategy" | |
| ) | |
| if proof_candidates: | |
| best_proof = self._select_best_proof(proof_candidates) | |
| solution["best_proof"] = best_proof | |
| solution["confidence"] = best_proof["confidence"] | |
| explanation = self.explanation_generator.generate(best_proof, problem) | |
| solution["explanation"] = explanation | |
| solution["time_taken"] = time.time() - start_time | |
| except Exception as e: | |
| solution["error"] = str(e) | |
| solution["time_taken"] = time.time() - start_time | |
| return solution | |
| def _solve_with_neural(self, problem: OlympiadProblem) -> Dict[str, Any]: | |
| try: | |
| object_types = ( | |
| list(problem.points.keys()) | |
| + list(problem.lines.keys()) | |
| + list(problem.circles.keys()) | |
| ) | |
| result = self.neural_prover.solve_problem( | |
| problem.statement, object_types[:5] | |
| ) | |
| return { | |
| "strategy": "neural", | |
| "success": result["is_valid"], | |
| "steps": result["proof_steps"], | |
| "confidence": 0.8 if result["is_valid"] else 0.2, | |
| "theorems_used": [t[0] for t in result["relevant_theorems"]], | |
| "score": result["proof_score"], | |
| } | |
| except Exception as e: | |
| return {"strategy": "neural", "success": False, "error": str(e)} | |
| def _solve_with_coordinates(self, problem: OlympiadProblem) -> Dict[str, Any]: | |
| try: | |
| return self.coordinate_solver.solve(problem) | |
| except Exception as e: | |
| return {"strategy": "coordinate", "success": False, "error": str(e)} | |
| def _solve_with_synthetic(self, problem: OlympiadProblem) -> Dict[str, Any]: | |
| try: | |
| return self.synthetic_solver.solve(problem) | |
| except Exception as e: | |
| return {"strategy": "synthetic", "success": False, "error": str(e)} | |
| def _solve_with_hybrid(self, problem: OlympiadProblem) -> Dict[str, Any]: | |
| try: | |
| neural_result = self._solve_with_neural(problem) | |
| if neural_result["success"]: | |
| verified = self.proof_verifier.verify_proof( | |
| neural_result["steps"], problem | |
| ) | |
| return { | |
| "strategy": "hybrid", | |
| "success": verified, | |
| "steps": neural_result["steps"], | |
| "confidence": 0.9 if verified else 0.3, | |
| "verification_result": verified, | |
| } | |
| return {"strategy": "hybrid", "success": False} | |
| except Exception as e: | |
| return {"strategy": "hybrid", "success": False, "error": str(e)} | |
| def _select_best_proof(self, proof_candidates: List[Dict]) -> Dict[str, Any]: | |
| scored_proofs = [] | |
| for proof in proof_candidates: | |
| score = 0.0 | |
| score += proof.get("confidence", 0) * 0.4 | |
| steps = proof.get("steps", []) | |
| length_penalty = min(len(steps) / 20.0, 1.0) | |
| score += (1.0 - length_penalty) * 0.2 | |
| strategy_bonus = { | |
| "hybrid": 0.3, | |
| "neural": 0.2, | |
| "coordinate": 0.15, | |
| "synthetic": 0.15, | |
| } | |
| score += strategy_bonus.get(proof.get("strategy"), 0.1) | |
| if proof.get("verification_result", False): | |
| score += 0.1 | |
| scored_proofs.append((score, proof)) | |
| scored_proofs.sort(key=lambda x: x[0], reverse=True) | |
| return scored_proofs[0][1] if scored_proofs else None | |
Xet Storage Details
- Size:
- 6.22 kB
- Xet hash:
- 167e6a2a6c77a3758004a969f3fef1d27ce1020b3d7a7d9fab22db247a304758
·
Xet efficiently stores files, intelligently splitting them into unique chunks and accelerating uploads and downloads. More info.