File size: 4,165 Bytes
f3ae860 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 | """
Ejemplos de uso del modelo Metamatemático NLE v7.0
====================================================
Requisitos:
pip install torch>=2.5.1 torch-geometric>=2.7.0 huggingface-hub>=0.31
Ejecutar:
python example.py
"""
from model import MetamaticoPredictor, ActorCriticNetwork, encode_query, encode_goal, empty_graph_data, ACTIONS
import torch
# ─── Ejemplo 1: Uso rápido con from_pretrained ────────────────────────────────
print("=" * 60)
print("Ejemplo 1 — Uso rápido")
print("=" * 60)
model = MetamaticoPredictor.from_pretrained()
result = model.predict("Prove that the square root of 2 is irrational")
print(f"Query : Prove that sqrt(2) is irrational")
print(f"Action : {result['action']}")
print(f"Confidence: {result['confidence']:.1%}")
print(f"Probs : {result['probabilities']}")
print()
# ─── Ejemplo 2: Predicciones en lote ─────────────────────────────────────────
print("=" * 60)
print("Ejemplo 2 — Predicciones en lote")
print("=" * 60)
queries = [
"Prove that there are infinitely many prime numbers",
"What is the definition of a category?",
"Compute the integral of e^x from 0 to 1",
"Is the group Z/6Z isomorphic to Z/2Z × Z/3Z?",
"What is 2 + 2?",
"Hello, who are you?",
"Formalize the first isomorphism theorem in Lean 4",
"Prove by induction that sum of first n naturals is n(n+1)/2",
]
results = model.predict_batch(queries)
print(f"{'Action':<12} {'Conf':>6} Query")
print("-" * 60)
for q, r in zip(queries, results):
print(f"{r['action']:<12} {r['confidence']:>5.0%} {q[:55]}")
print()
# ─── Ejemplo 3: Con goal Lean 4 ───────────────────────────────────────────────
print("=" * 60)
print("Ejemplo 3 — Con goal Lean 4")
print("=" * 60)
lean_queries = [
("Is this valid?", "⊢ ∀ n : ℕ, n + 0 = n"),
("How do I prove this?","⊢ ∀ a b : ℤ, a * b = b * a"),
("Lean goal check", "⊢ ∃ x : ℝ, x ^ 2 = 2"),
]
for query, goal in lean_queries:
r = model.predict(query, lean_goal=goal)
print(f"Query : {query}")
print(f"Goal : {goal}")
print(f"Action: {r['action']} (conf={r['confidence']:.1%})")
print()
# ─── Ejemplo 4: Uso directo con PyTorch ───────────────────────────────────────
print("=" * 60)
print("Ejemplo 4 — Forward pass directo con PyTorch")
print("=" * 60)
from huggingface_hub import hf_hub_download
weights_path = hf_hub_download(
repo_id="metamatematico/Metamatematico",
filename="neural_agent.pt"
)
net = ActorCriticNetwork()
net.load_state_dict(torch.load(weights_path, map_location="cpu", weights_only=True))
net.eval()
graph = empty_graph_data()
q_emb = encode_query("prove the fundamental theorem of algebra").unsqueeze(0)
goal_emb = encode_goal("⊢ ∀ p : Polynomial ℂ, p.degree ≥ 1 → ∃ z : ℂ, p.eval z = 0").unsqueeze(0)
with torch.no_grad():
logits, value = net(graph, q_emb, goal_emb=goal_emb)
probs = torch.softmax(logits, dim=-1)
print(f"Logits : {logits.squeeze().tolist()}")
print(f"Probs : {probs.squeeze().tolist()}")
print(f"Value : {value.item():.4f}")
print(f"Action : {ACTIONS[int(probs.argmax())]}")
print()
# ─── Ejemplo 5: Cargar best checkpoint ───────────────────────────────────────
print("=" * 60)
print("Ejemplo 5 — Cargar best.pt (mejor checkpoint supervisado)")
print("=" * 60)
best_path = hf_hub_download(
repo_id="metamatematico/Metamatematico",
filename="best.pt"
)
model_best = MetamaticoPredictor(best_path)
r = model_best.predict("Show that every finite group of prime order is cyclic")
print(f"Action: {r['action']} (conf={r['confidence']:.1%})")
|