README.md

---
license: mit
---

# PVSGym: A Proof Learning Environment

https://www.manojacharya.com/pvsgym

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:

``` text
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:

``` text
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:
```

``` text
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:
```

``` text
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:
```

``` text
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:
```

``` text
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:
```

``` text
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:
```

``` text
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:

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

### Health Check

``` bash
curl http://localhost:8000/health
```

### Command Recommendation Endpoint

Example request:

``` bash
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/pvsgym