Views
No views yet
1pvs_sft5
2├── config.json
3├── generation_config.json
4├── model-00001-of-00003.safetensors
5├── model-00002-of-00003.safetensors
6├── model-00003-of-00003.safetensors
7├── model.safetensors.index.json
8├── recommended_commands.csv
9├── special_tokens_map.json
10├── tokenizer_config.json
11├── tokenizer.json
12├── tokenizer.model
13└── training_args.binImportant: The model is sensitive to newline formatting.
For reference, see therecommendimplementation here:
https://huggingface.co/ma7583/pvs_oracle/blob/main/sft_fastapi.py Note: The history requires three previous commands or "None" to denote empty.
1Current Sequent:
2[1] norm((# x := -1, y := 0 #)) = 1
3
4Prev Command 1: (EXPAND "point_on_polygon_perimeter?")
5Prev Command 2: (INST + "s")
6Prev Command 3: (HIDE-ALL-BUT 1)
7Next Command:1Current Sequent:
2{1} expt(c, (3 + 4 * n)) = expt(c, (1 + 4 * n)) * expt(c, 2)
3
4Prev Command 1: (PROPAX)
5Prev Command 2: (HIDE 2)
6Prev Command 3: (EXPAND "^")
7Next Command:1Current Sequent:
2[-1] derivable?(sin, x!1) AND derivable?(sin, x!1) IMPLIES deriv(sin * sin, x!1) = 2 * (deriv(sin, x!1) * sin(x!1))
3[-2] derivable?[real](sin * sin, x!1)
4[-3] derivable?[real](cos * cos, x!1)
5[-4] FORALL (x: real): derivable?[real](sin, x)
6{-5} FORALL (x: real): derivable?[real](cos, x)
7[1] deriv(cos * cos, x!1) + deriv(sin * sin, x!1) = const_fun(0)(x!1)
8
9Prev Command 1: (ASSERT)
10Prev Command 2: (EXPAND "derivable?" -4)
11Prev Command 3: (EXPAND "derivable?" -5)
12Next Command:1Current Sequent:
2[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)
3
4Prev Command 1: (ASSERT)
5Prev Command 2: (ASSERT)
6Prev Command 3: (HIDE 2)
7Next Command:1Current Sequent:
2{-1} FORALL (a: {x: real | 0 < x AND x <= pi / 2}): sin(a) > 0
3[-2] a <= pi / 2
4[1] sin(a) > 0
5
6Prev Command 1: (SKEEP)
7Prev Command 2: (CASE "a <= pi/2")
8Prev Command 3: (LEMMA "sin_pos_0tohalfpi")
9Next Command:1Current Sequent:
2{-1} FORALL (x_1: real): NOT (key_arb_intersections(p, v, G)(x_1) OR parallel_intersections(p, v, G)(x_1))
3{1} FORALL (x: real): NOT key_arb_intersections(p, v, G)(x)
4
5Prev Command 1: (EXPAND "empty?")
6Prev Command 2: (EXPAND "member")
7Prev Command 3: (GROUND)
8Next Command:1Current Sequent:
2{-1} FORALL (x_1: real): NOT (key_arb_intersections(p, v, G)(x_1) OR parallel_intersections(p, v, G)(x_1))
3{1} FORALL (x: real): NOT key_arb_intersections(p, v, G)(x)
4
5Prev Command 1: None
6Prev Command 2: None
7Prev Command 3: (GROUND)
8Next Command:python -m uvicorn sft_fastapi:app --host 0.0.0.0 --port 8000curl http://localhost:8000/health1curl -X POST http://localhost:8000/recommend -H "Content-Type: application/json" -d '{
2 "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)",
3 "prev_commands": ["None", "None", "None"],
4 "top_k": 3
5 }'