Career at Pramaana
Career at Pramaana
Research Engineer, Formal Methods
Location
Location
San Jose, California
San Jose, California
Employment Type
Employment Type
Full Time
Full Time
Location Type
Location Type
Onsite
Onsite
Department
Department
Technology
Technology
Location Type
Onsite
Department
Technology
Overview
Application
About Pramaana
Pramaana is on a mission to define the gold standard for verification. We are building the future of trustworthy AI by moving beyond probabilistic models to deterministic systems. Our core focus is on formal verification and proof-based reasoning, enabling us to mathematically validate the correctness of AI-generated information. We are solving the "trust" problem in AI for high-stakes environments where accuracy is non-negotiable.
About the Role
This role lies at the heart of Pramaana’s technical strategy: bridging the gap between the probabilistic nature of Large Language Models (LLMs) and the deterministic guarantees of formal logic. As a Research Engineer in Formal Methods, you will pioneer neuro-symbolic architectures that allow AI systems to reason with mathematical certainty. Your work will directly enable our platform to guarantee correctness in high-stakes domains, translating unstructured natural language into machine-checkable specifications.
Key Responsibilities
Research and implement methods to convert natural language statements into formal specifications and proofs using Lean, Coq, or Isabelle.
Develop techniques to guide LLM generation using formal proof assistants, tree-search algorithms, and tactic prediction.
Build automated reasoning engines to validate the logical consistency of AI-generated chains of thought using formal solvers.
Curate formal knowledge libraries and axioms like Lean Mathlib required to verify real-world claims across domains.
Design rigorous benchmarks to measure the soundness and completeness of our verification pipeline.
Contribute to the development of the company’s research strategy in artificial intelligence, formal verification, and proof-based reasoning.
Qualifications
Education: PhD or Master’s in Computer Science, Mathematics, Logic, or related field.
Formal Methods: Proficiency in Interactive Theorem Prover (ITP) such as Lean 4.
Engineering: Strong coding skills in Python and functional languages (OCaml, etc.).
AI Fundamentals: Solid understanding of Transformer architectures, LLMs, and neuro-symbolic reasoning.
Preferred: Expert knowledge of Lean 4 or experience with SMT solvers.
Overview
Application
About Pramaana
Pramaana is on a mission to define the gold standard for verification. We are building the future of trustworthy AI by moving beyond probabilistic models to deterministic systems. Our core focus is on formal verification and proof-based reasoning, enabling us to mathematically validate the correctness of AI-generated information. We are solving the "trust" problem in AI for high-stakes environments where accuracy is non-negotiable.
About the Role
This role lies at the heart of Pramaana’s technical strategy: bridging the gap between the probabilistic nature of Large Language Models (LLMs) and the deterministic guarantees of formal logic. As a Research Engineer in Formal Methods, you will pioneer neuro-symbolic architectures that allow AI systems to reason with mathematical certainty. Your work will directly enable our platform to guarantee correctness in high-stakes domains, translating unstructured natural language into machine-checkable specifications.
Key Responsibilities
Research and implement methods to convert natural language statements into formal specifications and proofs using Lean, Coq, or Isabelle.
Develop techniques to guide LLM generation using formal proof assistants, tree-search algorithms, and tactic prediction.
Build automated reasoning engines to validate the logical consistency of AI-generated chains of thought using formal solvers.
Curate formal knowledge libraries and axioms like Lean Mathlib required to verify real-world claims across domains.
Design rigorous benchmarks to measure the soundness and completeness of our verification pipeline.
Contribute to the development of the company’s research strategy in artificial intelligence, formal verification, and proof-based reasoning.
Qualifications
Education: PhD or Master’s in Computer Science, Mathematics, Logic, or related field.
Formal Methods: Proficiency in Interactive Theorem Prover (ITP) such as Lean 4.
Engineering: Strong coding skills in Python and functional languages (OCaml, etc.).
AI Fundamentals: Solid understanding of Transformer architectures, LLMs, and neuro-symbolic reasoning.
Preferred: Expert knowledge of Lean 4 or experience with SMT solvers.
Overview
Application
About Pramaana
Pramaana is on a mission to define the gold standard for verification. We are building the future of trustworthy AI by moving beyond probabilistic models to deterministic systems. Our core focus is on formal verification and proof-based reasoning, enabling us to mathematically validate the correctness of AI-generated information. We are solving the "trust" problem in AI for high-stakes environments where accuracy is non-negotiable.
About the Role
This role lies at the heart of Pramaana’s technical strategy: bridging the gap between the probabilistic nature of Large Language Models (LLMs) and the deterministic guarantees of formal logic. As a Research Engineer in Formal Methods, you will pioneer neuro-symbolic architectures that allow AI systems to reason with mathematical certainty. Your work will directly enable our platform to guarantee correctness in high-stakes domains, translating unstructured natural language into machine-checkable specifications.
Key Responsibilities
Research and implement methods to convert natural language statements into formal specifications and proofs using Lean, Coq, or Isabelle.
Develop techniques to guide LLM generation using formal proof assistants, tree-search algorithms, and tactic prediction.
Build automated reasoning engines to validate the logical consistency of AI-generated chains of thought using formal solvers.
Curate formal knowledge libraries and axioms like Lean Mathlib required to verify real-world claims across domains.
Design rigorous benchmarks to measure the soundness and completeness of our verification pipeline.
Contribute to the development of the company’s research strategy in artificial intelligence, formal verification, and proof-based reasoning.
Qualifications
Education: PhD or Master’s in Computer Science, Mathematics, Logic, or related field.
Formal Methods: Proficiency in Interactive Theorem Prover (ITP) such as Lean 4.
Engineering: Strong coding skills in Python and functional languages (OCaml, etc.).
AI Fundamentals: Solid understanding of Transformer architectures, LLMs, and neuro-symbolic reasoning.
Preferred: Expert knowledge of Lean 4 or experience with SMT solvers.
