| """ |
| example_usage.py - Test local or remote nanoGentzen pipeline |
| """ |
| import torch |
| from transformers import AutoModel, AutoTokenizer |
| from kernel import Sequent, Imp, And, Var, verify_proof_tree |
| from search import NeuralProofSearch |
|
|
| device = "cuda" if torch.cuda.is_available() else "cpu" |
|
|
| print("[*] Loading nanoGentzen model & tokenizer...") |
| model = AutoModel.from_pretrained("./hf_model", trust_remote_code=True).to(device) |
| tokenizer = AutoTokenizer.from_pretrained("./hf_model", trust_remote_code=True) |
|
|
| searcher = NeuralProofSearch(model, tokenizer, device=device) |
|
|
| |
| P, Q = Var("P"), Var("Q") |
| goal = Sequent((P, Imp(P, Q)), (Q,)) |
|
|
| print(f"[*] Proving goal: {goal.to_str()}") |
| proof_tree = searcher.prove(goal, max_depth=8) |
|
|
| if proof_tree: |
| print("[✓] PROOF FOUND & VERIFIED:") |
| print(f" Sound: {verify_proof_tree(proof_tree)}") |
| print(f" Tree : {proof_tree}") |
| else: |
| print("[✗] Proof failed or timed out.") |
|
|
