ma7583/pvs_oracle

PVSGym: A Proof Learning Environment

Paper: https://openreview.net/forum?id=NpytqGYVPa&noteId=NpytqGYVPa

This repository contains models and a web server that use LLMs to assist theorem proving in PVS.

---

Model Files

Place all model files in a directory that follows this structure:

pvs_sft5
├── config.json
├── generation_config.json
├── model-00001-of-00003.safetensors
├── model-00002-of-00003.safetensors
├── model-00003-of-00003.safetensors
├── model.safetensors.index.json
├── recommended_commands.csv
├── special_tokens_map.json
├── tokenizer_config.json
├── tokenizer.json
├── tokenizer.model
└── training_args.bin

---

Input Format

Important: The model is sensitive to newline formatting.
For reference, see the recommend implementation here:
https://huggingface.co/ma7583/pvs_oracle/blob/main/sft_fastapi.py Note: The history requires three previous commands or "None" to denote empty.

Each query to the recommender should be formatted like this:

Current Sequent:
[1]   norm((# x := -1, y := 0 #)) = 1

Prev Command 1: (EXPAND "point_on_polygon_perimeter?")
Prev Command 2: (INST + "s")
Prev Command 3: (HIDE-ALL-BUT 1)
Next Command:

Current Sequent:
{1}   expt(c, (3 + 4 * n)) = expt(c, (1 + 4 * n)) * expt(c, 2)

Prev Command 1: (PROPAX)
Prev Command 2: (HIDE 2)
Prev Command 3: (EXPAND "^")
Next Command:

Current Sequent:
[-1]  derivable?(sin, x!1) AND derivable?(sin, x!1) IMPLIES deriv(sin * sin, x!1) = 2 * (deriv(sin, x!1) * sin(x!1))
[-2]  derivable?[real](sin * sin, x!1)
[-3]  derivable?[real](cos * cos, x!1)
[-4]  FORALL (x: real): derivable?[real](sin, x)
{-5}  FORALL (x: real): derivable?[real](cos, x)
[1]   deriv(cos * cos, x!1) + deriv(sin * sin, x!1) = const_fun(0)(x!1)

Prev Command 1: (ASSERT)
Prev Command 2: (EXPAND "derivable?" -4)
Prev Command 3: (EXPAND "derivable?" -5)
Next Command:

Current Sequent:
[1]   FORALL (x: real): LET S = LAMBDA (n: nat): powerseq(cos_coef, x)(2 * n) IN conv_series?(S) AND cos(x) = inf_sum(S)

Prev Command 1: (ASSERT)
Prev Command 2: (ASSERT)
Prev Command 3: (HIDE 2)
Next Command:

Current Sequent:
{-1}  FORALL (a: {x: real | 0 < x AND x <= pi / 2}): sin(a) > 0
[-2]  a <= pi / 2
[1]   sin(a) > 0

Prev Command 1: (SKEEP)
Prev Command 2: (CASE "a <= pi/2")
Prev Command 3: (LEMMA "sin_pos_0tohalfpi")
Next Command:

Current Sequent:
{-1}  FORALL (x_1: real): NOT (key_arb_intersections(p, v, G)(x_1) OR parallel_intersections(p, v, G)(x_1))
{1}   FORALL (x: real): NOT key_arb_intersections(p, v, G)(x)

Prev Command 1: (EXPAND "empty?")
Prev Command 2: (EXPAND "member")
Prev Command 3: (GROUND)
Next Command:

Current Sequent:
{-1}  FORALL (x_1: real): NOT (key_arb_intersections(p, v, G)(x_1) OR parallel_intersections(p, v, G)(x_1))
{1}   FORALL (x: real): NOT key_arb_intersections(p, v, G)(x)

Prev Command 1: None
Prev Command 2: None
Prev Command 3: (GROUND)
Next Command:

---

Running the Web Server

Start the FastAPI server with:

python -m uvicorn sft_fastapi:app --host 0.0.0.0 --port 8000

Health Check

curl http://localhost:8000/health

Command Recommendation Endpoint

Example request:

curl -X POST http://localhost:8000/recommend   -H "Content-Type: application/json"   -d '{
    "sequent": "{1}   FORALL (A, B: simple_polygon_2d, j: below(A`num_vertices), i: nat): LET IV = injected_vertices(A, B, A`num_vertices), s = edges_of_polygon(A)(j), L = injected_vertices(A, B, j)`length, Q = injected_edge_seq(s, injected_edge(s, B)) IN i < IV`length AND i >= L AND i < Q`length + L IMPLIES IV`seq(i) = Q`seq(i - L)",
    "prev_commands": ["None", "None", "None"],
    "top_k": 3
  }'

---

PVSgym

PVSGym is not strictly required to run this server, but a joint demo will be added later.

Repository: https://github.com/manoja328/expmath/tree/main/pvspy