Gym/resources_servers/math_formal_lean/configs/nemotron_clean_easy.yaml at main · pthombre/Gym · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
math_formal_lean:
  resources_servers:
    math_formal_lean:
      entrypoint: app.py
      sandbox_host: ${oc.env:NEMO_SKILLS_SANDBOX_HOST,127.0.0.1}
      sandbox_port: ${oc.env:NEMO_SKILLS_SANDBOX_PORT,6000}
      compilation_timeout: 30.0
      domain: math
      verified: false
      description: Lean4 formal proof verification environment
      value: Improve formal theorem proving capabilities

math_formal_lean_simple_agent:
  responses_api_agents:
    simple_agent:
      entrypoint: app.py
      resources_server:
        type: resources_servers
        name: math_formal_lean
      model_server:
        type: responses_api_models
        name: policy_model
      datasets:
      - name: train
        type: train
        jsonl_fpath: resources_servers/math_formal_lean/data/nemotron_clean_easy.jsonl
        license: Apache 2.0