Update README.md

README.md

@@ -4,12 +4,18 @@ license: mit
 
 # PVSGym: A Proof Learning Environment
 
-Paper link: https://openreview.net/forum?id=NpytqGYVPa&noteId=NpytqGYVPa
+Paper: https://openreview.net/forum?id=NpytqGYVPa&noteId=NpytqGYVPa
 
-This repo contains models and web server that uses LLMs to assist theorem proving in PVS.
+This repository contains models and a web server that use LLMs to assist
+theorem proving in PVS.
 
-Put all model files that follows this tree:
-```
+------------------------------------------------------------------------
+
+## Model Files
+
+Place all model files in a directory that follows this structure:
+
+``` text
 pvs_sft5
 ├── config.json
 ├── generation_config.json
@@ -25,11 +31,17 @@ pvs_sft5
 └── training_args.bin
 ```
 
-## Input examples ( Model is sensitive to newlines formatting):
-(Implementaion details ( recommend function) here https://huggingface.co/ma7583/pvs_oracle/blob/main/sft_fastapi.py )
+------------------------------------------------------------------------
 
+## 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
+
+Each query to the recommender should be formatted like this:
+
+``` text
 Current Sequent:
 [1]   norm((# x := -1, y := 0 #)) = 1
 
@@ -39,7 +51,7 @@ 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)
 
@@ -47,10 +59,9 @@ 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)
@@ -63,10 +74,9 @@ 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)
 
@@ -74,24 +84,21 @@ 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)
@@ -100,33 +107,41 @@ Prev Command 1: (EXPAND "empty?")
 Prev Command 2: (EXPAND "member")
 Prev Command 3: (GROUND)
 Next Command:
-
 ```
 
+------------------------------------------------------------------------
 
+## Running the Web Server
 
-## Start the web server with the model running
+Start the FastAPI server with:
 
-```python -m uvicorn sft_fastapi:app --host 0.0.0.0 --port 8000```
+``` bash
+python -m uvicorn sft_fastapi:app --host 0.0.0.0 --port 8000
+```
 
-## Send requests to the server
+### Health Check
 
-`curl http://localhost:8000/health` --> to check server health
+``` bash
+curl http://localhost:8000/health
+```
 
+### Command Recommendation Endpoint
 
-```
-curl -X POST http://localhost:8000/recommend \
-  -H "Content-Type: application/json" \
-  -d '{
+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 stricly required to run this but we will later add a demo that uses both. 
+PVSGym is not strictly required to run this server, but a joint demo
+will be added later.
 
-PVSgym repo: https://github.com/manoja328/expmath/tree/main/pvspy
+Repository: https://github.com/manoja328/expmath/tree/main/pvspy