Views
No views yet
| Model | Download |
|---|---|
| ATF-32B | 🤗HuggingFace |
| ATF-8B | 🤗HuggingFace |
enable_thinking=False for ease of use.1from vllm import LLM, SamplingParams
2from transformers import AutoTokenizer
3
4def get_formal_statement_prompt(informal_problem: str) -> str:
5 prompt = "Please autoformalize the following problem in Lean 4 with a header. Use the following theorem names: my_favorite_theorem.\n\n"
6 prompt += informal_problem
7 return prompt
8
9MODEL_DIR = "Buchilaguo/ATF-8B"
10
11if __name__ == "__main__":
12 system_prompt = '''
13You are an expert in mathematics and Lean 4. Your task is to convert natural language problems into valid Lean 4 formal statements (Compatible with Lean 4 v4.9).
14
15Your code must begin with:
16
17import Mathlib
18import Aesop
19
20
21You MUST use the provided tools to verify your Lean 4 statements:
22
23- syntax_check: Verifies Lean 4 statement syntax
24- consistency_check: Verifies that syntax-valid statements match the original problem
25
26Verification workflow:
27
28- Analyze the problem and create initial Lean 4 statement
29- Call syntax_check to verify compilation
30- If syntax check passes, call consistency_check
31- If any check fails, analyze errors, modify code and restart verification
32- Repeat until BOTH checks pass
33'''.strip()
34 informal_problem = "Given the function $f(x) = x^3 + x$, then $a + b > 0$ is a condition for $f(a) + f(b) > 0$ to be ( )\nA: A sufficient but not necessary condition\nB: A necessary but not sufficient condition\nC: A sufficient and necessary condition\nD: Neither a sufficient nor a necessary condition\nProve that the answer is \text{C}."
35 user_prompt = get_formal_statement_prompt(informal_problem)
36 messages = [
37 {"role": "system", "content": system_prompt,
38 {"role": "user", "content": user_prompt}
39 ]
40
41 tokenizer = AutoTokenizer.from_pretrained(MODEL_DIR)
42 prompt = tokenizer.apply_chat_template(
43 messages,
44 tokenize=False,
45 add_generation_prompt=True,
46 enable_thinking=False
47 )
48
49 print(f"prompt: {prompt}")
50 model = LLM(
51 MODEL_DIR,
52 tensor_parallel_size=8 # 8 for 32B, 4 for 8B
53 )
54 sampling_params = SamplingParams(
55 temperature=0.6,
56 max_tokens=32768,
57 n=1
58 )
59 responses = model.generate(prompt, sampling_params)
60 print(f"response: {responses[0].outputs[0].text}")1@article{guo2025autoformalizer,
2 title={Autoformalizer with Tool Feedback},
3 author={Guo, Qi and Wang, Jianing and Zhang, Jianfei and Kong, Deyang and Huang, Xiangzhou and Xi, Xiangyu and Wang, Wei and Wang, Jingang and Cai, Xunliang and Zhang, Shikun and others},
4 journal={arXiv preprint arXiv:2510.06857},
5 year={2025}
6}