DeepSeek Prover¶
"DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data" presents an approach to generate mathematical proofs for theorems generated from informal math problems. This approach shows promising results to advance the capabilities of models towards theorem proving using synthetic data. Until this moment the dataset and the model trained on top of it haven't been opened, let's see how the approach works to reproduce the pipeline using distilabel. The following figure depicts the approach taken to generate the dataset:
The authors propose a method for generating Lean 4 proof data from informal mathematical problems. Their approach translates high-school and undergraduate-level mathematical competition problems into formal statements.
Here we show how to deal with steps 1 and 2, but the authors ensure the theorems are checked using the lean4 program on the generated proofs, and iterate for a series of steps, fine-tuning a model on the synthetic data (DeepSeek prover 7B), regenerating the dataset, and continue the process until no further improvement is found.
Replication¶
Note
The section is named Replication but we will show how we can use distilabel to create the different steps outlined in the DeepSeek-Prover approach. We intentionally let some steps out of the pipeline, but this can easily be extended.
We will define the components needed to generate a dataset like the one depicted in the previous figure (we won't call lean4 or do the fine-tuning, this last step can be done outside of distilabel). The different blocks will have all the docstrings as we would have in the internal steps to showcase how they are done, but they can be omitted for brevity.
Installation¶
To reproduce the code below, we need to install distilabel as it follows:
We have decided to use InferenceEndpointsLLM, but any other provider with a strong model could work.
Building blocks¶
There are three components we needed to define for this pipeline, for the different components in the paper: A task to formalize the original statements, another one to assess the relevance of the theorems, and a final one to generate proofs for the theorems.
Note
We will use the same LLM for all the tasks, so we will define once and reuse it for the different tasks:
DeepSeekProverAutoFormalization¶
This Task corresponds to the first step in the figure. Given an informal statement, it will formalize it for us in Lean 4 language, meaning it will translate from an informal statement that could be gathered from the internet, to the lean4 structured language.
DeepSeekProverAutoFormalization
_PARSE_DEEPSEEK_PROVER_AUTOFORMAL_REGEX = r"```lean4(.*?)```"
template_deepseek_prover_auto_formalization = """\
Mathematical Problem in Natural Language:
{{ informal_statement }}
{%- if few_shot %}
Please use the following examples to guide you with the answer:
{%- for example in examples %}
- {{ example }}
{%- endfor %}
{% endif -%}"""
class DeepSeekProverAutoFormalization(Task):
examples: Optional[List[str]] = None
system_prompt: str = "Translate the problem to Lean 4 (only the core declaration):\n```lean4\nformal statement goes here\n```"
_template: Union[Template, None] = PrivateAttr(...)
_few_shot: bool = PrivateAttr(default=False)
def load(self) -> None:
super().load()
self._template = Template(template_deepseek_prover_auto_formalization)
@property
def inputs(self) -> List[str]:
return ["informal_statement"]
@property
def outputs(self):
return ["formal_statement", "model_name"]
def format_input(self, input: str) -> ChatType: # type: ignore
return [
{
"role": "system",
"content": self.system_prompt,
},
{
"role": "user",
"content": self._template.render(
informal_statement=input[self.inputs[0]],
few_shot=bool(self.examples),
examples=self.examples,
),
},
]
@override
def format_output( # type: ignore
self, output: Union[str, None], input: Dict[str, Any] = None
) -> Dict[str, Any]: # type: ignore
match = re.search(_PARSE_DEEPSEEK_PROVER_AUTOFORMAL_REGEX, output, re.DOTALL)
if match:
match = match.group(1).strip()
return {"formal_statement": match}
Following the paper, they found that the model yields better results if it uses examples in a few shot setting, so this class allows to take some examples to help in generating the formulation. Let's see an example of how we can instantiate it:
from textwrap import dedent
examples = [
dedent("""
## Statement in natural language:
For real numbers k and x:
If x is equal to (13 - √131) / 4, and
If the equation 2x² - 13x + k = 0 is satisfied,
Then k must be equal to 19/4.
## Formalized:
theorem mathd_algebra_116 (k x : ℝ) (h₀ : x = (13 - Real.sqrt 131) / 4)
(h₁ : 2 * x ^ 2 - 13 * x + k = 0) : k = 19 / 4 :="""),
dedent("""
## Statement in natural language:
The greatest common divisor (GCD) of 20 factorial (20!) and 200,000 is equal to 40,000.
## Formalized:
theorem mathd_algebra_116 (k x : ℝ) (h₀ : x = (13 - Real.sqrt 131) / 4)
(h₁ : 2 * x ^ 2 - 13 * x + k = 0) : k = 19 / 4 :="""),
dedent("""
## Statement in natural language:
Given two integers x and y:
If y is positive (greater than 0),
And y is less than x,
And the equation x + y + xy = 80 is true,
Then x must be equal to 26.
## Formalized:
theorem mathd_algebra_116 (k x : ℝ) (h₀ : x = (13 - Real.sqrt 131) / 4)
(h₁ : 2 * x ^ 2 - 13 * x + k = 0) : k = 19 / 4 :="""),
]
auto_formalization = DeepSeekProverAutoFormalization(
name="auto_formalization",
input_batch_size=8,
llm=llm,
examples=examples
)
DeepSeekProverScorer¶
The next Task corresponds to the second step, the model scoring and assessment. It uses an LLM as judge to evaluate the relevance of the theorem, and assigns a score so it can be filtered afterwards.
DeepSeekProverScorer
template_deepseek_prover_scorer = """\
To evaluate whether a formal Lean4 statement will be of interest to the community, consider the following criteria:
1. Relevance to Current Research: Does the statement address a problem or concept that is actively being researched in mathematics or related fields? Higher relevance scores indicate greater potential interest.
2. Complexity and Depth: Is the statement complex enough to challenge existing theories and methodologies, yet deep enough to provide significant insights or advancements? Complexity and depth showcase Lean4's capabilities and attract interest.
3. Interdisciplinary Potential: Does the statement offer opportunities for interdisciplinary research, connecting mathematics with other fields such as computer science, physics, or biology? Interdisciplinary projects often garner wide interest.
4. Community Needs and Gaps: Does the statement fill an identified need or gap within the Lean4 community or the broader mathematical community? Addressing these needs directly correlates with interest.
5. Innovativeness: How innovative is the statement? Does it propose new methods, concepts, or applications? Innovation drives interest and engagement.
Customize your evaluation for each problem accordingly, assessing it as 'excellent', 'good', 'above average', 'fair' or 'poor'.
You should respond in the following format for each statement:
'''
Natural language: (Detailed explanation of the informal statement, including any relevant background information, assumptions, and definitions.)
Analysis: (Provide a brief justification for each score, highlighting why the statement scored as it did across the criteria.)
Assessment: (Based on the criteria, rate the statement as 'excellent', 'good', 'above average', 'fair' or 'poor'. JUST the Assessment.)
'''"""
class DeepSeekProverScorer(Task):
_template: Union[Template, None] = PrivateAttr(...)
def load(self) -> None:
super().load()
self._template = Template(template_deepseek_prover_scorer)
@property
def inputs(self) -> List[str]:
return ["informal_statement", "formal_statement"]
@property
def outputs(self):
return ["natural_language", "analysis", "assessment", "model_name"]
def format_input(self, input: str) -> ChatType:
return [
{
"role": "system",
"content": self._template.render(),
},
{
"role": "user",
"content": f"## Informal statement:\n{input[self.inputs[0]]}\n\n ## Formal statement:\n{input[self.inputs[1]]}",
},
]
@override
def format_output(
self, output: Union[str, None], input: Dict[str, Any] = None
) -> Dict[str, Any]:
try:
result = output.split("Natural language:")[1].strip()
natural_language, analysis = result.split("Analysis:")
analysis, assessment = analysis.split("Assessment:")
natural_language = natural_language.strip()
analysis = analysis.strip()
assessment = assessment.strip()
except Exception:
natural_language = analysis = assessment = None
return {
"natural_language": natural_language,
"analysis": analysis,
"assessment": assessment
}
DeepSeekProverSolver¶
The last task is in charge of generating a proof for the theorems generated in the previous steps.
DeepSeekProverSolver
class DeepSeekProverSolver(Task):
system_prompt: str = (
"You are an expert in proving mathematical theorems formalized in lean4 language. "
"Your answers consist just in the proof to the theorem given, and nothing else."
)
@property
def inputs(self) -> List[str]:
return ["formal_statement"]
@property
def outputs(self):
return ["proof"]
def format_input(self, input: str) -> ChatType:
prompt = dedent("""
Give me a proof for the following theorem:
```lean4
{theorem}
```"""
)
return [
{
"role": "system",
"content": self.system_prompt,
},
{
"role": "user",
"content": prompt.format(theorem=input["formal_statement"]),
},
]
def format_output(
self, output: Union[str, None], input: Dict[str, Any] = None
) -> Dict[str, Any]:
import re
match = re.search(_PARSE_DEEPSEEK_PROVER_AUTOFORMAL_REGEX, output, re.DOTALL)
if match:
match = match.group(1).strip()
return {"proof": match}
Additionally, the original pipeline defined in the paper includes a step to check the final proofs using the lean 4 language that we have omitted for simplicity. The fine tuning can be done completely offline, and come back to the pipeline after each iteration/training run.
All the docstrings have been removed from the code blocks, but can be seen in the full pipeline.
Code¶
Lets's put the building blocks together to create the final pipeline with distilabel. For this example we have generated a sample dataset plaguss/informal-mathematical-statements-tiny of informal mathematical statements starting from casey-martin/multilingual-mathematical-autoformalization, but as the paper mentions, we can create formal statements and it's corresponding proofs starting from informal ones:
Click to see the full pipeline
deepseek_prover.py
# Copyright 2023-present, Argilla, Inc.
#
# Licensed under the Apache License, Version 2.0 (the "License");
# you may not use this file except in compliance with the License.
# You may obtain a copy of the License at
#
# http://www.apache.org/licenses/LICENSE-2.0
#
# Unless required by applicable law or agreed to in writing, software
# distributed under the License is distributed on an "AS IS" BASIS,
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
# See the License for the specific language governing permissions and
# limitations under the License.
import re
from pathlib import Path
from textwrap import dedent
from typing import Any, Dict, List, Optional, Union
from distilabel.llms import InferenceEndpointsLLM
from distilabel.pipeline import Pipeline
from distilabel.steps import LoadDataFromHub
from distilabel.steps.tasks.base import Task
from distilabel.steps.tasks.typing import ChatType
from jinja2 import Template
from pydantic import PrivateAttr
from typing_extensions import override
_PARSE_DEEPSEEK_PROVER_AUTOFORMAL_REGEX = r"```lean4(.*?)```"
template_deepseek_prover_auto_formalization = """\
Mathematical Problem in Natural Language:
{{ informal_statement }}
{%- if few_shot %}
Please use the following examples to guide you with the answer:
{%- for example in examples %}
- {{ example }}
{%- endfor %}
{% endif -%}"""
class DeepSeekProverAutoFormalization(Task):
"""Task to translate a mathematical problem from natural language to Lean 4.
Note:
A related dataset (MMA from the paper) can be found in Hugging Face:
[casey-martin/multilingual-mathematical-autoformalization](https://huggingface.co/datasets/casey-martin/multilingual-mathematical-autoformalization).
Input columns:
- informal_statement (`str`): The statement to be formalized using Lean 4.
Output columns:
- formal_statement (`str`): The formalized statement using Lean 4, to be analysed.
Categories:
- generation
References:
- [`DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data`](https://arxiv.org/abs/2405.14333).
- [`Lean 4`](https://github.com/leanprover/lean4).
Examples:
Formalize a mathematical problem from natural language to Lean 4:
```python
from distilabel.steps.tasks import DeepSeekProverAutoFormalization
from distilabel.llms.huggingface import InferenceEndpointsLLM
# Consider this as a placeholder for your actual LLM.
prover_autoformal = DeepSeekProverAutoFormalization(
llm=InferenceEndpointsLLM(
model_id="deepseek-ai/deepseek-math-7b-instruct",
tokenizer_id="deepseek-ai/deepseek-math-7b-instruct",
),
)
prover_autoformal.load()
result = next(
prover_autoformal.process(
[
{"informal_statement": "If a polynomial g is monic, then the root of g is integral over the ring R."},
]
)
)
# result
# [
# {
# 'informal_statement': 'If a polynomial g is monic, then the root of g is integral over the ring R.',
# 'formal_statement': 'theorem isIntegral_root (hg : g.Monic) : IsIntegral R (root g):=',
# 'distilabel_metadata': {
# 'raw_output_deep_seek_prover_auto_formalization_0': '```lean4\ntheorem isIntegral_root (hg : g.Monic) : IsIntegral R (root g):=\n```'
# },
# 'model_name': 'deepseek-prover'
# }
# ]
```
Use a few-shot setting to formalize a mathematical problem from natural language to Lean 4:
```python
from distilabel.steps.tasks import DeepSeekProverAutoFormalization
from distilabel.llms.huggingface import InferenceEndpointsLLM
# You can gain inspiration from the following examples to create your own few-shot examples:
# https://github.com/yangky11/miniF2F-lean4/blob/main/MiniF2F/Valid.lean
# Consider this as a placeholder for your actual LLM.
prover_autoformal = DeepSeekProverAutoFormalization(
llm=InferenceEndpointsLLM(
model_id="deepseek-ai/deepseek-math-7b-instruct",
tokenizer_id="deepseek-ai/deepseek-math-7b-instruct",
),
examples=[
"theorem amc12a_2019_p21 (z : ℂ) (h₀ : z = (1 + Complex.I) / Real.sqrt 2) :\n\n((∑ k : ℤ in Finset.Icc 1 12, z ^ k ^ 2) * (∑ k : ℤ in Finset.Icc 1 12, 1 / z ^ k ^ 2)) = 36 := by\n\nsorry",
"theorem amc12a_2015_p10 (x y : ℤ) (h₀ : 0 < y) (h₁ : y < x) (h₂ : x + y + x * y = 80) : x = 26 := by\n\nsorry"
]
)
prover_autoformal.load()
result = next(
prover_autoformal.process(
[
{"informal_statement": "If a polynomial g is monic, then the root of g is integral over the ring R."},
]
)
)
# result
# [
# {
# 'informal_statement': 'If a polynomial g is monic, then the root of g is integral over the ring R.',
# 'formal_statement': 'theorem isIntegral_root (hg : g.Monic) : IsIntegral R (root g):=',
# 'distilabel_metadata': {
# 'raw_output_deep_seek_prover_auto_formalization_0': '```lean4\ntheorem isIntegral_root (hg : g.Monic) : IsIntegral R (root g):=\n```'
# },
# 'model_name': 'deepseek-prover'
# }
# ]
```
"""
examples: Optional[List[str]] = None
system_prompt: str = "Translate the problem to Lean 4 (only the core declaration):\n```lean4\nformal statement goes here\n```"
_template: Union[Template, None] = PrivateAttr(...)
_few_shot: bool = PrivateAttr(default=False)
def load(self) -> None:
"""Loads the Jinja2 template."""
super().load()
self._template = Template(template_deepseek_prover_auto_formalization)
@property
def inputs(self) -> List[str]:
"""The input for the task is the `instruction`."""
return ["informal_statement"]
@property
def outputs(self):
"""The output for the task is a list of `instructions` containing the generated instructions."""
return ["formal_statement", "model_name"]
def format_input(self, input: str) -> ChatType: # type: ignore
"""The input is formatted as a `ChatType` assuming that the instruction
is the first interaction from the user within a conversation. And the
`system_prompt` is added as the first message if it exists."""
return [
{
"role": "system",
"content": self.system_prompt,
},
{
"role": "user",
"content": self._template.render(
informal_statement=input[self.inputs[0]],
few_shot=bool(self.examples),
examples=self.examples,
),
},
]
@override
def format_output( # type: ignore
self, output: Union[str, None], input: Dict[str, Any] = None
) -> Dict[str, Any]: # type: ignore
"""Extracts the formal statement from the Lean 4 output."""
match = re.search(_PARSE_DEEPSEEK_PROVER_AUTOFORMAL_REGEX, output, re.DOTALL)
if match:
match = match.group(1).strip()
return {"formal_statement": match}
template_deepseek_prover_scorer = """\
To evaluate whether a formal Lean4 statement will be of interest to the community, consider the following criteria:
1. Relevance to Current Research: Does the statement address a problem or concept that is actively being researched in mathematics or related fields? Higher relevance scores indicate greater potential interest.
2. Complexity and Depth: Is the statement complex enough to challenge existing theories and methodologies, yet deep enough to provide significant insights or advancements? Complexity and depth showcase Lean4's capabilities and attract interest.
3. Interdisciplinary Potential: Does the statement offer opportunities for interdisciplinary research, connecting mathematics with other fields such as computer science, physics, or biology? Interdisciplinary projects often garner wide interest.
4. Community Needs and Gaps: Does the statement fill an identified need or gap within the Lean4 community or the broader mathematical community? Addressing these needs directly correlates with interest.
5. Innovativeness: How innovative is the statement? Does it propose new methods, concepts, or applications? Innovation drives interest and engagement.
Customize your evaluation for each problem accordingly, assessing it as 'excellent', 'good', 'above average', 'fair' or 'poor'.
You should respond in the following format for each statement:
'''
Natural language: (Detailed explanation of the informal statement, including any relevant background information, assumptions, and definitions.)
Analysis: (Provide a brief justification for each score, highlighting why the statement scored as it did across the criteria.)
Assessment: (Based on the criteria, rate the statement as 'excellent', 'good', 'above average', 'fair' or 'poor'. JUST the Assessment.)
'''"""
class DeepSeekProverScorer(Task):
"""Task to evaluate the quality of a formalized mathematical problem in Lean 4,
inspired by the DeepSeek-Prover task for scoring.
Note:
A related dataset (MMA from the paper) can be found in Hugging Face:
[casey-martin/multilingual-mathematical-autoformalization](https://huggingface.co/datasets/casey-martin/multilingual-mathematical-autoformalization).
Input columns:
- informal_statement (`str`): The statement to be formalized using Lean 4.
- formal_statement (`str`): The formalized statement using Lean 4, to be analysed.
Output columns:
- natural_language (`str`): Explanation for the problem.
- analysis (`str`): Analysis of the different points defined in the prompt.
- assessment (`str`): Result of the assessment.
Categories:
- scorer
- quality
- response
References:
- [`DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data`](https://arxiv.org/abs/2405.14333).
- [`Lean 4`](https://github.com/leanprover/lean4).
Examples:
Analyse a formal statement in Lean 4:
```python
from distilabel.steps.tasks import DeepSeekProverScorer
from distilabel.llms.huggingface import InferenceEndpointsLLM
# Consider this as a placeholder for your actual LLM.
prover_scorer = DeepSeekProverAutoFormalization(
llm=InferenceEndpointsLLM(
model_id="deepseek-ai/deepseek-math-7b-instruct",
tokenizer_id="deepseek-ai/deepseek-math-7b-instruct",
),
)
prover_scorer.load()
result = next(
prover_scorer.process(
[
{"formal_statement": "theorem isIntegral_root (hg : g.Monic) : IsIntegral R (root g):="},
]
)
)
# result
# [
# {
# 'formal_statement': 'theorem isIntegral_root (hg : g.Monic) : IsIntegral R (root g):=',
# 'informal_statement': 'INFORMAL',
# 'analysis': 'ANALYSIS',
# 'assessment': 'ASSESSMENT',
# 'distilabel_metadata': {
# 'raw_output_deep_seek_prover_scorer_0': 'Natural language:\nINFORMAL\nAnalysis:\nANALYSIS\nAssessment:\nASSESSMENT'
# },
# 'model_name': 'deepseek-prover-scorer'
# }
# ]
```
"""
_template: Union[Template, None] = PrivateAttr(...)
def load(self) -> None:
"""Loads the Jinja2 template."""
super().load()
self._template = Template(template_deepseek_prover_scorer)
@property
def inputs(self) -> List[str]:
"""The input for the task is the `instruction`."""
return ["informal_statement", "formal_statement"]
@property
def outputs(self):
"""The output for the task is a list of `instructions` containing the generated instructions."""
return ["natural_language", "analysis", "assessment", "model_name"]
def format_input(self, input: str) -> ChatType: # type: ignore
"""The input is formatted as a `ChatType` assuming that the instruction
is the first interaction from the user within a conversation. And the
`system_prompt` is added as the first message if it exists."""
return [
{
"role": "system",
"content": self._template.render(),
},
{
"role": "user",
"content": f"## Informal statement:\n{input[self.inputs[0]]}\n\n ## Formal statement:\n{input[self.inputs[1]]}",
},
]
@override
def format_output( # type: ignore
self, output: Union[str, None], input: Dict[str, Any] = None
) -> Dict[str, Any]: # type: ignore
"""Analyses the formal statement with Lean 4 output and generates an assessment
and the corresponding informal assessment."""
try:
result = output.split("Natural language:")[1].strip()
natural_language, analysis = result.split("Analysis:")
analysis, assessment = analysis.split("Assessment:")
natural_language = natural_language.strip()
analysis = analysis.strip()
assessment = assessment.strip()
except Exception:
natural_language = analysis = assessment = None
return {
"natural_language": natural_language,
"analysis": analysis,
"assessment": assessment,
}
class DeepSeekProverSolver(Task):
"""Task to generate a proof for a formal statement (theorem) in lean4.
Input columns:
- formal_statement (`str`): The formalized statement using Lean 4.
Output columns:
- proof (`str`): The proof for the formal statement theorem.
Categories:
- scorer
- quality
- response
References:
- [`DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data`](https://arxiv.org/abs/2405.14333).
"""
system_prompt: str = (
"You are an expert in proving mathematical theorems formalized in lean4 language. "
"Your answers consist just in the proof to the theorem given, and nothing else."
)
@property
def inputs(self) -> List[str]:
"""The input for the task is the `formal_statement`."""
return ["formal_statement"]
@property
def outputs(self):
"""The output for the task is the proof for the formal statement theorem."""
return ["proof"]
def format_input(self, input: str) -> ChatType: # type: ignore
"""The input is formatted as a `ChatType`, with a system prompt to guide our model."""
prompt = dedent("""
Give me a proof for the following theorem:
```lean4
{theorem}
```""")
return [
{
"role": "system",
"content": self.system_prompt,
},
{
"role": "user",
"content": prompt.format(theorem=input["formal_statement"]),
},
]
def format_output( # type: ignore
self, output: Union[str, None], input: Dict[str, Any] = None
) -> Dict[str, Any]: # type: ignore
import re
match = re.search(_PARSE_DEEPSEEK_PROVER_AUTOFORMAL_REGEX, output, re.DOTALL)
if match:
match = match.group(1).strip()
return {"proof": match}
examples = [
dedent("""
## Statement in natural language:
For real numbers k and x:
If x is equal to (13 - √131) / 4, and
If the equation 2x² - 13x + k = 0 is satisfied,
Then k must be equal to 19/4.
## Formalized:
theorem mathd_algebra_116 (k x : ℝ) (h₀ : x = (13 - Real.sqrt 131) / 4)
(h₁ : 2 * x ^ 2 - 13 * x + k = 0) : k = 19 / 4 :="""),
dedent("""
## Statement in natural language:
The greatest common divisor (GCD) of 20 factorial (20!) and 200,000 is equal to 40,000.
## Formalized:
theorem mathd_algebra_116 (k x : ℝ) (h₀ : x = (13 - Real.sqrt 131) / 4)
(h₁ : 2 * x ^ 2 - 13 * x + k = 0) : k = 19 / 4 :="""),
dedent("""
## Statement in natural language:
Given two integers x and y:
If y is positive (greater than 0),
And y is less than x,
And the equation x + y + xy = 80 is true,
Then x must be equal to 26.
## Formalized:
theorem mathd_algebra_116 (k x : ℝ) (h₀ : x = (13 - Real.sqrt 131) / 4)
(h₁ : 2 * x ^ 2 - 13 * x + k = 0) : k = 19 / 4 :="""),
]
with Pipeline(name="test_deepseek_prover") as pipeline:
data_loader = LoadDataFromHub(
repo_id="plaguss/informal-mathematical-statements-tiny",
split="val",
batch_size=8,
)
llm = InferenceEndpointsLLM(
model_id="meta-llama/Meta-Llama-3-70B-Instruct",
)
auto_formalization = DeepSeekProverAutoFormalization(
name="auto_formalization", input_batch_size=8, llm=llm, examples=examples
)
prover_scorer = DeepSeekProverScorer(
name="prover_scorer",
input_batch_size=8,
llm=llm,
)
proof_generator = DeepSeekProverSolver(
name="proof_generator", input_batch_size=8, llm=llm
)
(data_loader >> auto_formalization >> prover_scorer >> proof_generator)
if __name__ == "__main__":
import argparse
parser = argparse.ArgumentParser()
parser.add_argument(
"-d",
"--dry-run",
action=argparse.BooleanOptionalAction,
help="Do a dry run for testing purposes.",
)
args = parser.parse_args()
pipeline_parameters = {
data_loader.name: {"split": "val"},
auto_formalization.name: {
"llm": {
"generation_kwargs": {
"temperature": 0.6,
"top_p": 0.9,
"max_new_tokens": 512,
}
}
},
prover_scorer.name: {
"llm": {
"generation_kwargs": {
"temperature": 0.6,
"top_p": 0.9,
"max_new_tokens": 512,
}
}
},
}
ds_name = "test_deepseek_prover"
if args.dry_run:
distiset = pipeline.dry_run(batch_size=1, parameters=pipeline_parameters)
distiset.save_to_disk(Path.home() / f"Downloads/{ds_name}")
import pprint
pprint.pprint(distiset["default"]["train"][0])
else:
distiset = pipeline.run(parameters=pipeline_parameters)
distiset.push_to_hub(ds_name, include_script=True)
The script can be run run for a dry run or not, depending on the argument (the pipeline will run without dry run by default), and will be pushed to the hub with the name your_username/test_deepseek_prover:
Final dataset: plaguss/test_deepseek_prover.