How to get all premises in a random Lean repo?

[Some-random]

I'm working on translating natural language reasoning task into Lean code and solving it using theorem proving techniques (for examples, please check here). For this, I need a way to extract all premises from the file so I can select the relevant ones for reasoning tasks. I briefly looked over the code but it appears that a corpus.jsonl is required before any such selection of premises can occur.

Furthermore, I'm curious to know if the existing ReProver model can handle this task? Although the problem I've outlined might seem outside its current scope, it could potentially be solvable given that the required tactics are fairly straightforward - such as apply, exact, split, etc.

[yangky11]

For corpus.jsonl, you can look into the code for generating LeanDojo Benchmark. For the other question, maybe ReProver can be used, but I don't see a way to collect enough aligned data of natural language -> formal theorem.

[Some-random]

Thanks for guiding me to the demo. I've now sorted the issue of finding premises. Yet, I'm still wrestling with producing proofs for my natural language reasoning task. I'm using GPT4 to formalize natural language reasoning problems into Lean code and using ReProver to handle the theorem proving part.

For my example, I give premises in the form of axiom A1 : ∀ x, zumpus x → tumpus x and states in the form of ⊢ ¬brown polly to the model, and ReProver can pick the right premise axiom A4 : ∀ x, vumpus x → ¬ brown x, but tacgen model struggles to produce the correct tactics, which should be apply A4.

I'm unsure if I'm doing something wrong, or if the gap between math theorem training data and translated natural language reasoning training data is too wide for successful proofs. I would appreciate any suggestions!

[yangky11]

Can you show me a simple Python script of how you use the models?

[Some-random]

Thanks for the reply! The code is here, I basically copied the demo code from ReProver readme and used my example data. The premise selection result is correct, but I'm not getting the tactics I want (which is apply A4).

import torch
from typing import Union, List
from transformers import AutoTokenizer, T5EncoderModel
from transformers import AutoTokenizer, AutoModelForSeq2SeqLM


tokenizer = AutoTokenizer.from_pretrained("kaiyuy/leandojo-lean3-retriever-byt5-small")
model = T5EncoderModel.from_pretrained("kaiyuy/leandojo-lean3-retriever-byt5-small")

tokenizer_tacgen = AutoTokenizer.from_pretrained("kaiyuy/leandojo-lean3-retriever-tacgen-byt5-small")
model_tacgen = AutoModelForSeq2SeqLM.from_pretrained("kaiyuy/leandojo-lean3-retriever-tacgen-byt5-small")


state = "⊢ ¬brown polly"
premises = [
    "constant zumpus : obj → Prop",
    "constant tumpus : obj → Prop",
    "constant transparent : obj → Prop",
    "constant vumpus : obj → Prop",
    "constant brown : obj → Prop",
    "constant wumpus : obj → Prop",
    "constant wooden : obj → Prop",
    "constant jompus : obj → Prop",
    "constant floral : obj → Prop",
    "constant yumpus : obj → Prop",
    "constant mean : obj → Prop",
    "constant dumpus : obj → Prop",
    "constant rompus : obj → Prop",
    "constant spicy : obj → Prop",
    "constant impus : obj → Prop",
    "constant large : obj → Prop",
    "constant numpus : obj → Prop",
    "constant feisty : obj → Prop",
    "constant polly : obj",
    "axiom A1 : ∀ x, zumpus x → tumpus x",
    "axiom A2 : ∀ x, zumpus x → transparent x",
    "axiom A3 : ∀ x, vumpus x → zumpus x",
    "axiom A4 : ∀ x, vumpus x → ¬ brown x",
    "axiom A5 : ∀ x, wumpus x → vumpus x",
    "axiom A6 : ∀ x, wumpus x → wooden x",
    "axiom A7 : ∀ x, jompus x → wumpus x",
    "axiom A8 : ∀ x, jompus x → ¬ floral x",
    "axiom A9 : ∀ x, yumpus x → jompus x",
    "axiom A10 : ∀ x, yumpus x → mean x",
    "axiom A11 : ∀ x, dumpus x → yumpus x",
    "axiom A12 : ∀ x, rompus x → brown x",
    "axiom A13 : ∀ x, dumpus x → spicy x",
    "axiom A14 : ∀ x, impus x → dumpus x",
    "axiom A15 : ∀ x, impus x → large x",
    "axiom A16 : ∀ x, numpus x → impus x",
    "axiom A17 : ∀ x, numpus x → ¬ feisty x",
    "axiom A18 : vumpus polly"
]

@torch.no_grad()
def encode(s: Union[str, List[str]]) -> torch.Tensor:
    """Encode texts into feature vectors."""
    if isinstance(s, str):
        s = [s]
        should_squeeze = True
    else:
        should_squeeze = False
    tokenized_s = tokenizer(s, return_tensors="pt", padding=True)
    hidden_state = model(tokenized_s.input_ids).last_hidden_state
    lens = tokenized_s.attention_mask.sum(dim=1)
    features = (hidden_state * tokenized_s.attention_mask.unsqueeze(2)).sum(dim=1) / lens.unsqueeze(1)
    if should_squeeze:
      features = features.squeeze()
    return features

@torch.no_grad()
def retrieve(state: str, premises: List[str], k: int) -> List[str]:
    """Retrieve the top-k premises given a state."""
    state_emb = encode(state)
    premise_embs = encode(premises)
    scores = (state_emb @ premise_embs.T)
    topk = scores.topk(k).indices.tolist()
    return [premises[i] for i in topk]

print("Retrieved premises:")
ret = retrieve(state, premises, k=2)
for p in ret:
    print(p, end="\n")

input = "\n\n".join([ret[0]] + [state])
print("------ INPUT ------\n", input)
tokenized_input = tokenizer_tacgen(input, return_tensors="pt", max_length=2300, truncation=True)

# Generate multiple tactics via beam search.
tactic_candidates_ids = model_tacgen.generate(
    tokenized_input.input_ids,
    max_length=1024,
    num_beams=20,
    length_penalty=0.0,
    do_sample=False,
    num_return_sequences=20,
    early_stopping=False,
)
tactic_candidates = tokenizer_tacgen.batch_decode(
    tactic_candidates_ids, skip_special_tokens=True
)
print("\n------ Multiple OUTPUTS ------")
for tac in tactic_candidates:
    print(tac)

[yangky11]

The code seems correct, though the model may not perform very well since the data is quite different from its training data.